deadlock caused by two urgent locations

Question

a small exampleDuring the simulation, I find that if one state is in urgent location, the other state is about to reach urgent location, and it will deadlock. And I want to verify the upper and lower bounds of time, so I must set urgent location if there is not time. How can I solve this situation?

Answer 1

The deadlock involves the following chain of dependencies:

1. P1 is in urgent location and thus blocking the time passage.
2. P1 is blocked from leaving this urgent location by waiting for c? synchronization.
3. P2 is blocked by the guard t>=3 (and cannot supply c! to #2) because P2.t==0, moreover clock P2.t cannot progress because the time is stopped by #1.
4. P3 is blocked by the guard t>=2, where P3.t in [0,1], moreover P3.t cannot progress because #1 is blocking.

The deadlock is due to a 1-3 dependency cycle -- you have to break one of these dependencies in order to resolve the deadlock.