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

Bug 529 - simulations stop prematurely when one of the conditions is satisfied
Summary: simulations stop prematurely when one of the conditions is satisfied
Status: NEW
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: unspecified
Hardware: PC All
: P2 normal
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2012-01-06 18:16 CET by Marius Mikučionis
Modified: 2012-01-06 18:17 CET (History)
0 users

See Also:
Architecture:

Attachments
Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
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.