model - UPPAAL 验证器

Question

我在 UPPAAL 软件中有一个模型，并尝试在每种情况下验证 items[2] == 3。我试过了： A<>(items[0] == 0 and items 1 == 0 and items[2] == 3)

我做了一个“关闭”状态（对于每个模板），无论 items[2] == 3，模型都会去那里。从那个状态开始没有向外。如果我正确阅读了文档，A<> 应该会找到这种状态并检查 items[2] == 3。

你知道我做错了什么吗？

在此处输入图像描述

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

谢谢转发！

标签： modelverificationuppaal

Answer 1

A<>如果出现死锁或无限跟踪避免 state 属性，则属性可能会变为 false。

尝试启用Diagnostic tracein Options，然后再次检查属性并检查模拟器中的跟踪。当心死锁、无限延迟和无限循环（最后一步以红色突出显示）。