formal-verification - Uppaal 验证未按预期工作

Question

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

我正在尝试在我的模型中验证是否 Person(0)In最终会出现 Person(0) Out。

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

即使我在模拟器中手动检查了所有可能性，但我无法获得任何反例来验证（理论上应该满足这个条件）。

我使用的语法是否存在问题，或者 UPPAAL 是否存在此类验证的已知问题？

Answer 1

您可以通过检查选项 -> 诊断跟踪 -> 一些将反例加载到模拟器中。对于这个特定的查询（导致属性），一个常见的问题是系统可能永远停留在某个位置（或循环通过多个转换），这基本上会阻止达到目标。反例跟踪的循环部分以红色突出显示。如果回路中只有一个位置，则可能难以观察/理解。模拟器仍然允许用户向跟踪添加过渡，这是合法的，并且可能给人以系统最终会达到目标的印象，但跟踪的重点是系统无法达到的方式，那就是停止（如果没有不变量，也允许停顿）。

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