A binary synchronization transition of a low priority process is
enabled even if a binary synchronization transition of a higher priority
process using the same channel is possible.
This problem occurs only when also a delaying transition in a third
process is enabled.
It is visible in the last transition in the attached example trace.
Example model: see attachment 1 [details]
Example trace: see attachment 2 [details]
Created attachment 214 [details]
Created attachment 215 [details]
Fixed in rev. 4378 (4.0.9) and 4379 (trunk).
We have changed the semantics because it was inconsistent.
Before, priority was resolved by comparing the priorities of
the processes involved in two transitions by descending order.
Now, it is resolved by considering the highest priority process,
which is in line with priority ceiling protocols.
In this example, it is normal to have the synchronization with
the new semantics (though not normal with the old one).