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.
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.