search

SRI-CSL / sally

A model checker for infinite-state systems.
http://sri-csl.github.io/sally/
GNU General Public License v2.0
69 stars 12 forks source link

Parse errors #46

Open rainoftime opened 7 years ago

rainoftime commented 7 years ago

It seems sally can only parse examples from /test/regess/*.

Whenever running the mcmt cases from the examples folder, I got the following information:

Parse error: ../../examples/honeywell/Ex3.mcmt:28:20:

And the sal cases returned

src/parser/sal/sal_state.cpp:620: sally::expr::term_ref sally::parser::sal_state::mk_term_from_guarded(sally::expr::term_ref, const std::vector<sally::expr::term_ref>&): Assertion false 'failed'. Aborted (core dumped)

dddejan commented 7 years ago

Sorry, this is not well documented.

The .mcmt examples were obtained by a translation process from SAL, and they are not in the pure mcmt language. They need the option --lsal-extensions to parse.

Sally does not yet support the SAL language, the SAL files are just there as they are the original models from which the mcmt models were generated.

rainoftime commented 7 years ago

Thank you!