This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 466

Summary: Inappropriate treatment of channel priorities
Product: UPPAAL Reporter: Mohammad Mousavi <smr_mousavi>
Component: EngineAssignee: Alexandre David <adavid>
Status: RESOLVED FIXED    
Severity: major    
Priority: P2    
Version: 4.0.8   
Hardware: PC   
OS: Windows XP   
URL: http://www.win.tue.nl/~mousavi/dynamic.xml
Architecture:

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.