Skip to content

Don't eliminate enumerations to integers for CIF to mCRL2

Currently, we employ the EnumsToInts CIF to CIF transformation as preprocessing in the CIF to mCRL2 transformation. This means that if we want to write properties over enumeration values, we have to write them over integers instead. If we apply linearization and then transform to mCRL2, this applies to location names as well. This is not very convenient.

Rather than through elimination to integers, it would be better to transform the CIF enumerations/types to mCRL2 sorts, and support some expressions over enumerations natively.