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.