First Last Prev Next    No search results available      Search page      Enter new bug
Bug#: 466
Product:
Component:
Status: RESOLVED
Resolution: FIXED
Assigned To: Alexandre David <adavid@cs.aau.dk>
Hardware:
OS:
Version:
Priority:
Severity:
Reporter: Mohammad Mousavi <smr_mousavi@yahoo.com>
Add CC:
CC:
URL:
Summary:

Attachment Type Creator Created Size Actions
Create a New Attachment (proposed patch, testcase, etc.) View All

Bug 466 depends on: Show dependency tree
Show dependency graph
Bug 466 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: 2009-03-29 19:51 
I am getting a counter-example from UPPAAL which clearly violates priorities. 
Consider the model uploaded at the above URL, 
when I try to model-check the following property 

E<> ((not C11.lostMsg) and (not C12.lostMsg) and Process0.NV_Inactivated and ( 
( P1.Alive or (not jnd[0])  ) and    ( P2.Alive or (not jnd[1])   )  )  )

and generate the shortest diagnostic trace, 
in the generated trace, before the last transition labeled  sndtruebeat[0] 
(taken by Process0)  both 
sndtruebeat[0] and rcvfalsebeat[2] are enabled. 
The system description specifies: 
chan priority sndtruebeat[0] < rcvfalsebeat[2];
However, in the generated trace sndtruebeat[0] is taken.

------- Comment #1 From Alexandre David 2009-08-13 15:31:31 ------- 
The state is not reachable with the development version.

------- Comment #2 From Alexandre David 2009-08-17 15:54:47 ------- 
Fixed in rev. 4384.
First Last Prev Next    No search results available      Search page      Enter new bug