我想了解 [1] 中讨论的 UPPAAL SMC 示例。
这是 UPPAAL-SMC 示例：
三个定时自动机应该可视化 UPPAAL SMC 中的概率分布。在论文中指出，三个 TA 的 END 位置可以在时间间隔 [6,12]、[4,12] 和 [0,+∞) 内到达。我在 UPPAAL 中对 A1 TA 进行了建模，并且由于更新 X=0 并且边缘中的防护 x >= 2，因此不可能到达 END 位置。如何详细计算时间间隔？
[1] http://people.cs.aau.dk/~kgl/SSFT2015/SMC%20tutorial.pdf
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]，假设存在一些时间变量。