- Best to review per commit. I added support for each concept in a separate commit.
- The CIF to mCRL2 transformation now supports:
- Biconditional binary operator. Precondition checker is not updated, as precondition was missing (was a bug). In mCRL2, we use mCRL'2
==for both CIF's<=>and=now. - Cast expressions that don't change the type.
- Location references. They get eliminated by linearization.
- Channels and receive expressions. They get eliminated by linearization.
- Trivially 'true' init preds in components. They have no effect and are thus ignored.
- Non-restrictive invariants. They have no effect and are thus ignored.
- 'if' expressions.
- 'switch' expressions. Supported through conversion to
ifexpressions. - Equations. Only for algebraic variables, as continuous variables are not supported. Equations get eliminated by eliminating algebraic variables. May introduce
ifexpressions if equations are defined per location. - 'if' updates. Supported by transforming them to
ifexpressions. (fixes #229 (closed))
- Biconditional binary operator. Precondition checker is not updated, as precondition was missing (was a bug). In mCRL2, we use mCRL'2
- Other changes:
-
CifToMcrl2PreChecker: sorted theNoSpecificBinaryOpentries.
-
Addresses #948 (closed) Closes #229 (closed)
Edited by Dennis Hendriks