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