uppaal - 如果 Uppaal 去掉相对时间怎么办？

Question

我希望这里有人可以给我你的建议或知识。

我已经在 Uppaal 和 Spin 中阅读了有关火车门的示例。我还尝试使用 Uppaal 来验证我的计划，结果非常好。然而。我想稍微扩展我的计划。因此，我尝试使用 Spin 来验证一些与时间无关的属性。

我的问题是：我是否可以理解，如果我删除相对时间（时钟），Uppaal 可以处理相同的旋转。如果没有，你能给我一个例子或财产来证明吗？

任何信息或建议对我都有帮助。非常感谢您的阅读。

Answer 1

UPPAAL 假设密集时间语义，这意味着像“下一个状态”这样的查询没有意义。它还假设同步时间，因此它的算法可以利用的假设更少，因此对于不定时模型的验证可能会更慢。