Bug 597

Summary: simulate query with check returns too few simulations
Product: UPPAAL Reporter: Marius Mikučionis <marius>
Component: EngineAssignee: Marius Mikučionis <marius>
Status: ASSIGNED ---    
Severity: normal CC: adavid
Priority: P5    
Version: 4.1.19   
Hardware: All   
OS: All   
Attachments: model demonstrating 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.