uppaal - 两个紧急位置导致的僵局

Question

一个小例子在模拟过程中，我发现如果一个状态处于紧急位置，另一个状态即将到达紧急位置，就会死锁。而且我想验证时间的上下限，所以如果没有时间我必须设置紧急位置。我该如何解决这种情况？

Answer 1

死锁涉及以下依赖链：

1. P1处于紧急位置，因此阻塞了时间流逝。
2. P1 通过等待c?同步被阻止离开这个紧急位置。
3. P2 被守卫阻止t>=3（并且无法提供c!给#2），因为P2.t==0，而且时钟P2.t无法前进，因为时间被#1 停止。
4. P3 被守卫 阻挡t>=2，其中P3.t in [0,1]，而且P3.t由于#1 阻挡而无法前进。

死锁是由于 1-3 依赖循环造成的——您必须打破这些依赖之一才能解决死锁。