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

Bug 597 - simulate query with check returns too few simulations
Summary: simulate query with check returns too few simulations
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.1.19
Hardware: All All
: P5 normal
Assignee: Marius Mikučionis
Depends on:
Reported: 2015-06-09 13:21 CEST by Marius Mikučionis
Modified: 2015-06-21 14:01 CEST (History)
1 user (show)

See Also:

model demonstrating bug (10.07 KB, text/xml)
2015-06-09 13:21 CEST, Marius Mikučionis

Note You need to log in before you can comment on or make changes to this bug.
Description Marius Mikučionis 2015-06-09 13:21:28 CEST
Created attachment 280 [details]
model demonstrating bug

the demonstrating model attached.

consider the following queries:
A[] timer >= 100 imply forall (i : t_id) Task(i).Done

is satisfied (hence all tasks should be done by time==100)

try to extract 10 successful simulations:
simulate 10 [<=100] {timer} : 10 : forall (i : t_id) Task(i).Done

since all tasks are done by time==100, it should return all 10 simulation runs, but it returns with only 0, 1, 2, or so runs.
Comment 1 Marius Mikučionis 2015-06-21 14:01:10 CEST
the location Resource.QueueTask is committed, but the process can only leave it by receiving synchronization -- this violates SMC assumption that the process can progress independently, hence the model is not valid for SMC. It works if the committed flag is removed.

Uppaal needs to check the error flags and report the error (possibly with a trace) to the user properly.