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

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

See Also:
Architecture:

Attachments
Test case (1.85 KB, text/plain)
2005-05-09 19:38 CEST, Gerd Behrmann 		Details
Add an attachment (proposed patch, testcase, etc.)

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.