UPPAAL验证器

Question

我在UPPAAL软件中有一个模型，并尝试验证items2 == 3是否在每种情况下。我已经尝试过了: A<>(items == 0和items1 == 0和items2 == 3)

我创建了一个“关闭”状态(对于每个模板)，无论items2 == 3是否在那里，模型都会在那里。从这个状态没有向外。如果我正确地阅读了文档，A<>应该会准确地找到这个状态，并检查items2 == 3。

你知道我做错了什么吗？

enter image description here

我检查过了，这是唯一的死锁/活锁

谢谢你的转发！

Answer 1

如果存在避免使用状态属性的死锁或无限跟踪，则A<>属性可能变为false。

尝试在Options中启用Diagnostic trace，然后再次检查该属性，并在模拟器中检查跟踪。注意死锁、无限延迟和无限循环(最后一步以红色突出显示)。