Bug 438 - false error index out of range for channel array on disabled transition
Summary: false error index out of range for channel array on disabled transition
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: unspecified
Hardware: All All
: P2 minor
Assignee: Alexandre David
URL:
: 442 (view as bug list)
Depends on:
Blocks:
 
Reported: 2008-04-01 15:07 CEST by Marius Mikučionis
Modified: 2008-09-12 17:17 CEST (History)
1 user (show)

See Also:
Architecture:


Attachments
model to trigger the error (1.27 KB, text/xml)
2008-04-01 15:07 CEST, Marius Mikučionis
Details
sample query to start verification (91 bytes, application/octet-stream)
2008-04-01 15:08 CEST, Marius Mikučionis
Details

Note You need to log in before you can comment on or make changes to this bug.
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. ***