This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 201 - Deadlock during broadcast channel synchronization
Summary: Deadlock during broadcast channel synchronization
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.5.9
Hardware: All All
: P3 enhancement
Assignee: Gerd Behrmann
Depends on:
Reported: 2005-09-22 12:12 CEST by Leonid Mokrushin
Modified: 2005-12-09 12:37 CET (History)
0 users

See Also:


Note You need to log in before you can comment on or make changes to this bug.
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 

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.