Bug 466 - Inappropriate treatment of channel priorities
Summary: Inappropriate treatment of channel priorities
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.0.8
Hardware: PC Windows XP
: P2 major
Assignee: Alexandre David
URL: http://www.win.tue.nl/~mousavi/dynami...
Depends on:
Blocks:
 
Reported: 2009-03-29 19:51 CEST by Mohammad Mousavi
Modified: 2009-08-17 15:54 CEST (History)
0 users

See Also:
Architecture:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Mohammad Mousavi 2009-03-29 19:51:59 CEST
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 Alexandre David 2009-08-13 15:31:31 CEST
The state is not reachable with the development version.
Comment 2 Alexandre David 2009-08-17 15:54:47 CEST
Fixed in rev. 4384.