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

Bug 438

Summary: false error index out of range for channel array on disabled transition
Product: UPPAAL Reporter: Marius Mikučionis <marius>
Component: EngineAssignee: Alexandre David <adavid>
Severity: minor CC: tbourke
Priority: P2    
Version: unspecified   
Hardware: All   
OS: All   
Attachments: model to trigger the error
sample query to start verification

Description Marius Mikučionis 2008-04-01 15:07:03 CEST
UPPAAL reports index out of range error and stops verification even though the transition is disabled.
The problem has been reported on yahoo mailing list.
Comment 1 Marius Mikučionis 2008-04-01 15:07:46 CEST
Created attachment 203 [details]
model to trigger the error
Comment 2 Marius Mikučionis 2008-04-01 15:08:13 CEST
Created attachment 204 [details]
sample query to start verification
Comment 3 Marius Mikučionis 2008-04-01 15:11:23 CEST
It appears that UPPAAL looks at synchronization first, before evaluating the guards. I produced a fix on a trunk (rev.3441) to evaluate the integer guards before any synchronization expression is touched.
Regression passed, hopefully nothing is broken.
Comment 4 Alexandre David 2008-09-12 17:17:02 CEST
*** Bug 442 has been marked as a duplicate of this bug. ***