Skip to content

#1220 CIF to mCRL2: support CIF specifications with multiple initial states

  • Best to review per commit.
  • End-user visible changes:
    • The CIF to mCRL2 transformer now supports CIF specifications with multiple initial states. That is, discrete variables with multiple initial values as well as automata with multiple initial locations are now supported. However, CIF specifications with more than 231 - 1 = 2,147,483,647 potential initial states are not supported.
    • If such a CIF specification with multiple initial states is transformed, an additional initialize action is generated, and this action is then performed to non-deterministically choose an initial state, after which process P is started from that initial state. No such action is generated if the CIF specification has a single initial state. Note that this initialize action is required to get the proper state space. If it is left out, all initial states are merged, and variables can have any value, the initial state can be both marked and non-marked, etc. We need to keep initial state strictly separate.
    • The transformer no longer performs the 'Add default initial values' transformation as pre-processing.
  • Other changes:
    • AutOnlyWithCertainNumberOfInitLocsCheck: it now also allows to check a specification for only having automata with at least one location.

Addresses #1220 (closed)

Merge request reports

Loading