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) ) and ( P2.Alive or (not jnd) ) ) )
and generate the shortest diagnostic trace,
in the generated trace, before the last transition labeled sndtruebeat
(taken by Process0) both
sndtruebeat and rcvfalsebeat are enabled.
The system description specifies:
chan priority sndtruebeat < rcvfalsebeat;
However, in the generated trace sndtruebeat is taken.
The state is not reachable with the development version.
Fixed in rev. 4384.