Skip to content

CIF to mCRL2 documentation, make preprocessing and supported specification consistent.

CIF to mCRL2 documentation is not consistent on whether something that is removed during preprocessing is "supported".

For example, in the cif2mcrl2 documentation:

=== Supported specifications

The CIF to mCRL2 transformer supports a subset of CIF specifications.
The following restrictions apply:

* Algebraic variables are not supported.

=== Preprocessing

The following <<tools-cif2cif-chapter-index,CIF to CIF transformations>> are applied as preprocessing (in the given order), to increase the subset of CIF specifications that can be transformed:

* <<tools-cif2cif-chapter-elim-alg-vars>>

Thus, an input specification with algebraic variables can be converted with this tool. Similarly, enum values are supported (as they are converted to ints).

We should remove the restrictions that are not really restrictions. Also, check this for the other tool documentation (I had a quick check and couldn't find other situations).

Edited by Ferdie Reijnen