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.