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`