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.
Created attachment 203 [details]
model to trigger the error
Created attachment 204 [details]
sample query to start verification
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.
*** Bug 442 has been marked as a duplicate of this bug. ***