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

Bug 151

Summary: Deadlock check is inaccurate
Product: UPPAAL Reporter: Gerd Behrmann <behrmann>
Component: EngineAssignee: Gerd Behrmann <behrmann>
Status: CLOSED FIXED    
Severity: blocker CC: marius, miles
Priority: P2    
Version: 3.4.9   
Hardware: All   
OS: All   
Architecture:
Attachments: Test case

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.