modelmodel-checkinguppaal

UPPAAL SMC motivating example

I want to understand the UPPAAL SMC example discussed in [1].

Here is the UPPAAL-SMC example:

UPPAAL-SMC example

The three timed automata should visualize the probability distribution in UPPAAL SMC. In the paper it is indicated that the END-locations of the three TAs can be reached within the time intervals [6,12], [4,12] and [0,+∞). I modeled the A1 TA in UPPAAL and there is no possibility to reach the END location because of the update X=0 and the guard x >= 2 in the edges. How the time-intervals are calculated in detail?

[1] http://people.cs.aau.dk/~kgl/SSFT2015/SMC%20tutorial.pdf

Solution

  • A1: is comprised by four states s1, s2, s3, s4 = END. The amount of time that can be spent inside s1 is lower-bounded by the guard x >= 2 and upper-bounded by the label x <= 4. The same holds for s2 and s3. Hence, the time interval for A1 is [2 + 2 + 2, 4 + 4 + 4] = [6, 12].

    A2: is comprised by two paths s1, s2, s3, s4, s5 = END and s1, s6, s7, s5 = END. The first path is the same as A1. The time interval of the second path is [4, 8]. Overall, the time interval for A2 is [min(6, 4), max(12, 8)] = [4, 12].

    A3: there are no time labels nor guards, hence the time interval is [0, +oo], assuming the existence of some time variable.