UPPAAL:什么导致时钟停止运行？

Question

我目前正在运行我的UPPAAL模拟器。在某个点之后，我的模拟器停止运行代码。这一点因我所提供的声明而异。但我想知道时钟什么时候停止运行？有什么能触发这一切的吗？

Answer 1

我不确定我是否正确地解释了你的问题，如果我能读懂你的模型，我可以给你一些精确的建议。

试图猜测问题是什么，我可以说，有时候Uppaal模拟器采取无穷多个离散步骤(转换)，而不增加--任何一个时钟变量。

感觉是“时钟停止了”，而其余的模拟正在进行。在这种情况下，时间并没有停止: Uppaal，在所有可能的路径中，它只是在探索时钟不进化的路径。如果模拟器(或模型检查器)可以在不增加时钟变量的情况下进行无限次的转换，那就是"Zeno路径“的一个例子。

编写模型的人有责任避免采用zeno路径的可能性。

如果您不确定您的模型是否没有Zeno路径，您可以使用已知的方法来验证一个时间自动机没有zeno路径(在Uppaal中)。

另一种可能是模拟器完全停止运行，说存在死锁。在这种情况下，问题不在于时钟停止运行，而是出现了禁用所有可能的转换的情况(可能是因为从未启用所有可能的保护，或者因为启用的转换的所有可能的目标状态都有一些时间不变量是假的)。