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 Mar 12, 2018 by Michaela Klauck
Assignee Loading
Time tracking Loading