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

Bug 151 - Deadlock check is inaccurate
Summary: Deadlock check is inaccurate
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.4.9
Hardware: All All
: P2 blocker
Assignee: Gerd Behrmann
Depends on:
Reported: 2005-05-09 19:37 CEST by Gerd Behrmann
Modified: 2005-06-29 21:29 CEST (History)
2 users (show)

See Also:

Test case (1.85 KB, text/plain)
2005-05-09 19:38 CEST, Gerd Behrmann

Note You need to log in before you can comment on or make changes to this bug.
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 1 Gerd Behrmann 2005-05-09 19:38:30 CEST
Created attachment 33 [details]
Test case
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.