ExecutionLog | `- Expected Cost | +- [f] | 0 | +- [Program] | i :~ {1 : 1} | j :~ {1 : 0} | 0:While(x 1 + j) | j :~ {1 : 1 + j} | 1:If(i 4) Then | i :~ {1 : 1} | Tick(40) | Else | sample :~ {1/3 : 1;1/3 : 2;1/3 : 3} | i :~ {1 : i + sample} | Tick(1) | +- While.step | | | +- [Problem] | | 0:While(x 1 + j) | | j :~ {1 : 1 + j} | | 1:If(i 4) Then | | i :~ {1 : 1} | | Tick(40) | | Else | | sample :~ {1/3 : 1;1/3 : 2;1/3 : 3} | | i :~ {1 : i + sample} | | Tick(1) | | | +- [f] | | 0 | | | +- Expected Cost Body | | | | | `- ite(i 4,41,[1 | ]) | | | +- linear-template | | | | | `- 3 + [-3 + i | -3 + i 0] + [4 + -i | 4 + -i 0] + [-j + x | -j + x 0] | | | +- [Norms] | | [[1 | ],[-3 + i | -3 + i 0],[4 + -i | 4 + -i 0],[-j + x | -j + x 0]] | | | +- [Invariant] | | x 1 + j ==> ite(i 4,41,[1 | ]) + h([1 | ],ite(i 4,-2,1/3[-2 + i | -2 + i 0] + 1/3[-1 + i | -1 + i 0] + 1/3[i | i 0]),ite(i 4,3,1/3[3 + -i | 3 + -i 0] + 1/3[2 + -i | 2 + -i 0] + 1/3[1 + -i | 1 + -i 0]),[-1 + -j + x | -1 + -j + x 0]) h([1 | ],[-3 + i | -3 + i 0],[4 + -i | 4 + -i 0],[-j + x | -j + x 0]) | | 1 + j 1 + x ==> 0 h([1 | ],[-3 + i | -3 + i 0],[4 + -i | 4 + -i 0],[-j + x | -j + x 0]) | | | `- 41[-j + x | -j + x 0] | `- 41[x | x 0] [Success] 41[x | x 0] Degree: 1