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.
Created attachment 33 [details]
Reassigning to me.
This bug affects the liveness checker as well.
A fix for UPPAAL 3.4 has been checked into CVS.
A fix for 3.5 has been checked in.