当我A[] not deadlock在模型上的 Verifier 中运行查询时，验证停止并出现错误：
验证因错误而中止。这很可能是由超出范围的分配或超出范围的数组查找引起的。
这是否暗示我的模型在“超出范围的赋值或超出范围的数组查找”发生之前是无死锁的？
问问题
1266 次
2 回答
0
如果 UPPAAL 能够回答查询，那么继续搜索状态空间是没有意义的。所以我认为你可以假设状态空间 UPPAAL 设法搜索的部分是无死锁的。
请记住，可能通过多个跟踪达到错误状态，但这取决于您的模型。
听起来您已经知道为什么会收到此错误。您可以尝试通过向!willCauseError()模型添加保护来修复它，以确保您永远不会陷入这种错误状态。不过，这本身可能会导致僵局。为避免这种情况，您可以使用对面的守卫添加从相关位置到自身的过渡willCauseError()。这将迫使程序进入活锁而不是死锁。
于 2014-05-18T15:23:11.070 回答
-1
解决方案是在检查死锁时使用索引变量扩展查询，例如
A[] not deadlock || indexVarble => 24
所以如果出现死锁，应该是在我们超出范围的时候。（在示例中，范围为 [0-23]）
于 2014-05-18T17:30:33.953 回答