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

Bug 542 - false deadlock claimed and even trace provided, but no deadlock is found
Summary: false deadlock claimed and even trace provided, but no deadlock is found
Status: NEW
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.1.13
Hardware: PC All
: P5 minor
Assignee: Alexandre David
Depends on:
Reported: 2013-01-15 23:23 CET by Marius Mikučionis
Modified: 2013-01-16 00:21 CET (History)
1 user (show)

See Also:

sample model (7.23 KB, text/xml)
2013-01-15 23:23 CET, Marius Mikučionis

Note You need to log in before you can comment on or make changes to this bug.
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.