|Summary:||Deadlock during broadcast channel synchronization|
|Product:||UPPAAL||Reporter:||Leonid Mokrushin <leom>|
|Component:||Engine||Assignee:||Gerd Behrmann <behrmann>|
Description Leonid Mokrushin 2005-09-22 12:12:47 CEST
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.
Comment 1 Gerd Behrmann 2005-09-22 12:36:23 CEST
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.
Comment 2 Gerd Behrmann 2005-10-04 16:46:34 CEST
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.
Comment 3 Gerd Behrmann 2005-11-06 17:44:42 CET
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.
Comment 4 Gerd Behrmann 2005-12-09 12:37:33 CET
The priority extensions has the exact same problem: A transition to a state not satisfying the target invariant still takes priority over other transitions.