Support complex initial state specifications
When restricting the initial state using an arithmetic expression (over global variables q1, q2, q3
in this case), the error message:
error: Complex initial states specifications are not yet supported. is thrown.
It would be nice to extend the range of supported expressions because in e.g. PRISM case studies they are used very often.
"restrict-initial":{ "exp":{ "op":"≥", "left":{ "op":"+", "left":{ "op":"+", "left":"q1", "right":"q2" }, "right":"q3" }, "right":1 } },
The currently supported syntax for initial state restrictions is checked in DissectInitialStatesRestriction()
in AutomataNetwork.cs
. And the error message is thrown in CreateSetInitialStateAndTransients()
in CompiledAutomaton.cs
Edited by Michaela Klauck