Expected Cost
|
+- [f]
|    0
|
+- [Program]
|    0:If(y ≥ 0) Then
|        Skip
|      Else
|        Abort
|    1:While(0 ≥ 1 + n)
|        Choice
|          9/10: n :~ {1 : 1 + n}
|          1/10: Skip
|        Tick(9)
|        NonDet
|          {2:While(y ≥ 100)
|               Choice
|                 1/2: y :~ {1 : -100 + y}
|                 1/2: y :~ {1 : -90 + y}
|               Tick(5)}
|          {Skip}
|        y :~ {1 : 1000 + y}
|
+- While.step
|  |
|  +- [Problem]
|  |    1:While(0 ≥ 1 + n)
|  |        Choice
|  |          9/10: n :~ {1 : 1 + n}
|  |          1/10: Skip
|  |        Tick(9)
|  |        NonDet
|  |          {2:While(y ≥ 100)
|  |               Choice
|  |                 1/2: y :~ {1 : -100 + y}
|  |                 1/2: y :~ {1 : -90 + y}
|  |               Tick(5)}
|  |          {Skip}
|  |        y :~ {1 : 1000 + y}
|  |
|  +- [f]
|  |    0
|  |
|  +- Expected Cost Body
|  |  |
|  |  +- Expected Cost
|  |  |  |
|  |  |  +- [f]
|  |  |  |    0
|  |  |  |
|  |  |  +- [Program]
|  |  |  |    NonDet
|  |  |  |      {2:While(y ≥ 100)
|  |  |  |           Choice
|  |  |  |             1/2: y :~ {1 : -100 + y}
|  |  |  |             1/2: y :~ {1 : -90 + y}
|  |  |  |           Tick(5)}
|  |  |  |      {Skip}
|  |  |  |
|  |  |  +- While.step
|  |  |  |  |
|  |  |  |  +- [Problem]
|  |  |  |  |    2:While(y ≥ 100)
|  |  |  |  |        Choice
|  |  |  |  |          1/2: y :~ {1 : -100 + y}
|  |  |  |  |          1/2: y :~ {1 : -90 + y}
|  |  |  |  |        Tick(5)
|  |  |  |  |
|  |  |  |  +- [f]
|  |  |  |  |    0
|  |  |  |  |
|  |  |  |  +- Expected Cost Body
|  |  |  |  |  |
|  |  |  |  |  `- 5
|  |  |  |  |
|  |  |  |  +- linear-template
|  |  |  |  |  |
|  |  |  |  |  `- 1 + [-99 + y | -99 + y ≥ 0]
|  |  |  |  |
|  |  |  |  +- [Norms]
|  |  |  |  |    [[1 | ⊤],[-99 + y | -99 + y ≥ 0]]
|  |  |  |  |
|  |  |  |  +- [Invariant]
|  |  |  |  |    y ≥ 100 ==> 5 + h([1 | ⊤],1/2·[-199 + y | -199 + y ≥ 0] + 1/2·[-189 + y | -189 + y ≥ 0]) ≼ h([1 | ⊤],[-99 + y | -99 + y ≥ 0])
|  |  |  |  |    100 ≥ 1 + y ==> 0 ≼ h([1 | ⊤],[-99 + y | -99 + y ≥ 0])
|  |  |  |  |
|  |  |  |  `- 5·[-99 + y | -99 + y ≥ 0]
|  |  |  |
|  |  |  `- 5·[-99 + y | -99 + y ≥ 0]
|  |  |
|  |  +- Expected Cost
|  |  |  |
|  |  |  +- [f]
|  |  |  |    0
|  |  |  |
|  |  |  +- [Program]
|  |  |  |    y :~ {1 : 1000 + y}
|  |  |  |
|  |  |  `- 0
|  |  |
|  |  +- Expected Cost
|  |  |  |
|  |  |  +- [f]
|  |  |  |    0
|  |  |  |
|  |  |  +- [Program]
|  |  |  |    NonDet
|  |  |  |      {2:While(y ≥ 100)
|  |  |  |           Choice
|  |  |  |             1/2: y :~ {1 : -100 + y}
|  |  |  |             1/2: y :~ {1 : -90 + y}
|  |  |  |           Tick(5)}
|  |  |  |      {Skip}
|  |  |  |
|  |  |  `- 0
|  |  |
|  |  `- 81/10 + 9/2·[-99 + y | -99 + y ≥ 0] + 9/10 + 1/2·[-99 + y | -99 + y ≥ 0]
|  |
|  +- mixed-lin-template
|  |  |
|  |  `- 1 + 2·([-99 + y | -99 + y ≥ 0]) + 2·([-99 + y | -99 + y ≥ 0]·[-n | -n ≥ 0]) + 2·([-n | -n ≥ 0]) + [-n | -n ≥ 0]^2
|  |
|  +- [Norms]
|  |    [[1 | ⊤],[-99 + y | -99 + y ≥ 0],[99·(n) + -n·y | -99 + y ≥ 0 ∧  -n ≥ 0],[-n | -n ≥ 0],[n^2 | -n ≥ 0]]
|  |
|  +- While.step
|  |  |
|  |  +- [Problem]
|  |  |    2:While(y ≥ 100)
|  |  |        Choice
|  |  |          1/2: y :~ {1 : -100 + y}
|  |  |          1/2: y :~ {1 : -90 + y}
|  |  |        Tick(5)
|  |  |
|  |  +- [f]
|  |  |    [-901·(n) + -n·y | 901 + y ≥ 0 ∧  -n ≥ 0]
|  |  |
|  |  +- linear-template
|  |  |  |
|  |  |  `- 1 + [-99 + y | -99 + y ≥ 0] + [-99 + y | -99 + y ≥ 0]·[100·(n) | 100·(n) ≥ 0] + [-901·(n) + -n·y | 901 + y ≥ 0 ∧  -n ≥ 0]
|  |  |
|  |  +- [Norms]
|  |  |    [[1 | ⊤],[-99 + y | -99 + y ≥ 0],[-9900·(n) + 100·(n·y) | -99 + y ≥ 0 ∧  100·(n) ≥ 0],[-901·(n) + -n·y | 901 + y ≥ 0 ∧  -n ≥ 0]]
|  |  |
|  |  +- [Invariant]
|  |  |    y ≥ 100 ==> 0 + h([1 | ⊤],1/2·[-199 + y | -199 + y ≥ 0] + 1/2·[-189 + y | -189 + y ≥ 0],50·[-199·(n) + n·y | -199 + y ≥ 0 ∧  100·(n) ≥ 0] + 50·[-189·(n) + n·y | -189 + y ≥ 0 ∧  100·(n) ≥ 0],1/2·[-801·(n) + -n·y | 801 + y ≥ 0 ∧  -n ≥ 0] + 1/2·[-811·(n) + -n·y | 811 + y ≥ 0 ∧  -n ≥ 0]) ≼ h([1 | ⊤],[-99 + y | -99 + y ≥ 0],[-9900·(n) + 100·(n·y) | -99 + y ≥ 0 ∧  100·(n) ≥ 0],[-901·(n) + -n·y | 901 + y ≥ 0 ∧  -n ≥ 0])
|  |  |    100 ≥ 1 + y ==> [-901·(n) + -n·y | 901 + y ≥ 0 ∧  -n ≥ 0] ≼ h([1 | ⊤],[-99 + y | -99 + y ≥ 0],[-9900·(n) + 100·(n·y) | -99 + y ≥ 0 ∧  100·(n) ≥ 0],[-901·(n) + -n·y | 901 + y ≥ 0 ∧  -n ≥ 0])
|  |  |
|  |  `- [-901·(n) + -n·y | 901 + y ≥ 0 ∧  -n ≥ 0]
|  |
|  +- [Invariant]
|  |    0 ≥ 1 + n ==> 81/10 + 9/2·[-99 + y | -99 + y ≥ 0] + 9/10 + 1/2·[-99 + y | -99 + y ≥ 0] + h([1 | ⊤],sup(900,9/10·[901 + y | 901 + y ≥ 0]) + sup(100,1/10·[901 + y | 901 + y ≥ 0]),9/10·[-901 + -901·(n) + -n·y + -y | -1 + -n ≥ 0 ∧  901 + y ≥ 0] + 1/10·[-901·(n) + -n·y | 901 + y ≥ 0 ∧  -n ≥ 0],-9/10·[1 + n | -1 + -n ≥ 0] + -1/10·[n | -n ≥ 0],9/10·[1 + 2·(n) + n^2 | -1 + -n ≥ 0] + 1/10·[n^2 | -n ≥ 0]) ≼ h([1 | ⊤],[-99 + y | -99 + y ≥ 0],[99·(n) + -n·y | -99 + y ≥ 0 ∧  -n ≥ 0],[-n | -n ≥ 0],[n^2 | -n ≥ 0])
|  |    1 + n ≥ 1 ==> 0 ≼ h([1 | ⊤],[-99 + y | -99 + y ≥ 0],[99·(n) + -n·y | -99 + y ≥ 0 ∧  -n ≥ 0],[-n | -n ≥ 0],[n^2 | -n ≥ 0])
|  |
|  `- 50/9·[99·(n) + -n·y | -99 + y ≥ 0 ∧  -n ≥ 0] + 250000/81·[n^2 | -n ≥ 0]
|
`- [y ≥ 0] · (50/9·[99·(n) + -n·y | -99 + y ≥ 0 ∧  -n ≥ 0] + 250000/81·[n^2 | -n ≥ 0])