ExecutionLog
|
`- 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)
   |          y :~ {1 : 1000 + y}}
   |          {Skip}
   |
   +- 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)
   |  |          y :~ {1 : 1000 + y}}
   |  |          {Skip}
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- Expected Cost Body
   |  |  |
   |  |  +- Expected Cost
   |  |  |  |
   |  |  |  +- [f]
   |  |  |  |    0
   |  |  |  |
   |  |  |  +- [Program]
   |  |  |  |    2:While(y  100)
   |  |  |  |        Choice
   |  |  |  |          1/2: y :~ {1 : -100 + y}
   |  |  |  |          1/2: y :~ {1 : -90 + y}
   |  |  |  |        Tick(5)
   |  |  |  |
   |  |  |  +- 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]
   |  |  |  |    2:While(y  100)
   |  |  |  |        Choice
   |  |  |  |          1/2: y :~ {1 : -100 + y}
   |  |  |  |          1/2: y :~ {1 : -90 + y}
   |  |  |  |        Tick(5)
   |  |  |  |
   |  |  |  `- 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) + -ny | -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) + -ny | 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) + -ny | 901 + y  0   -n  0]
   |  |  |
   |  |  +- [Norms]
   |  |  |    [[1 | ],[-99 + y | -99 + y  0],[-9900(n) + 100(ny) | -99 + y  0   100(n)  0],[-901(n) + -ny | 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) + ny | -199 + y  0   100(n)  0] + 50[-189(n) + ny | -189 + y  0   100(n)  0],1/2[-801(n) + -ny | 801 + y  0   -n  0] + 1/2[-811(n) + -ny | 811 + y  0   -n  0])  h([1 | ],[-99 + y | -99 + y  0],[-9900(n) + 100(ny) | -99 + y  0   100(n)  0],[-901(n) + -ny | 901 + y  0   -n  0])
   |  |  |    100  1 + y ==> [-901(n) + -ny | 901 + y  0   -n  0]  h([1 | ],[-99 + y | -99 + y  0],[-9900(n) + 100(ny) | -99 + y  0   100(n)  0],[-901(n) + -ny | 901 + y  0   -n  0])
   |  |  |
   |  |  `- [-901(n) + -ny | 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[-99 + y | -99 + y  0]) + sup(100,1/10[-99 + y | -99 + y  0]),sup(9/10[-901 + -901(n) + -ny + -y | -1 + -n  0   901 + y  0],9/10[99 + 99(n) + -ny + -y | -99 + y  0   -1 + -n  0]) + sup(1/10[-901(n) + -ny | 901 + y  0   -n  0],1/10[99(n) + -ny | -99 + 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) + -ny | -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) + -ny | -99 + y  0   -n  0],[-n | -n  0],[n^2 | -n  0])
   |  |
   |  `- 50/9[99(n) + -ny | -99 + y  0   -n  0] + 250000/81[n^2 | -n  0]
   |
   `- [y  0]  (50/9[99(n) + -ny | -99 + y  0   -n  0] + 250000/81[n^2 | -n  0])

[Success] [y  0]
            (50/9[99(n) + -ny | -99 + y
                     0   -n  0] + 250000/81[n^2
                                                | -n  0])
Degree: 2