|Summary:||Deadlock check is inaccurate|
|Product:||UPPAAL||Reporter:||Gerd Behrmann <behrmann>|
|Component:||Engine||Assignee:||Gerd Behrmann <behrmann>|
Description Gerd Behrmann 2005-05-09 19:37:43 CEST
In certain models, some deadlocks are missed by the deadlock detector. I have attached one such model, which has a deadlock in the second location of process P0 (for x=450 and y=0), but this deadlock is not detected. The deadlock is detected when the second reset of y is removed. The problem seems to be that during deadlock detection, when computing the subset of a symbolic state which is not deadlocked, resets of a clock are assumed to be possible at any point in time. This is not entirely true, as the invariant must of course be satisfied.
Comment 2 Gerd Behrmann 2005-05-09 19:39:29 CEST
Reassigning to me.
Comment 3 Gerd Behrmann 2005-05-10 14:42:58 CEST
This bug affects the liveness checker as well. A fix for UPPAAL 3.4 has been checked into CVS.
Comment 4 Gerd Behrmann 2005-06-17 18:16:19 CEST
A fix for 3.5 has been checked in.