Bug 542

Summary: false deadlock claimed and even trace provided, but no deadlock is found
Product: UPPAAL Reporter: Marius Mikučionis <marius>
Component: EngineAssignee: Alexandre David <adavid>
Status: NEW ---    
Severity: minor CC: filipjares
Priority: P5    
Version: 4.1.13   
Hardware: PC   
OS: All   
Attachments: sample model

Description Marius Mikučionis 2013-01-15 23:23:02 CET
Created attachment 256 [details]
sample model

Deadlock properties in conjunction with clock constraints may exhibit false results.
For example, the following property yields a trace, but the deadlock is not shown in the simulator:

E<> (gl_h<2000) && deadlock

Interestingly, upon a very similar query Uppaal does not claim deadlock:

E<> deadlock && (gl_h<2000)

I think the problem is that with the first query, the query checker applies the clock constrain and then checks the deadlock (which might be there as the symbolic state just got constrained), and in the second query, the "deadlock" is always false and thus the constraint is never evaluated.
Comment 1 Marius Mikučionis 2013-01-15 23:31:37 CET
Stable version 4.0.13 also has this issue.