0

我用 UPPAAL 建立了一个模型，并使用验证器检查死锁。答案是：物业不满意。因此存在死锁。

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

4

1 回答 1

1

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

于 2016-11-29T07:34:55.190 回答