我想了解 [1] 中讨论的 UPPAAL SMC 示例。
这是 UPPAAL-SMC 示例：
三个定时自动机应该可视化 UPPAAL SMC 中的概率分布。在论文中指出，三个 TA 的 END 位置可以在时间间隔 [6,12]、[4,12] 和 [0,+∞) 内到达。我在 UPPAAL 中对 A1 TA 进行了建模，并且由于更新 X=0 并且边缘中的保护 x >= 2，因此不可能到达 END 位置。 时间间隔如何详细计算？
【问题讨论】：
标签： model model-checking uppaal
A1：由四个状态s1, s2, s3, s4 = END组成。可以在s1 内花费的时间量的下限是守卫x >= 2，上限是标签x <= 4。 s2 和 s3 也是如此。因此，A1 的时间间隔为[2 + 2 + 2, 4 + 4 + 4] = [6, 12]。
A2：由s1, s2, s3, s4, s5 = END 和s1, s6, s7, s5 = END 两条路径组成。第一条路径与 A1 相同。第二条路径的时间间隔为[4, 8]。总的来说，A2的时间间隔是[min(6, 4), max(12, 8)] = [4, 12]。
A3：没有时间标签也没有守卫，因此时间间隔为[0, +oo]，假设存在某个时间变量。
【讨论】：