Take a train gate example from demo/smc directory.
Try the following property:
Pr[<=1000] (<> (t>50) && (Gate.len<2))
the expected probability should be close to zero, but UPPAAL reports close 1.
if one swaps the terms, like: Pr[<=1000] (<> (Gate.len<2) && (t>50))
then UPPAAL reports close to zero.
I tried to debug this, and queryfilter never reports "satisfied", but somehow the simulations stop just right on time 50.
forgot to mention that t is the additional global clock that is never reset.