| Summary: | false deadlock claimed and even trace provided, but no deadlock is found | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Marius Mikučionis <marius> |
| Component: | Engine | Assignee: | Alexandre David <adavid> |
| Status: | NEW --- | ||
| Severity: | minor | CC: | filipjares |
| Priority: | P5 | ||
| Version: | 4.1.13 | ||
| Hardware: | PC | ||
| OS: | All | ||
| Architecture: | |||
| Attachments: | sample model | ||
Stable version 4.0.13 also has this issue. |
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.