pins2lts-mc / treedbs with state vector of size 1

utwente-fmt / ltsmin

The LTSmin model checking toolset

http://ltsmin.utwente.nl

BSD 3-Clause "New" or "Revised" License

51 stars 30 forks source link

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

Open jacopol opened 4 years ago

jacopol commented 4 years ago

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 commented 4 years ago

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.