Skip to content

#838 Warn about state/event exclusion invariants with events that are not in the alphabet of the specification

  • Best to review per commit.
  • Changes:
    • Type checker now warns about state/event exclusion invariants with events that are not in the send/receive/synchronization alphabet of the specification. Note that state/event exclusion invariants with events that are only used as channels is not a problem.
    • Removed a similar check in the CIF to BDD conversion, as that is now a duplicate.
    • The CIF to CIF 'eliminate state/event exclusion invariants' transformation now removes state/event exclusion invariants for events that are not in the synchronization, send or receive alphabet of the specification, rather than converting them to automata. This prevents the events from becoming part of the synchronization alphabet of the specification, which would mean transitions could then become possible for these events, while that was not the case before the transformation. It thus prevents the state space of the specification from changing due to such cases. If any such invariants are encountered, the transformation prints a warning.
    • Improved some JavaDocs.

Closes #838 (closed)

Edited by Dennis Hendriks

Merge request reports