cif2mcrl2: support models with input variables and multiple initial states
The cif2mcrl2 does not support specifications with input variables and multiple initial states. Extend the tool to support these specifications.
Possible features to support:
-
Multiple initial states (limited to Java's max_int, so 2^31 - 1). (!1314 (merged)) -
Multiple initial states (without an upper bound on the number of them). (!1315 (merged)) -
Input variables. (!1319 (merged)) -
State/event exclusion invariants. (!1321 (merged)) -
Initialization predicates in components. (!1329 (merged)) -
Automata with multiple initial states, where it can't be statically decided which one is the single initial state. (these become initialization predicates during linearization) (!1330 (merged)) -
State invariants. (eliminating them can lead to initialization predicates in components, so that needs to be supported first) (!1332 (merged))
Edited by Dennis Hendriks