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

Bug 529

Summary: simulations stop prematurely when one of the conditions is satisfied
Product: UPPAAL Reporter: Marius Mikučionis <marius>
Component: EngineAssignee: Alexandre David <adavid>
Status: NEW ---    
Severity: normal    
Priority: P2    
Version: unspecified   
Hardware: PC   
OS: All   
Architecture:

Description Marius Mikučionis 2012-01-06 18:16:49 CET 
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.
Comment 1 Marius Mikučionis 2012-01-06 18:17:32 CET 
forgot to mention that t is the additional global clock that is never reset.