First Last Prev Next    No search results available      Search page      Enter new bug
Bug#: 438
Product:
Component:
Status: RESOLVED
Resolution: FIXED
Assigned To: Alexandre David <adavid@cs.aau.dk>
Hardware:
OS:
Version:
Priority:
Severity:
Reporter: Marius Mikucionis <marius@cs.aau.dk>
Add CC:
CC:
Remove selected CCs
URL:
Summary:

Attachment Type Creator Created Size Actions
model to trigger the error text/xml Marius Mikucionis 2008-04-01 15:07 1.27 KB Details
sample query to start verification application/octet-stream Marius Mikucionis 2008-04-01 15:08 91 bytes Details
Create a New Attachment (proposed patch, testcase, etc.) View All

Bug 438 depends on: Show dependency tree
Show dependency graph
Bug 438 blocks:
Votes: 0    Show votes for this bug    Vote for this bug

Additional Comments:







View Bug Activity   |   Format For Printing   |   XML   |   Clone This Bug

Description:   Opened: 2008-04-01 15:07 
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 From Marius Mikucionis 2008-04-01 15:07:46 ------- 
Created an attachment (id=203) [details]
model to trigger the error

------- Comment #2 From Marius Mikucionis 2008-04-01 15:08:13 ------- 
Created an attachment (id=204) [details]
sample query to start verification

------- Comment #3 From Marius Mikucionis 2008-04-01 15:11:23 ------- 
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 From Alexandre David 2008-09-12 17:17:02 ------- 
*** Bug 442 has been marked as a duplicate of this bug. ***
First Last Prev Next    No search results available      Search page      Enter new bug