Expected Cost
|
+- [f]
|    0
|
+- [Program]
|    i :~ {1 : 0}
|    0:While(n ≥ 1 + i)
|        Choice
|          1/2: flag :~ {1 : 1}
|               1:While(flag ≥ 1)
|                   Choice
|                     1/3: flag :~ {1 : 0}
|                          Tick(3)
|                     2/3: Choice
|                            1/2: flag :~ {1 : 1}
|                                 Tick(5)
|                            1/2: flag :~ {1 : 1}
|                                 Tick(7)
|          1/2: Skip
|        i :~ {1 : 1 + i}
|
+- While.step
|  |
|  +- [Problem]
|  |    0:While(n ≥ 1 + i)
|  |        Choice
|  |          1/2: flag :~ {1 : 1}
|  |               1:While(flag ≥ 1)
|  |                   Choice
|  |                     1/3: flag :~ {1 : 0}
|  |                          Tick(3)
|  |                     2/3: Choice
|  |                            1/2: flag :~ {1 : 1}
|  |                                 Tick(5)
|  |                            1/2: flag :~ {1 : 1}
|  |                                 Tick(7)
|  |          1/2: Skip
|  |        i :~ {1 : 1 + i}
|  |
|  +- [f]
|  |    0
|  |
|  +- Expected Cost Body
|  |  |
|  |  +- Expected Cost
|  |  |  |
|  |  |  +- [f]
|  |  |  |    0
|  |  |  |
|  |  |  +- [Program]
|  |  |  |    Choice
|  |  |  |      1/2: flag :~ {1 : 1}
|  |  |  |           1:While(flag ≥ 1)
|  |  |  |               Choice
|  |  |  |                 1/3: flag :~ {1 : 0}
|  |  |  |                      Tick(3)
|  |  |  |                 2/3: Choice
|  |  |  |                        1/2: flag :~ {1 : 1}
|  |  |  |                             Tick(5)
|  |  |  |                        1/2: flag :~ {1 : 1}
|  |  |  |                             Tick(7)
|  |  |  |      1/2: Skip
|  |  |  |
|  |  |  +- While.step
|  |  |  |  |
|  |  |  |  +- [Problem]
|  |  |  |  |    1:While(flag ≥ 1)
|  |  |  |  |        Choice
|  |  |  |  |          1/3: flag :~ {1 : 0}
|  |  |  |  |               Tick(3)
|  |  |  |  |          2/3: Choice
|  |  |  |  |                 1/2: flag :~ {1 : 1}
|  |  |  |  |                      Tick(5)
|  |  |  |  |                 1/2: flag :~ {1 : 1}
|  |  |  |  |                      Tick(7)
|  |  |  |  |
|  |  |  |  +- [f]
|  |  |  |  |    0
|  |  |  |  |
|  |  |  |  +- Expected Cost Body
|  |  |  |  |  |
|  |  |  |  |  `- 5
|  |  |  |  |
|  |  |  |  +- linear-template
|  |  |  |  |  |
|  |  |  |  |  `- 1 + [flag | flag ≥ 0]
|  |  |  |  |
|  |  |  |  +- [Norms]
|  |  |  |  |    [[1 | ⊤],[flag | flag ≥ 0]]
|  |  |  |  |
|  |  |  |  +- [Invariant]
|  |  |  |  |    flag ≥ 1 ==> 5 + h([1 | ⊤],2/3) ≼ h([1 | ⊤],[flag | flag ≥ 0])
|  |  |  |  |    1 ≥ 1 + flag ==> 0 ≼ h([1 | ⊤],[flag | flag ≥ 0])
|  |  |  |  |
|  |  |  |  `- 15·[flag | flag ≥ 0]
|  |  |  |
|  |  |  `- 15/2
|  |  |
|  |  +- Expected Cost
|  |  |  |
|  |  |  +- [f]
|  |  |  |    0
|  |  |  |
|  |  |  +- [Program]
|  |  |  |    i :~ {1 : 1 + i}
|  |  |  |
|  |  |  `- 0
|  |  |
|  |  +- Expected Cost
|  |  |  |
|  |  |  +- [f]
|  |  |  |    0
|  |  |  |
|  |  |  +- [Program]
|  |  |  |    Choice
|  |  |  |      1/2: flag :~ {1 : 1}
|  |  |  |           1:While(flag ≥ 1)
|  |  |  |               Choice
|  |  |  |                 1/3: flag :~ {1 : 0}
|  |  |  |                      Tick(3)
|  |  |  |                 2/3: Choice
|  |  |  |                        1/2: flag :~ {1 : 1}
|  |  |  |                             Tick(5)
|  |  |  |                        1/2: flag :~ {1 : 1}
|  |  |  |                             Tick(7)
|  |  |  |      1/2: Skip
|  |  |  |
|  |  |  `- 0
|  |  |
|  |  `- 15/2
|  |
|  +- linear-template
|  |  |
|  |  `- 1 + [-i + n | -i + n ≥ 0]
|  |
|  +- [Norms]
|  |    [[1 | ⊤],[-i + n | -i + n ≥ 0]]
|  |
|  +- [Invariant]
|  |    n ≥ 1 + i ==> 15/2 + h([1 | ⊤],[-1 + -i + n | -1 + -i + n ≥ 0]) ≼ h([1 | ⊤],[-i + n | -i + n ≥ 0])
|  |    1 + i ≥ 1 + n ==> 0 ≼ h([1 | ⊤],[-i + n | -i + n ≥ 0])
|  |
|  `- 15/2·[-i + n | -i + n ≥ 0]
|
`- 15/2·[n | n ≥ 0]