The following system causes deadlock and process P0 cannot move from loc1 to loc2: broadcast chan fire; P0: (loc1)---[fire!]--->(loc2) P1: (loc3)---[fire?]--->(loc4, Invariant: false) The workaround is to use committed location between loc3 and loc4 in P1. However it requires additional reasoning about how this location should be left if invariant in false.
I see the problem. It is caused by P1 being stopped from entering loc4 not by a guard but by an invariant on the loc4; this might also have been an upper bound on a clock and the problem would have been the same. But, this behaviour is actually according to the semantics described in the help files (in the GUI). We could change the semantics, but this will most likely require non-trivial changes in how to compute successors.
I reduce the severity to an enhancement bug, as technically the behaviour is as documented. But I do consider this a very unfortunate behaviour that we should consider changing when we get the possbility.
Reducing priority as I do not consider this essential for 3.6 final. The behaviour is unfortunate, but major work on semantics is problematic at this point.
The priority extensions has the exact same problem: A transition to a state not satisfying the target invariant still takes priority over other transitions.