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

Bug 201

Summary:	Deadlock during broadcast channel synchronization
Product:	UPPAAL	Reporter:	Leonid Mokrushin <leom>
Component:	Engine	Assignee:	Gerd Behrmann <behrmann>
Status:	ASSIGNED ---
Severity:	enhancement
Priority:	P3
Version:	3.5.9
Hardware:	All
OS:	All
Architecture:

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.