系统包含死锁 - 如何找到它？ （UPPAAL）

Question

我使用UPPAAL建立了模型，并使用验证程序检查死锁。答案是：财产不满意。因此存在僵局。

UPPAAL有办法报告有关死锁的更多详细信息，例如特定情况下所有变量的状态和当前值吗？

Answer 1

是的。我们可以在UPPAAL i-e中追踪死锁，我们可以找到导致死锁的状态或路径。 转到选项 - >诊断跟踪 - >最快。您可以在诊断追踪中选择某些/最快/最短的选项中的任何一个。选择最快后。转到验证程序并检查死锁锁定属性。在进入模拟器之后，通过选择“是”存储新模拟曲线，它将向您显示新的商店曲线，使属性不可满足。 希望它会有帮助