search

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

Can ltsmin read the SMV format file? #207

Open gipsyh opened 1 year ago

gipsyh commented 1 year ago

Can ltsmin read the SMV format file?

thanks!

jacopol commented 1 year ago

Hi Yuheng Su, Currently, LTSmin cannot read SMV, unfortunately. But we would be interested if you would contribute that.

The "standard" way would be to provide a language module by implementing the PINS-interface for SMV (similar to DVE, Promela, etc.). This would provide access to parallel explicit state model checking + POR, and to (multicore) symbolic model checking. An interesting alternative would be to define a new "symbolic" interface, and use the symbolic algorithms from LTSmin directly on SMV models (this would save some re-encoding of the state space).