ExecutionLog | `- Expected Cost | +- [f] | 0 | +- [Program] | Tick(5) | 0:If(0 v_x) Then | Tick(1) | Tick(3) | 1:While(0 v_x) | SAMPLE :~ {1/6 : -2;1/6 : -1;1/6 : 0;1/6 : 1;1/6 : 2;1/6 : 3} | v_x :~ {1 : SAMPLE + v_x} | Else | Tick(1) | 2:If(0 v_y) Then | Tick(1) | Tick(3) | 3:While(0 v_x) | SAMPLE :~ {1/6 : -2;1/6 : -1;1/6 : 0;1/6 : 1;1/6 : 2;1/6 : 3} | v_x :~ {1 : SAMPLE + v_x} | Else | Tick(1) | 4:While(v__0 1) | Tick(1) | Tick(1) | v__1 :~ {1 : 1 + v__01} | v_3 :~ {1 : -1 + v__0} | BREAK :~ {1 : 0} | 5:While(1 1 + BREAK v__1 1) | Tick(1) | Tick(1) | Tick(1) | NonDet | {BREAK :~ {1 : 1}} | {Tick(1) | Tick(1) | v_8 :~ {1 : -1 + v__1} | Tick(1) | Tick(1) | v__1 :~ {1 : v_8}} | Tick(1) | v__0 :~ {1 : v_3} | v__01 :~ {1 : v__1} | Tick(1) | v__2 :~ {1 : v__01} | 6:While(v__2 1) | Tick(1) | Tick(1) | v_10 :~ {1 : -1 + v__2} | v_i_0 :~ {1 : 0} | 7:While(v_z 1 + v_i_0) | Tick(1) | Tick(2) | Tick(1) | v_i_0 :~ {1 : 1 + v_i_0} | Tick(1) | v__2 :~ {1 : v_10} | Tick(1) | Tick(1) | 8:While(0 v_x) | SAMPLE :~ {1/6 : -2;1/6 : -1;1/6 : 0;1/6 : 1;1/6 : 2;1/6 : 3} | v_x :~ {1 : SAMPLE + v_x} | Abort | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | 4:While(v__0 1) | | Tick(1) | | Tick(1) | | v__1 :~ {1 : 1 + v__01} | | v_3 :~ {1 : -1 + v__0} | | BREAK :~ {1 : 0} | | 5:While(1 1 + BREAK v__1 1) | | Tick(1) | | Tick(1) | | Tick(1) | | NonDet | | {BREAK :~ {1 : 1}} | | {Tick(1) | | Tick(1) | | v_8 :~ {1 : -1 + v__1} | | Tick(1) | | Tick(1) | | v__1 :~ {1 : v_8}} | | Tick(1) | | v__0 :~ {1 : v_3} | | v__01 :~ {1 : v__1} | | | +- While.step | | | | | +- [Problem] | | | 4:While(v__0 1) | | | Tick(1) | | | Tick(1) | | | v__1 :~ {1 : 1 + v__01} | | | v_3 :~ {1 : -1 + v__0} | | | BREAK :~ {1 : 0} | | | 5:While(1 1 + BREAK v__1 1) | | | Tick(1) | | | Tick(1) | | | Tick(1) | | | NonDet | | | {BREAK :~ {1 : 1}} | | | {Tick(1) | | | Tick(1) | | | v_8 :~ {1 : -1 + v__1} | | | Tick(1) | | | Tick(1) | | | v__1 :~ {1 : v_8}} | | | Tick(1) | | | v__0 :~ {1 : v_3} | | | v__01 :~ {1 : v__1} | | | | | +- [f] | | | 0 | | | | | +- Expected Cost Body | | | | | | | +- Expected Cost | | | | | | | | | +- [f] | | | | | 0 | | | | | | | | | +- [Program] | | | | | 5:While(1 1 + BREAK v__1 1) | | | | | Tick(1) | | | | | Tick(1) | | | | | Tick(1) | | | | | NonDet | | | | | {BREAK :~ {1 : 1}} | | | | | {Tick(1) | | | | | Tick(1) | | | | | v_8 :~ {1 : -1 + v__1} | | | | | Tick(1) | | | | | Tick(1) | | | | | v__1 :~ {1 : v_8}} | | | | | | | | | +- While.step | | | | | | | | | | | +- [Problem] | | | | | | 5:While(1 1 + BREAK v__1 1) | | | | | | Tick(1) | | | | | | Tick(1) | | | | | | Tick(1) | | | | | | NonDet | | | | | | {BREAK :~ {1 : 1}} | | | | | | {Tick(1) | | | | | | Tick(1) | | | | | | v_8 :~ {1 : -1 + v__1} | | | | | | Tick(1) | | | | | | Tick(1) | | | | | | v__1 :~ {1 : v_8}} | | | | | | | | | | | +- [f] | | | | | | 0 | | | | | | | | | | | +- Expected Cost Body | | | | | | | | | | | | | `- 7 | | | | | | | | | | | +- mixed-iteration-template | | | | | | | | | | | | | `- [1 + -BREAK | 1 + -BREAK 0] + 2([1 + -BREAK | 1 + -BREAK 0][v__1 | v__1 0]) + [1 + -BREAK | 1 + -BREAK 0]^2 + [v__1 | v__1 0] + [v__1 | v__1 0]^2 | | | | | | | | | | | +- [Norms] | | | | | | [[1 + -BREAK | 1 + -BREAK 0],[-BREAKv__1 + v__1 | 1 + -BREAK 0 v__1 0],[1 + -2(BREAK) + BREAK^2 | 1 + -BREAK 0],[v__1 | v__1 0],[v__1^2 | v__1 0]] | | | | | | | | | | | +- [Invariant] | | | | | | 1 1 + BREAK v__1 1 ==> 7 + h([1 + -BREAK | 1 + -BREAK 0],[-1 + BREAK + -BREAKv__1 + v__1 | -1 + v__1 0 1 + -BREAK 0],[1 + -2(BREAK) + BREAK^2 | 1 + -BREAK 0],sup([v__1 | v__1 0],[-1 + v__1 | -1 + v__1 0]),sup([v__1^2 | v__1 0],[1 + -2(v__1) + v__1^2 | -1 + v__1 0])) h([1 + -BREAK | 1 + -BREAK 0],[-BREAKv__1 + v__1 | 1 + -BREAK 0 v__1 0],[1 + -2(BREAK) + BREAK^2 | 1 + -BREAK 0],[v__1 | v__1 0],[v__1^2 | v__1 0]) | | | | | | 1 1 + v__1 1 + BREAK 2 ==> 0 h([1 + -BREAK | 1 + -BREAK 0],[-BREAKv__1 + v__1 | 1 + -BREAK 0 v__1 0],[1 + -2(BREAK) + BREAK^2 | 1 + -BREAK 0],[v__1 | v__1 0],[v__1^2 | v__1 0]) | | | | | | | | | | | `- 7[-BREAKv__1 + v__1 | 1 + -BREAK 0 v__1 0] | | | | | | | | | `- 7[-BREAKv__1 + v__1 | 1 + -BREAK 0 v__1 0] | | | | | | | +- Expected Cost | | | | | | | | | +- [f] | | | | | 0 | | | | | | | | | +- [Program] | | | | | Tick(1) | | | | | v__0 :~ {1 : v_3} | | | | | v__01 :~ {1 : v__1} | | | | | | | | | `- [1 | ] | | | | | | | +- Expected Cost | | | | | | | | | +- [f] | | | | | [1 | ] | | | | | | | | | +- [Program] | | | | | 5:While(1 1 + BREAK v__1 1) | | | | | Tick(1) | | | | | Tick(1) | | | | | Tick(1) | | | | | NonDet | | | | | {BREAK :~ {1 : 1}} | | | | | {Tick(1) | | | | | Tick(1) | | | | | v_8 :~ {1 : -1 + v__1} | | | | | Tick(1) | | | | | Tick(1) | | | | | v__1 :~ {1 : v_8}} | | | | | | | | | `- [1 | ] | | | | | | | `- [1 | ] + [1 | ] + 7[1 + v__01 | 1 + v__01 0] + [1 | ] | | | | | +- mixed-lin-template | | | | | | | `- 1 + [1 + v__01 | 1 + v__01 0] + [1 + v__01 | 1 + v__01 0][v__0 | v__0 0] + 2([v__0 | v__0 0]) + [v__0 | v__0 0]^2 | | | | | +- [Norms] | | | [[1 | ],[1 + v__01 | 1 + v__01 0],[v__0 + v__0v__01 | 1 + v__01 0 v__0 0],[v__0 | v__0 0],[v__0^2 | v__0 0]] | | | | | +- While.step | | | | | | | +- [Problem] | | | | 5:While(1 1 + BREAK v__1 1) | | | | Tick(1) | | | | Tick(1) | | | | Tick(1) | | | | NonDet | | | | {BREAK :~ {1 : 1}} | | | | {Tick(1) | | | | Tick(1) | | | | v_8 :~ {1 : -1 + v__1} | | | | Tick(1) | | | | Tick(1) | | | | v__1 :~ {1 : v_8}} | | | | | | | +- [f] | | | | [v_3 + v_3v__1 | 1 + v__1 0 v_3 0] | | | | | | | +- linear-template | | | | | | | | | `- 1 + 2([1 + -BREAK | 1 + -BREAK 0]) + [v_3 + v_3v__1 | 1 + v__1 0 v_3 0] + 2([v__1 | v__1 0]) | | | | | | | +- [Norms] | | | | [[1 | ],[1 + -BREAK | 1 + -BREAK 0],[v_3 + v_3v__1 | 1 + v__1 0 v_3 0],[v__1 | v__1 0]] | | | | | | | +- [Invariant] | | | | 1 1 + BREAK v__1 1 ==> 0 + h([1 | ],[1 + -BREAK | 1 + -BREAK 0],sup([v_3 + v_3v__1 | 1 + v__1 0 v_3 0],[v_3v__1 | v_3 0 v__1 0]),sup([v__1 | v__1 0],[-1 + v__1 | -1 + v__1 0])) h([1 | ],[1 + -BREAK | 1 + -BREAK 0],[v_3 + v_3v__1 | 1 + v__1 0 v_3 0],[v__1 | v__1 0]) | | | | 1 1 + v__1 1 + BREAK 2 ==> [v_3 + v_3v__1 | 1 + v__1 0 v_3 0] h([1 | ],[1 + -BREAK | 1 + -BREAK 0],[v_3 + v_3v__1 | 1 + v__1 0 v_3 0],[v__1 | v__1 0]) | | | | | | | `- [v_3 + v_3v__1 | 1 + v__1 0 v_3 0] | | | | | +- [Invariant] | | | v__0 1 ==> [1 | ] + [1 | ] + 7[1 + v__01 | 1 + v__01 0] + [1 | ] + h([1 | ],[1 | ] + [1 + v__01 | 1 + v__01 0],[-2 + 2(v__0) + v__0v__01 + -v__01 | -1 + v__0 0 2 + v__01 0],[-1 + v__0 | -1 + v__0 0],[1 + -2(v__0) + v__0^2 | -1 + v__0 0]) h([1 | ],[1 + v__01 | 1 + v__01 0],[v__0 + v__0v__01 | 1 + v__01 0 v__0 0],[v__0 | v__0 0],[v__0^2 | v__0 0]) | | | 1 1 + v__0 ==> 0 h([1 | ],[1 + v__01 | 1 + v__01 0],[v__0 + v__0v__01 | 1 + v__01 0 v__0 0],[v__0 | v__0 0],[v__0^2 | v__0 0]) | | | | | `- 1/2[1 + v__01 | 1 + v__01 0] + 7[v__0 + v__0v__01 | 1 + v__01 0 v__0 0] + 7/2[v__0^2 | v__0 0] | | | `- 1/2[1 + v__01 | 1 + v__01 0] + 7[v__0 + v__0v__01 | 1 + v__01 0 v__0 0] + 7/2[v__0^2 | v__0 0] | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | Tick(1) | | v__2 :~ {1 : v__01} | | 6:While(v__2 1) | | Tick(1) | | Tick(1) | | v_10 :~ {1 : -1 + v__2} | | v_i_0 :~ {1 : 0} | | 7:While(v_z 1 + v_i_0) | | Tick(1) | | Tick(2) | | Tick(1) | | v_i_0 :~ {1 : 1 + v_i_0} | | Tick(1) | | v__2 :~ {1 : v_10} | | Tick(1) | | Tick(1) | | 8:While(0 v_x) | | SAMPLE :~ {1/6 : -2;1/6 : -1;1/6 : 0;1/6 : 1;1/6 : 2;1/6 : 3} | | v_x :~ {1 : SAMPLE + v_x} | | Abort | | | +- Expected Cost | | | | | +- [f] | | | 0 | | | | | +- [Program] | | | 6:While(v__2 1) | | | Tick(1) | | | Tick(1) | | | v_10 :~ {1 : -1 + v__2} | | | v_i_0 :~ {1 : 0} | | | 7:While(v_z 1 + v_i_0) | | | Tick(1) | | | Tick(2) | | | Tick(1) | | | v_i_0 :~ {1 : 1 + v_i_0} | | | Tick(1) | | | v__2 :~ {1 : v_10} | | | | | +- While.step | | | | | | | +- [Problem] | | | | 6:While(v__2 1) | | | | Tick(1) | | | | Tick(1) | | | | v_10 :~ {1 : -1 + v__2} | | | | v_i_0 :~ {1 : 0} | | | | 7:While(v_z 1 + v_i_0) | | | | Tick(1) | | | | Tick(2) | | | | Tick(1) | | | | v_i_0 :~ {1 : 1 + v_i_0} | | | | Tick(1) | | | | v__2 :~ {1 : v_10} | | | | | | | +- [f] | | | | 0 | | | | | | | +- Expected Cost Body | | | | | | | | | +- Expected Cost | | | | | | | | | | | +- [f] | | | | | | 0 | | | | | | | | | | | +- [Program] | | | | | | 7:While(v_z 1 + v_i_0) | | | | | | Tick(1) | | | | | | Tick(2) | | | | | | Tick(1) | | | | | | v_i_0 :~ {1 : 1 + v_i_0} | | | | | | | | | | | +- While.step | | | | | | | | | | | | | +- [Problem] | | | | | | | 7:While(v_z 1 + v_i_0) | | | | | | | Tick(1) | | | | | | | Tick(2) | | | | | | | Tick(1) | | | | | | | v_i_0 :~ {1 : 1 + v_i_0} | | | | | | | | | | | | | +- [f] | | | | | | | 0 | | | | | | | | | | | | | +- Expected Cost Body | | | | | | | | | | | | | | | `- 4 | | | | | | | | | | | | | +- linear-template | | | | | | | | | | | | | | | `- 1 + [-v_i_0 + v_z | -v_i_0 + v_z 0] | | | | | | | | | | | | | +- [Norms] | | | | | | | [[1 | ],[-v_i_0 + v_z | -v_i_0 + v_z 0]] | | | | | | | | | | | | | +- [Invariant] | | | | | | | v_z 1 + v_i_0 ==> 4 + h([1 | ],[-1 + -v_i_0 + v_z | -1 + -v_i_0 + v_z 0]) h([1 | ],[-v_i_0 + v_z | -v_i_0 + v_z 0]) | | | | | | | 1 + v_i_0 1 + v_z ==> 0 h([1 | ],[-v_i_0 + v_z | -v_i_0 + v_z 0]) | | | | | | | | | | | | | `- 4[-v_i_0 + v_z | -v_i_0 + v_z 0] | | | | | | | | | | | `- 4[-v_i_0 + v_z | -v_i_0 + v_z 0] | | | | | | | | | +- Expected Cost | | | | | | | | | | | +- [f] | | | | | | 0 | | | | | | | | | | | +- [Program] | | | | | | Tick(1) | | | | | | v__2 :~ {1 : v_10} | | | | | | | | | | | `- [1 | ] | | | | | | | | | +- Expected Cost | | | | | | | | | | | +- [f] | | | | | | [1 | ] | | | | | | | | | | | +- [Program] | | | | | | 7:While(v_z 1 + v_i_0) | | | | | | Tick(1) | | | | | | Tick(2) | | | | | | Tick(1) | | | | | | v_i_0 :~ {1 : 1 + v_i_0} | | | | | | | | | | | `- [1 | ] | | | | | | | | | `- [1 | ] + [1 | ] + 4[v_z | v_z 0] + [1 | ] | | | | | | | +- mixed-lin-template | | | | | | | | | `- 1 + 2([v__2 | v__2 0]) + [v__2 | v__2 0][v_z | v_z 0] + [v__2 | v__2 0]^2 + [v_z | v_z 0] | | | | | | | +- [Norms] | | | | [[1 | ],[v__2 | v__2 0],[v__2v_z | v__2 0 v_z 0],[v__2^2 | v__2 0],[v_z | v_z 0]] | | | | | | | +- [Invariant] | | | | v__2 1 ==> [1 | ] + [1 | ] + 4[v_z | v_z 0] + [1 | ] + h([1 | ],[-1 + v__2 | -1 + v__2 0],[v__2v_z + -v_z | -1 + v__2 0 v_z 0],[1 + -2(v__2) + v__2^2 | -1 + v__2 0],[v_z | v_z 0]) h([1 | ],[v__2 | v__2 0],[v__2v_z | v__2 0 v_z 0],[v__2^2 | v__2 0],[v_z | v_z 0]) | | | | 1 1 + v__2 ==> 0 h([1 | ],[v__2 | v__2 0],[v__2v_z | v__2 0 v_z 0],[v__2^2 | v__2 0],[v_z | v_z 0]) | | | | | | | `- 3[v__2 | v__2 0] + 4[v__2v_z | v__2 0 v_z 0] | | | | | `- 3[v__2 | v__2 0] + 4[v__2v_z | v__2 0 v_z 0] | | | +- Expected Cost | | | | | +- [f] | | | 0 | | | | | +- [Program] | | | Tick(1) | | | Tick(1) | | | 8:While(0 v_x) | | | SAMPLE :~ {1/6 : -2;1/6 : -1;1/6 : 0;1/6 : 1;1/6 : 2;1/6 : 3} | | | v_x :~ {1 : SAMPLE + v_x} | | | Abort | | | | | `- 2 | | | +- Expected Cost | | | | | +- [f] | | | 2 | | | | | +- [Program] | | | 6:While(v__2 1) | | | Tick(1) | | | Tick(1) | | | v_10 :~ {1 : -1 + v__2} | | | v_i_0 :~ {1 : 0} | | | 7:While(v_z 1 + v_i_0) | | | Tick(1) | | | Tick(2) | | | Tick(1) | | | v_i_0 :~ {1 : 1 + v_i_0} | | | Tick(1) | | | v__2 :~ {1 : v_10} | | | | | `- 2 | | | `- [1 | ] + 3[v__01 | v__01 0] + 4[v__01v_z | v__01 0 v_z 0] + 2 | +- Expected Cost | | | +- [f] | | [1 | ] + 3[v__01 | v__01 0] + 4[v__01v_z | v__01 0 v_z 0] + 2 | | | +- [Program] | | 4:While(v__0 1) | | Tick(1) | | Tick(1) | | v__1 :~ {1 : 1 + v__01} | | v_3 :~ {1 : -1 + v__0} | | BREAK :~ {1 : 0} | | 5:While(1 1 + BREAK v__1 1) | | Tick(1) | | Tick(1) | | Tick(1) | | NonDet | | {BREAK :~ {1 : 1}} | | {Tick(1) | | Tick(1) | | v_8 :~ {1 : -1 + v__1} | | Tick(1) | | Tick(1) | | v__1 :~ {1 : v_8}} | | Tick(1) | | v__0 :~ {1 : v_3} | | v__01 :~ {1 : v__1} | | | +- Expected Cost | | | | | +- [f] | | | [1 | ] | | | | | +- [Program] | | | 4:While(v__0 1) | | | Tick(1) | | | Tick(1) | | | v__1 :~ {1 : 1 + v__01} | | | v_3 :~ {1 : -1 + v__0} | | | BREAK :~ {1 : 0} | | | 5:While(1 1 + BREAK v__1 1) | | | Tick(1) | | | Tick(1) | | | Tick(1) | | | NonDet | | | {BREAK :~ {1 : 1}} | | | {Tick(1) | | | Tick(1) | | | v_8 :~ {1 : -1 + v__1} | | | Tick(1) | | | Tick(1) | | | v__1 :~ {1 : v_8}} | | | Tick(1) | | | v__0 :~ {1 : v_3} | | | v__01 :~ {1 : v__1} | | | | | `- [1 | ] | | | +- Expected Cost | | | | | +- [f] | | | 3[v__01 | v__01 0] + 4[v__01v_z | v__01 0 v_z 0] + 2 | | | | | +- [Program] | | | 4:While(v__0 1) | | | Tick(1) | | | Tick(1) | | | v__1 :~ {1 : 1 + v__01} | | | v_3 :~ {1 : -1 + v__0} | | | BREAK :~ {1 : 0} | | | 5:While(1 1 + BREAK v__1 1) | | | Tick(1) | | | Tick(1) | | | Tick(1) | | | NonDet | | | {BREAK :~ {1 : 1}} | | | {Tick(1) | | | Tick(1) | | | v_8 :~ {1 : -1 + v__1} | | | Tick(1) | | | Tick(1) | | | v__1 :~ {1 : v_8}} | | | Tick(1) | | | v__0 :~ {1 : v_3} | | | v__01 :~ {1 : v__1} | | | | | +- Expected Cost | | | | | | | +- [f] | | | | 3[v__01 | v__01 0] + 4[v__01v_z | v__01 0 v_z 0] | | | | | | | +- [Program] | | | | 4:While(v__0 1) | | | | Tick(1) | | | | Tick(1) | | | | v__1 :~ {1 : 1 + v__01} | | | | v_3 :~ {1 : -1 + v__0} | | | | BREAK :~ {1 : 0} | | | | 5:While(1 1 + BREAK v__1 1) | | | | Tick(1) | | | | Tick(1) | | | | Tick(1) | | | | NonDet | | | | {BREAK :~ {1 : 1}} | | | | {Tick(1) | | | | Tick(1) | | | | v_8 :~ {1 : -1 + v__1} | | | | Tick(1) | | | | Tick(1) | | | | v__1 :~ {1 : v_8}} | | | | Tick(1) | | | | v__0 :~ {1 : v_3} | | | | v__01 :~ {1 : v__1} | | | | | | | +- Expected Cost | | | | | | | | | +- [f] | | | | | 3[v__01 | v__01 0] | | | | | | | | | +- [Program] | | | | | 4:While(v__0 1) | | | | | Tick(1) | | | | | Tick(1) | | | | | v__1 :~ {1 : 1 + v__01} | | | | | v_3 :~ {1 : -1 + v__0} | | | | | BREAK :~ {1 : 0} | | | | | 5:While(1 1 + BREAK v__1 1) | | | | | Tick(1) | | | | | Tick(1) | | | | | Tick(1) | | | | | NonDet | | | | | {BREAK :~ {1 : 1}} | | | | | {Tick(1) | | | | | Tick(1) | | | | | v_8 :~ {1 : -1 + v__1} | | | | | Tick(1) | | | | | Tick(1) | | | | | v__1 :~ {1 : v_8}} | | | | | Tick(1) | | | | | v__0 :~ {1 : v_3} | | | | | v__01 :~ {1 : v__1} | | | | | | | | | +- While.step | | | | | | | | | | | +- [Problem] | | | | | | 4:While(v__0 1) | | | | | | Tick(1) | | | | | | Tick(1) | | | | | | v__1 :~ {1 : 1 + v__01} | | | | | | v_3 :~ {1 : -1 + v__0} | | | | | | BREAK :~ {1 : 0} | | | | | | 5:While(1 1 + BREAK v__1 1) | | | | | | Tick(1) | | | | | | Tick(1) | | | | | | Tick(1) | | | | | | NonDet | | | | | | {BREAK :~ {1 : 1}} | | | | | | {Tick(1) | | | | | | Tick(1) | | | | | | v_8 :~ {1 : -1 + v__1} | | | | | | Tick(1) | | | | | | Tick(1) | | | | | | v__1 :~ {1 : v_8}} | | | | | | Tick(1) | | | | | | v__0 :~ {1 : v_3} | | | | | | v__01 :~ {1 : v__1} | | | | | | | | | | | +- [f] | | | | | | 3[v__01 | v__01 0] | | | | | | | | | | | +- While.step | | | | | | | | | | | | | +- [Problem] | | | | | | | 5:While(1 1 + BREAK v__1 1) | | | | | | | Tick(1) | | | | | | | Tick(1) | | | | | | | Tick(1) | | | | | | | NonDet | | | | | | | {BREAK :~ {1 : 1}} | | | | | | | {Tick(1) | | | | | | | Tick(1) | | | | | | | v_8 :~ {1 : -1 + v__1} | | | | | | | Tick(1) | | | | | | | Tick(1) | | | | | | | v__1 :~ {1 : v_8}} | | | | | | | | | | | | | +- [f] | | | | | | | [v__1 | v__1 0] | | | | | | | | | | | | | +- linear-template | | | | | | | | | | | | | | | `- 1 + 2([1 + -BREAK | 1 + -BREAK 0]) + 3([v__1 | v__1 0]) | | | | | | | | | | | | | +- [Norms] | | | | | | | [[1 | ],[1 + -BREAK | 1 + -BREAK 0],[v__1 | v__1 0]] | | | | | | | | | | | | | +- [Invariant] | | | | | | | 1 1 + BREAK v__1 1 ==> 0 + h([1 | ],[1 + -BREAK | 1 + -BREAK 0],sup([v__1 | v__1 0],[-1 + v__1 | -1 + v__1 0])) h([1 | ],[1 + -BREAK | 1 + -BREAK 0],[v__1 | v__1 0]) | | | | | | | 1 1 + v__1 1 + BREAK 2 ==> [v__1 | v__1 0] h([1 | ],[1 + -BREAK | 1 + -BREAK 0],[v__1 | v__1 0]) | | | | | | | | | | | | | `- [v__1 | v__1 0] | | | | | | | | | | | +- linear-template | | | | | | | | | | | | | `- 1 + 2([v__0 | v__0 0]) + [v__01 | v__01 0] | | | | | | | | | | | +- [Norms] | | | | | | [[1 | ],[v__0 | v__0 0],[v__01 | v__01 0]] | | | | | | | | | | | +- [Invariant] | | | | | | v__0 1 ==> 0 + h([1 | ],[-1 + v__0 | -1 + v__0 0],[1 + v__01 | 1 + v__01 0]) h([1 | ],[v__0 | v__0 0],[v__01 | v__01 0]) | | | | | | 1 1 + v__0 ==> 3[v__01 | v__01 0] h([1 | ],[v__0 | v__0 0],[v__01 | v__01 0]) | | | | | | | | | | | `- 3[v__0 | v__0 0] + 3[v__01 | v__01 0] | | | | | | | | | `- 3[v__0 | v__0 0] + 3[v__01 | v__01 0] | | | | | | | +- Expected Cost | | | | | | | | | +- [f] | | | | | 4[v__01v_z | v__01 0 v_z 0] | | | | | | | | | +- [Program] | | | | | 4:While(v__0 1) | | | | | Tick(1) | | | | | Tick(1) | | | | | v__1 :~ {1 : 1 + v__01} | | | | | v_3 :~ {1 : -1 + v__0} | | | | | BREAK :~ {1 : 0} | | | | | 5:While(1 1 + BREAK v__1 1) | | | | | Tick(1) | | | | | Tick(1) | | | | | Tick(1) | | | | | NonDet | | | | | {BREAK :~ {1 : 1}} | | | | | {Tick(1) | | | | | Tick(1) | | | | | v_8 :~ {1 : -1 + v__1} | | | | | Tick(1) | | | | | Tick(1) | | | | | v__1 :~ {1 : v_8}} | | | | | Tick(1) | | | | | v__0 :~ {1 : v_3} | | | | | v__01 :~ {1 : v__1} | | | | | | | | | +- While.step | | | | | | | | | | | +- [Problem] | | | | | | 4:While(v__0 1) | | | | | | Tick(1) | | | | | | Tick(1) | | | | | | v__1 :~ {1 : 1 + v__01} | | | | | | v_3 :~ {1 : -1 + v__0} | | | | | | BREAK :~ {1 : 0} | | | | | | 5:While(1 1 + BREAK v__1 1) | | | | | | Tick(1) | | | | | | Tick(1) | | | | | | Tick(1) | | | | | | NonDet | | | | | | {BREAK :~ {1 : 1}} | | | | | | {Tick(1) | | | | | | Tick(1) | | | | | | v_8 :~ {1 : -1 + v__1} | | | | | | Tick(1) | | | | | | Tick(1) | | | | | | v__1 :~ {1 : v_8}} | | | | | | Tick(1) | | | | | | v__0 :~ {1 : v_3} | | | | | | v__01 :~ {1 : v__1} | | | | | | | | | | | +- [f] | | | | | | 4[v__01v_z | v__01 0 v_z 0] | | | | | | | | | | | +- While.step | | | | | | | | | | | | | +- [Problem] | | | | | | | 5:While(1 1 + BREAK v__1 1) | | | | | | | Tick(1) | | | | | | | Tick(1) | | | | | | | Tick(1) | | | | | | | NonDet | | | | | | | {BREAK :~ {1 : 1}} | | | | | | | {Tick(1) | | | | | | | Tick(1) | | | | | | | v_8 :~ {1 : -1 + v__1} | | | | | | | Tick(1) | | | | | | | Tick(1) | | | | | | | v__1 :~ {1 : v_8}} | | | | | | | | | | | | | +- [f] | | | | | | | [v__1v_z | v__1 0 v_z 0] | | | | | | | | | | | | | +- linear-template | | | | | | | | | | | | | | | `- 1 + 2([1 + -BREAK | 1 + -BREAK 0]) + 2([v__1 | v__1 0]) + [v__1v_z | v__1 0 v_z 0] | | | | | | | | | | | | | +- [Norms] | | | | | | | [[1 | ],[1 + -BREAK | 1 + -BREAK 0],[v__1 | v__1 0],[v__1v_z | v__1 0 v_z 0]] | | | | | | | | | | | | | +- [Invariant] | | | | | | | 1 1 + BREAK v__1 1 ==> 0 + h([1 | ],[1 + -BREAK | 1 + -BREAK 0],sup([v__1 | v__1 0],[-1 + v__1 | -1 + v__1 0]),sup([v__1v_z | v__1 0 v_z 0],[v__1v_z + -v_z | -1 + v__1 0 v_z 0])) h([1 | ],[1 + -BREAK | 1 + -BREAK 0],[v__1 | v__1 0],[v__1v_z | v__1 0 v_z 0]) | | | | | | | 1 1 + v__1 1 + BREAK 2 ==> [v__1v_z | v__1 0 v_z 0] h([1 | ],[1 + -BREAK | 1 + -BREAK 0],[v__1 | v__1 0],[v__1v_z | v__1 0 v_z 0]) | | | | | | | | | | | | | `- [v__1v_z | v__1 0 v_z 0] | | | | | | | | | | | +- linear-template | | | | | | | | | | | | | `- 1 + [v__0 | v__0 0] + [v__0 | v__0 0][v_z | v_z 0] + [v__01v_z | v__01 0 v_z 0] | | | | | | | | | | | +- [Norms] | | | | | | [[1 | ],[v__0 | v__0 0],[v__0v_z | v__0 0 v_z 0],[v__01v_z | v__01 0 v_z 0]] | | | | | | | | | | | +- [Invariant] | | | | | | v__0 1 ==> 0 + h([1 | ],[-1 + v__0 | -1 + v__0 0],[v__0v_z + -v_z | -1 + v__0 0 v_z 0],[v__01v_z + v_z | 1 + v__01 0 v_z 0]) h([1 | ],[v__0 | v__0 0],[v__0v_z | v__0 0 v_z 0],[v__01v_z | v__01 0 v_z 0]) | | | | | | 1 1 + v__0 ==> 4[v__01v_z | v__01 0 v_z 0] h([1 | ],[v__0 | v__0 0],[v__0v_z | v__0 0 v_z 0],[v__01v_z | v__01 0 v_z 0]) | | | | | | | | | | | `- 4[v__0v_z | v__0 0 v_z 0] + 4[v__01v_z | v__01 0 v_z 0] | | | | | | | | | `- 4[v__0v_z | v__0 0 v_z 0] + 4[v__01v_z | v__01 0 v_z 0] | | | | | | | `- 3[v__0 | v__0 0] + 3[v__01 | v__01 0] + 4[v__0v_z | v__0 0 v_z 0] + 4[v__01v_z | v__01 0 v_z 0] | | | | | +- Expected Cost | | | | | | | +- [f] | | | | 2 | | | | | | | +- [Program] | | | | 4:While(v__0 1) | | | | Tick(1) | | | | Tick(1) | | | | v__1 :~ {1 : 1 + v__01} | | | | v_3 :~ {1 : -1 + v__0} | | | | BREAK :~ {1 : 0} | | | | 5:While(1 1 + BREAK v__1 1) | | | | Tick(1) | | | | Tick(1) | | | | Tick(1) | | | | NonDet | | | | {BREAK :~ {1 : 1}} | | | | {Tick(1) | | | | Tick(1) | | | | v_8 :~ {1 : -1 + v__1} | | | | Tick(1) | | | | Tick(1) | | | | v__1 :~ {1 : v_8}} | | | | Tick(1) | | | | v__0 :~ {1 : v_3} | | | | v__01 :~ {1 : v__1} | | | | | | | `- 2 | | | | | `- 3[v__0 | v__0 0] + 3[v__01 | v__01 0] + 4[v__0v_z | v__0 0 v_z 0] + 4[v__01v_z | v__01 0 v_z 0] + 2 | | | `- [1 | ] + 3[v__0 | v__0 0] + 3[v__01 | v__01 0] + 4[v__0v_z | v__0 0 v_z 0] + 4[v__01v_z | v__01 0 v_z 0] + 2 | `- 5 + ite(0 v_x,4,[1 | ] + ite(0 v_y,4,[1 | ] + 1/2[1 + v__01 | 1 + v__01 0] + 7[v__0 + v__0v__01 | 1 + v__01 0 v__0 0] + 7/2[v__0^2 | v__0 0] + [1 | ] + 3[v__0 | v__0 0] + 3[v__01 | v__01 0] + 4[v__0v_z | v__0 0 v_z 0] + 4[v__01v_z | v__01 0 v_z 0] + 2)) [Success] 5 + ite(0 v_x ,4 ,[1 | ] + ite(0 v_y ,4 ,[1 | ] + 1/2[1 + v__01 | 1 + v__01 0] + 7[v__0 + v__0v__01 | 1 + v__01 0 v__0 0] + 7/2[v__0^2 | v__0 0] + [1 | ] + 3[v__0 | v__0 0] + 3[v__01 | v__01 0] + 4[v__0v_z | v__0 0 v_z 0] + 4[v__01v_z | v__01 0 v_z 0] + 2)) Degree: 2