ExecutionLog | `- Expected Cost | +- [f] | 0 | +- [Program] | 0:If(y 10) Then | Skip | Else | Abort | 1:While(x + -y 3) | sample :~ {1/3 : 1;1/3 : 2;1/3 : 3} | y :~ {1 : sample + y} | Tick(3) | 2:While(y 10) | Choice | 2/3: y :~ {1 : -10 + y} | 1/3: y :~ {1 : y} | Tick(1) | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | 1:While(x + -y 3) | | sample :~ {1/3 : 1;1/3 : 2;1/3 : 3} | | y :~ {1 : sample + y} | | Tick(3) | | | +- While.step | | | | | +- [Problem] | | | 1:While(x + -y 3) | | | sample :~ {1/3 : 1;1/3 : 2;1/3 : 3} | | | y :~ {1 : sample + y} | | | Tick(3) | | | | | +- [f] | | | 0 | | | | | +- Expected Cost Body | | | | | | | `- 3 | | | | | +- linear-template | | | | | | | `- 1 + [-2 + x + -y | -2 + x + -y 0] | | | | | +- [Norms] | | | [[1 | ],[-2 + x + -y | -2 + x + -y 0]] | | | | | +- [Invariant] | | | x + -y 3 ==> 3 + h([1 | ],1/3[-3 + x + -y | -3 + x + -y 0] + 1/3[-4 + x + -y | -4 + x + -y 0] + 1/3[-5 + x + -y | -5 + x + -y 0]) h([1 | ],[-2 + x + -y | -2 + x + -y 0]) | | | 3 1 + x + -y ==> 0 h([1 | ],[-2 + x + -y | -2 + x + -y 0]) | | | | | `- 3[-2 + x + -y | -2 + x + -y 0] | | | `- 3[-2 + x + -y | -2 + x + -y 0] | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | 2:While(y 10) | | Choice | | 2/3: y :~ {1 : -10 + y} | | 1/3: y :~ {1 : y} | | Tick(1) | | | +- While.step | | | | | +- [Problem] | | | 2:While(y 10) | | | Choice | | | 2/3: y :~ {1 : -10 + y} | | | 1/3: y :~ {1 : y} | | | Tick(1) | | | | | +- [f] | | | 0 | | | | | +- Expected Cost Body | | | | | | | `- [1 | ] | | | | | +- linear-template | | | | | | | `- 1 + [-9 + y | -9 + y 0] | | | | | +- [Norms] | | | [[1 | ],[-9 + y | -9 + y 0]] | | | | | +- [Invariant] | | | y 10 ==> [1 | ] + h([1 | ],2/3[-19 + y | -19 + y 0] + 1/3[-9 + y | -9 + y 0]) h([1 | ],[-9 + y | -9 + y 0]) | | | 10 1 + y ==> 0 h([1 | ],[-9 + y | -9 + y 0]) | | | | | `- 3/2[-9 + y | -9 + y 0] | | | `- 3/2[-9 + y | -9 + y 0] | +- Expected Cost | | | +- [f] | | 3/2[-9 + y | -9 + y 0] | | | +- [Program] | | 1:While(x + -y 3) | | sample :~ {1/3 : 1;1/3 : 2;1/3 : 3} | | y :~ {1 : sample + y} | | Tick(3) | | | +- While.step | | | | | +- [Problem] | | | 1:While(x + -y 3) | | | sample :~ {1/3 : 1;1/3 : 2;1/3 : 3} | | | y :~ {1 : sample + y} | | | Tick(3) | | | | | +- [f] | | | 3/2[-9 + y | -9 + y 0] | | | | | +- linear-template | | | | | | | `- 1 + [-9 + y | -9 + y 0] + 2([-2 + x + -y | -2 + x + -y 0]) | | | | | +- [Norms] | | | [[1 | ],[-9 + y | -9 + y 0],[-2 + x + -y | -2 + x + -y 0]] | | | | | +- [Invariant] | | | x + -y 3 ==> 0 + h([1 | ],1/3[-8 + y | -8 + y 0] + 1/3[-7 + y | -7 + y 0] + 1/3[-6 + y | -6 + y 0],1/3[-3 + x + -y | -3 + x + -y 0] + 1/3[-4 + x + -y | -4 + x + -y 0] + 1/3[-5 + x + -y | -5 + x + -y 0]) h([1 | ],[-9 + y | -9 + y 0],[-2 + x + -y | -2 + x + -y 0]) | | | 3 1 + x + -y ==> 3/2[-9 + y | -9 + y 0] h([1 | ],[-9 + y | -9 + y 0],[-2 + x + -y | -2 + x + -y 0]) | | | | | `- 3/2[-9 + y | -9 + y 0] + 3[-2 + x + -y | -2 + x + -y 0] | | | `- 3/2[-9 + y | -9 + y 0] + 3[-2 + x + -y | -2 + x + -y 0] | `- [y 10] (3[-2 + x + -y | -2 + x + -y 0] + 3/2[-9 + y | -9 + y 0] + 3[-2 + x + -y | -2 + x + -y 0]) [Success] [y 10] (3[-2 + x + -y | -2 + x + -y 0] + 3/2[-9 + y | -9 + y 0] + 3[-2 + x + -y | -2 + x + -y 0]) Degree: 1