Skip to content

#1247 CIF to CIF transformation to eliminate state invariants: add precondition to disallow synchronizing events

  • Best to review per commit.
  • End-user visible changes:
    • The CIF to CIF transformation to eliminate state invariants no longer supports synchronizing events, events that are in the alphabet of multiple automata. To eliminate synchronization, apply the 'Linearize (product)' CIF to CIF transformation before applying the 'Eliminate state invariants' transformation.
    • The CIF to mCRL2 transformer now applies the 'Eliminate state invariants' CIF to CIF transformation as preprocessing after linearization, rather than before linearization.

Addresses #1247 (closed)

Merge request reports

Loading