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

pins2lts-mc / treedbs with state vector of size 1 #175

Open
jacopol opened this issue Nov 14, 2019 · 1 comment
Open

pins2lts-mc / treedbs with state vector of size 1 #175

jacopol opened this issue Nov 14, 2019 · 1 comment

Comments

@jacopol
Copy link
Contributor

jacopol commented Nov 14, 2019

For small examples,*2lts-mc complains that a state vector of length 1 cannot be handled:
opaal2lts-mc, file treedbs-ll.c, line 488: assertion "nNodes >= 2" failed: Tree vectors too small: 1

This could be improved by adding a dummy state slot dummy:{1}.

There are several use cases for this:

  • users may try out the tool with a small example
  • we want to run unit tests on models from external language providers
  • we should support model checking of pre-computed (explicit) state spaces
@jacopol
Copy link
Contributor Author

jacopol commented Nov 14, 2019

A workaround that seems to work is currently: *2lts-mc --state=table.
So an alternative quick solution could be to change the default state representation when the state vector has length 1.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant