Uppaal核查未按预期工作

Question

因此，我试图在我的模型上运行一个非常简单的验证，但是我收到一条消息，表示属性不满意。

我试图验证，在我的模型中，如果Person(0)最终会出现In，那么Person(0)最终会出现Out。

Person(0).In --> Person(0).Out

即使我在模拟器中手动地检查了所有的可能性，我也无法得到这个验证的任何反例(理论上应该满足这个条件)。

我所使用的语法是否有问题，或者UPPAAL对这类验证是否有已知的问题？

Answer 1

您可以通过检查选项->诊断跟踪->来获得加载到模拟器中的反示例。对于这个特定的查询(引线到属性)，一个常见的问题是系统可能永远停留在某个位置(或者通过多个转换循环)，这基本上阻碍了目标的实现。反示例跟踪的循环部分以红色高亮显示。如果循环中只有一个位置，则很难观察/理解。模拟器仍然允许用户向跟踪添加转换，这是合法的，并且可能会给人留下系统最终会达到目标的印象，但跟踪的要点是，有一种方法是系统无法到达的，那就是通过延迟(如果没有不变的话也允许延迟)。

您可以在这些位置添加时间不变量，以避免无限循环和永远等待。