UPPAAL SMC激励示例
UPPAAL SMC motivating example
我想了解 [1] 中讨论的 UPPAAL SMC 示例。
这是 UPPAAL-SMC 示例：
三个时间自动机应该可视化 UPPAAL SMC 中的概率分布。在论文中指出，三个 TA 的结束位置可以在时间间隔 [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]，假设存在某个时间变量
我想了解 [1] 中讨论的 UPPAAL SMC 示例。
这是 UPPAAL-SMC 示例：
三个时间自动机应该可视化 UPPAAL SMC 中的概率分布。在论文中指出，三个 TA 的结束位置可以在时间间隔 [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]，假设存在某个时间变量