uppaal - 了解 Uppaal 中的紧急渠道

Question

我有三个自动机（见下文），单个全局声明urgent chan u;和系统声明system UrgentChannel, P1, P2;。我的理解是，通过建立u一个紧急通道，必须start进行从到的过渡。goal

我想了解为什么物业P1.start --> P1.goal不满意。模拟器中的反例在这里似乎没有帮助。

下载模型在这里。谢谢阅读！

• P1：
• P2：
• 紧急频道：

Answer 1

模拟器中的反例（诊断轨迹）有一条红色标记的尾部，表示它无限重复（P2 可以执行 zeno 循环）。基本上，Uppaal 试图告诉存在一个无限循环，它可能会阻止紧急转换达到目标状态。

如果删除进程 P2，则该属性成立。

如果您关心活性属性，​​那么这种 zeno 循环是不可取的，因此 Uppaal 正确地将它们报告为反例。

Answer 2

延迟转换 (L,v) -d-> (L,v+d) 的文档说“对于 L 中的所有位置 l 和所有位置 l'（不一定在 L 中），如果有来自 l 的边到 l' 然后要么： - 此边不通过紧急通道同步，或者 - 此边确实通过紧急通道同步，但对于所有 0 ≤ d' ≤ d，我们有 v+d' 不满足边缘。

那么为什么P2的边沿可以触发呢？