Skip to content

CIF to mCRL2 transformation ignores nesting of events

If you transform a CIF specification to mCRL2 that contains an event declared as part of a group or automaton, the resulting mCRL2 event uses the local name of the event instead the absolute name. For example:

group A:
   event B;
end

becomes

act B;

with no reference to group A.

It is possible to avoid this by applying the lift-events transformation before CIF to mCRL2, but that is not mentioned in the documentation.

Edited by Dennis Hendriks