ExecutionLog
|
`- 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]

[Success] 15/2[n | n  0]
Degree: 1