【发布时间】：2016-11-20 23:28:52
【问题描述】：
我目前正在运行我的 UPPAAL 模拟器。我的模拟器在某个时间点后停止运行代码。这一点取决于我提供的声明。但我想知道时钟什么时候停止运行？有什么东西会触发这个吗？
【问题讨论】：
-
请提供您的模板图片（在这种情况下相当于代码）
标签： model-checking uppaal
【发布时间】：2016-11-20 23:28:52
【问题描述】：
我不确定我是否正确解释了你的问题，如果我能读懂你的模型，我可能会给你一些准确的建议。
试图猜测问题出在哪里，我可以说有时 Uppaal 模拟器会采用无限多个离散步骤（转换）而不会增加任何时钟变量。
感觉是“时钟停止了”，而其余的模拟仍在继续。在这种情况下，时间实际上并没有停止：Uppaal，在所有可能的路径中，它只是在探索时钟不进化的路径。如果模拟器（或模型检查器）可以在不增加时钟变量的情况下进行无限多次转换，那就是“芝诺路径”的一个例子。
编写模型的人有责任避免采取芝诺路径的可能性。
如果您不确定您的模型是否没有 Zeno 路径，您可以使用已知方法来验证 Timed Automaton 是否没有 Zeno 路径（在 Uppaal 中）。
另一种可能是模拟器完全停止运行，说存在死锁。在这种情况下，问题不在于时钟停止运行，而是您遇到了所有可能的转换都被禁用的情况（可能是因为所有可能的保护都从未启用，或者因为您启用的转换的所有可能的目标状态都有一些时间不变量为假）
【讨论】：