- Best to review per commit. The commits about tests do change files multiple times, and intermediate ones are not entirely consistent with the output of the tool, as I applied some interactive rebasing.
- This essentially involves a complete rewrite of the CIF to mCRL2 transformer, now based on first doing linearization:
- See #352 (closed) for the reasons why we go this route.
- The transformation is now much simpler, and we can easily extend it for the various open issues.
- I kept the preconditions mostly the same. Similarly for handling of runtime errors. And so on. I tried to keep it as much as possible the same, while linearizing and not having an instance tree.
- Some parts are inspired by the code of the old implementation, like the application class, the 'generate value actions' option, conversion of types/expressions.
- End-user visible changes:
- The CIF to mCRL2 transformer has been completely re-implemented, and is now based on first linearizing the CIF specification.
- For a CIF specification, the generated mCRL2 model now has a single process. Removed the instance tree and instance tree debug related options. This is backward incompatible, but users will notice the missing options.
- Urgent locations and edges are no longer supported.
- I added section comments to the generated mCRL2 models.
- Less preprocessing before precondition check, to report as much as possible on the original model.
- No 'eliminate self' preprocessing, as component types are not supported anyway.
- Additional preprocessing to eliminate type declarations. And it now performs linearization.
- For recursive process call, now only the assigned variables are included, not all variables, and the arguments are named rather than positional. This reduces the model size and improves readability.
- Different naming scheme. Uses absolute names now, like we do in other transformations. Uses
'
instead of.
and ends with'
to ensure no keyword clashes. Value actions get a postfix. (fixes #224 (closed)) - No more summations in the generated mCRL2 models.
- No more location pointer (sort) for automata with only one location.
- Updated/improved documentation.
- The 'Generate value actions' option has been renamed from
--read-values
/-r
to--value-actions
/-v
. The read/write stuff doesn't exist anymore, so the old name no longer makes any sense. This is backward incompatible, but the old name doesn't exist anymore, so it gives an error. Users will notice that.
- Other changes:
- Added
CifCollectUtils.collectDiscVariables
. - I separated the application and library parts, for the CIF to mCRL2 transformation.
- I name the classes
CifToMcrl2*
, notCif2Mcrl2*
, as that fits with the other applications. - CIF integration tests
copy_all
script now handles.mcrl2.real
files. - Tests updated, improved, extended and no longer relevant ones removed.
- I added a script to generate state spaces using mCRL2. I ran it manually and checked the output of the test models.
- Added
Closes #352 (closed), #224 (closed)
Edited by Dennis Hendriks