Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[BUG] fails with modelator trace --model-checker tlc spec.tla spec.cfg #156

Closed
danwt opened this issue Dec 16, 2021 · 1 comment · Fixed by #157
Closed

[BUG] fails with modelator trace --model-checker tlc spec.tla spec.cfg #156

danwt opened this issue Dec 16, 2021 · 1 comment · Fixed by #157
Assignees
Labels
bug Something isn't working
Milestone

Comments

@danwt
Copy link
Contributor

danwt commented Dec 16, 2021

modelator 0.4.1

Description

modelator trace --model-checker tlc spec.tla spec.cfg
thread 'main' panicked at '[modelator] full TLA state should have been parsed', modelator/src/model/language/tla/json/mod.rs:10:13
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

I need time to create a minimal example.

System information

  • OS: OSX Big Sur M1

Additional context

Mirrors https://github.com/informalsystems/mbt/issues/45

@danwt danwt added the bug Something isn't working label Dec 16, 2021
@rnbguy
Copy link
Member

rnbguy commented Dec 17, 2021

The parser throws error because it does not support ranged sets i.e. 1..10. Let me create a PR to add support.

@rnbguy rnbguy self-assigned this Dec 17, 2021
@rnbguy rnbguy added this to the 12.2021 milestone Dec 17, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants