ExecutionLog | `- Expected Cost | +- [f] | 0 | +- [Program] | A :~ {1 : I} | B :~ {1 : 0} | Tick(1) | 0:While(C 1 + B) | B :~ {1 : 1 + B} | Tick(1) | 1:If(B C) Then | Skip | Else | Abort | D :~ {1 : C} | E :~ {1 : 0} | Tick(1) | 2:While(D 2 + E) | F :~ {1 : E} | G :~ {1 : 1 + E} | Tick(1) | 3:While(D 1 + G) | NonDet | {sample :~ {1/2 : 0;1/2 : 1} | G :~ {1 : G + sample} | Tick(1)} | {Choice | 1/2: F :~ {1 : G} | G :~ {1 : 1 + G} | 1/2: F :~ {1 : F} | G :~ {1 : G} | Tick(1)} | 4:If(G D) Then | Skip | Else | Abort | E :~ {1 : 1 + E} | H :~ {1 : I} | Tick(1) | 5:If(1 + E D) Then | Skip | Else | Abort | E :~ {1 : 0} | Tick(1) | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | 0:While(C 1 + B) | | B :~ {1 : 1 + B} | | Tick(1) | | | +- While.step | | | | | +- [Problem] | | | 0:While(C 1 + B) | | | B :~ {1 : 1 + B} | | | Tick(1) | | | | | +- [f] | | | 0 | | | | | +- Expected Cost Body | | | | | | | `- [1 | ] | | | | | +- linear-template | | | | | | | `- 1 + [-B + C | -B + C 0] | | | | | +- [Norms] | | | [[1 | ],[-B + C | -B + C 0]] | | | | | +- [Invariant] | | | C 1 + B ==> [1 | ] + h([1 | ],[-1 + -B + C | -1 + -B + C 0]) h([1 | ],[-B + C | -B + C 0]) | | | 1 + B 1 + C ==> 0 h([1 | ],[-B + C | -B + C 0]) | | | | | `- [-B + C | -B + C 0] | | | `- [-B + C | -B + C 0] | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | 1:If(B C) Then | | Skip | | Else | | Abort | | D :~ {1 : C} | | E :~ {1 : 0} | | Tick(1) | | 2:While(D 2 + E) | | F :~ {1 : E} | | G :~ {1 : 1 + E} | | Tick(1) | | 3:While(D 1 + G) | | NonDet | | {sample :~ {1/2 : 0;1/2 : 1} | | G :~ {1 : G + sample} | | Tick(1)} | | {Choice | | 1/2: F :~ {1 : G} | | G :~ {1 : 1 + G} | | 1/2: F :~ {1 : F} | | G :~ {1 : G} | | Tick(1)} | | 4:If(G D) Then | | Skip | | Else | | Abort | | E :~ {1 : 1 + E} | | H :~ {1 : I} | | Tick(1) | | 5:If(1 + E D) Then | | Skip | | Else | | Abort | | E :~ {1 : 0} | | Tick(1) | | | +- Expected Cost | | | | | +- [f] | | | 0 | | | | | +- [Program] | | | 2:While(D 2 + E) | | | F :~ {1 : E} | | | G :~ {1 : 1 + E} | | | Tick(1) | | | 3:While(D 1 + G) | | | NonDet | | | {sample :~ {1/2 : 0;1/2 : 1} | | | G :~ {1 : G + sample} | | | Tick(1)} | | | {Choice | | | 1/2: F :~ {1 : G} | | | G :~ {1 : 1 + G} | | | 1/2: F :~ {1 : F} | | | G :~ {1 : G} | | | Tick(1)} | | | 4:If(G D) Then | | | Skip | | | Else | | | Abort | | | E :~ {1 : 1 + E} | | | H :~ {1 : I} | | | Tick(1) | | | | | +- While.step | | | | | | | +- [Problem] | | | | 2:While(D 2 + E) | | | | F :~ {1 : E} | | | | G :~ {1 : 1 + E} | | | | Tick(1) | | | | 3:While(D 1 + G) | | | | NonDet | | | | {sample :~ {1/2 : 0;1/2 : 1} | | | | G :~ {1 : G + sample} | | | | Tick(1)} | | | | {Choice | | | | 1/2: F :~ {1 : G} | | | | G :~ {1 : 1 + G} | | | | 1/2: F :~ {1 : F} | | | | G :~ {1 : G} | | | | Tick(1)} | | | | 4:If(G D) Then | | | | Skip | | | | Else | | | | Abort | | | | E :~ {1 : 1 + E} | | | | H :~ {1 : I} | | | | Tick(1) | | | | | | | +- [f] | | | | 0 | | | | | | | +- Expected Cost Body | | | | | | | | | +- Expected Cost | | | | | | | | | | | +- [f] | | | | | | 0 | | | | | | | | | | | +- [Program] | | | | | | 3:While(D 1 + G) | | | | | | NonDet | | | | | | {sample :~ {1/2 : 0;1/2 : 1} | | | | | | G :~ {1 : G + sample} | | | | | | Tick(1)} | | | | | | {Choice | | | | | | 1/2: F :~ {1 : G} | | | | | | G :~ {1 : 1 + G} | | | | | | 1/2: F :~ {1 : F} | | | | | | G :~ {1 : G} | | | | | | Tick(1)} | | | | | | | | | | | +- While.step | | | | | | | | | | | | | +- [Problem] | | | | | | | 3:While(D 1 + G) | | | | | | | NonDet | | | | | | | {sample :~ {1/2 : 0;1/2 : 1} | | | | | | | G :~ {1 : G + sample} | | | | | | | Tick(1)} | | | | | | | {Choice | | | | | | | 1/2: F :~ {1 : G} | | | | | | | G :~ {1 : 1 + G} | | | | | | | 1/2: F :~ {1 : F} | | | | | | | G :~ {1 : G} | | | | | | | Tick(1)} | | | | | | | | | | | | | +- [f] | | | | | | | 0 | | | | | | | | | | | | | +- Expected Cost Body | | | | | | | | | | | | | | | `- [1 | ] | | | | | | | | | | | | | +- linear-template | | | | | | | | | | | | | | | `- 1 + [D + -G | D + -G 0] | | | | | | | | | | | | | +- [Norms] | | | | | | | [[1 | ],[D + -G | D + -G 0]] | | | | | | | | | | | | | +- [Invariant] | | | | | | | D 1 + G ==> [1 | ] + h([1 | ],sup(1/2[D + -G | D + -G 0] + 1/2[-1 + D + -G | -1 + D + -G 0],1/2[-1 + D + -G | -1 + D + -G 0] + 1/2[D + -G | D + -G 0])) h([1 | ],[D + -G | D + -G 0]) | | | | | | | 1 + G 1 + D ==> 0 h([1 | ],[D + -G | D + -G 0]) | | | | | | | | | | | | | `- 2[D + -G | D + -G 0] | | | | | | | | | | | `- 2[D + -G | D + -G 0] | | | | | | | | | +- Expected Cost | | | | | | | | | | | +- [f] | | | | | | 0 | | | | | | | | | | | +- [Program] | | | | | | 4:If(G D) Then | | | | | | Skip | | | | | | Else | | | | | | Abort | | | | | | E :~ {1 : 1 + E} | | | | | | H :~ {1 : I} | | | | | | Tick(1) | | | | | | | | | | | `- [G D] [1 | ] | | | | | | | | | +- Expected Cost | | | | | | | | | | | +- [f] | | | | | | [G D] [1 | ] | | | | | | | | | | | +- [Program] | | | | | | 3:While(D 1 + G) | | | | | | NonDet | | | | | | {sample :~ {1/2 : 0;1/2 : 1} | | | | | | G :~ {1 : G + sample} | | | | | | Tick(1)} | | | | | | {Choice | | | | | | 1/2: F :~ {1 : G} | | | | | | G :~ {1 : 1 + G} | | | | | | 1/2: F :~ {1 : F} | | | | | | G :~ {1 : G} | | | | | | Tick(1)} | | | | | | | | | | | +- While.step | | | | | | | | | | | | | +- [Problem] | | | | | | | 3:While(D 1 + G) | | | | | | | NonDet | | | | | | | {sample :~ {1/2 : 0;1/2 : 1} | | | | | | | G :~ {1 : G + sample} | | | | | | | Tick(1)} | | | | | | | {Choice | | | | | | | 1/2: F :~ {1 : G} | | | | | | | G :~ {1 : 1 + G} | | | | | | | 1/2: F :~ {1 : F} | | | | | | | G :~ {1 : G} | | | | | | | Tick(1)} | | | | | | | | | | | | | +- [f] | | | | | | | [G D] [1 | ] | | | | | | | | | | | | | +- linear-template | | | | | | | | | | | | | | | `- 2 + [1 + -D + G | 1 + -D + G 0] + 2([D + -G | D + -G 0]) | | | | | | | | | | | | | +- [Norms] | | | | | | | [[1 | ],[1 + -D + G | 1 + -D + G 0],[D + -G | D + -G 0]] | | | | | | | | | | | | | +- [Invariant] | | | | | | | D 1 + G ==> 0 + h([1 | ],sup(1/2[1 + -D + G | 1 + -D + G 0] + 1/2[2 + -D + G | 2 + -D + G 0],1/2[2 + -D + G | 2 + -D + G 0] + 1/2[1 + -D + G | 1 + -D + G 0]),sup(1/2[D + -G | D + -G 0] + 1/2[-1 + D + -G | -1 + D + -G 0],1/2[-1 + D + -G | -1 + D + -G 0] + 1/2[D + -G | D + -G 0])) h([1 | ],[1 + -D + G | 1 + -D + G 0],[D + -G | D + -G 0]) | | | | | | | 1 + G 1 + D ==> [G D] [1 | ] h([1 | ],[1 + -D + G | 1 + -D + G 0],[D + -G | D + -G 0]) | | | | | | | | | | | | | `- [1 | ] | | | | | | | | | | | `- [1 | ] | | | | | | | | | `- [1 | ] + 2[-1 + D + -E | -1 + D + -E 0] + [1 | ] | | | | | | | +- mixed-iteration-template | | | | | | | | | `- [-1 + D + -E | -1 + D + -E 0] + [-1 + D + -E | -1 + D + -E 0]^2 | | | | | | | +- [Norms] | | | | [[-1 + D + -E | -1 + D + -E 0],[1 + -2(D) + -2(DE) + D^2 + 2(E) + E^2 | -1 + D + -E 0]] | | | | | | | +- While.step | | | | | | | | | +- [Problem] | | | | | 3:While(D 1 + G) | | | | | NonDet | | | | | {sample :~ {1/2 : 0;1/2 : 1} | | | | | G :~ {1 : G + sample} | | | | | Tick(1)} | | | | | {Choice | | | | | 1/2: F :~ {1 : G} | | | | | G :~ {1 : 1 + G} | | | | | 1/2: F :~ {1 : F} | | | | | G :~ {1 : G} | | | | | Tick(1)} | | | | | | | | | +- [f] | | | | | [G D] [4 + -4(D) + -2(DE) + D^2 + 4(E) + E^2 | -2 + D + -E 0] | | | | | | | | | +- linear-template | | | | | | | | | | | `- 1 + [4 + -4(D) + -2(DE) + D^2 + 4(E) + E^2 | -2 + D + -E 0] + [1 + -D + G | 1 + -D + G 0] + 2([D + -G | D + -G 0]) | | | | | | | | | +- [Norms] | | | | | [[1 | ],[4 + -4(D) + -2(DE) + D^2 + 4(E) + E^2 | -2 + D + -E 0],[1 + -D + G | 1 + -D + G 0],[D + -G | D + -G 0]] | | | | | | | | | +- [Invariant] | | | | | D 1 + G ==> 0 + h([1 | ],[4 + -4(D) + -2(DE) + D^2 + 4(E) + E^2 | -2 + D + -E 0],sup(1/2[1 + -D + G | 1 + -D + G 0] + 1/2[2 + -D + G | 2 + -D + G 0],1/2[2 + -D + G | 2 + -D + G 0] + 1/2[1 + -D + G | 1 + -D + G 0]),sup(1/2[D + -G | D + -G 0] + 1/2[-1 + D + -G | -1 + D + -G 0],1/2[-1 + D + -G | -1 + D + -G 0] + 1/2[D + -G | D + -G 0])) h([1 | ],[4 + -4(D) + -2(DE) + D^2 + 4(E) + E^2 | -2 + D + -E 0],[1 + -D + G | 1 + -D + G 0],[D + -G | D + -G 0]) | | | | | 1 + G 1 + D ==> [G D] [4 + -4(D) + -2(DE) + D^2 + 4(E) + E^2 | -2 + D + -E 0] h([1 | ],[4 + -4(D) + -2(DE) + D^2 + 4(E) + E^2 | -2 + D + -E 0],[1 + -D + G | 1 + -D + G 0],[D + -G | D + -G 0]) | | | | | | | | | `- [4 + -4(D) + -2(DE) + D^2 + 4(E) + E^2 | -2 + D + -E 0] | | | | | | | +- [Invariant] | | | | D 2 + E ==> [1 | ] + 2[-1 + D + -E | -1 + D + -E 0] + [1 | ] + h([-2 + D + -E | -2 + D + -E 0],[4 + -4(D) + -2(DE) + D^2 + 4(E) + E^2 | -2 + D + -E 0]) h([-1 + D + -E | -1 + D + -E 0],[1 + -2(D) + -2(DE) + D^2 + 2(E) + E^2 | -1 + D + -E 0]) | | | | 2 + E 1 + D ==> 0 h([-1 + D + -E | -1 + D + -E 0],[1 + -2(D) + -2(DE) + D^2 + 2(E) + E^2 | -1 + D + -E 0]) | | | | | | | `- 3[-1 + D + -E | -1 + D + -E 0] + [1 + -2(D) + -2(DE) + D^2 + 2(E) + E^2 | -1 + D + -E 0] | | | | | `- 3[-1 + D + -E | -1 + D + -E 0] + [1 + -2(D) + -2(DE) + D^2 + 2(E) + E^2 | -1 + D + -E 0] | | | +- Expected Cost | | | | | +- [f] | | | 0 | | | | | +- [Program] | | | 5:If(1 + E D) Then | | | Skip | | | Else | | | Abort | | | E :~ {1 : 0} | | | Tick(1) | | | | | `- [1 + E D] [1 | ] | | | +- Expected Cost | | | | | +- [f] | | | [1 + E D] [1 | ] | | | | | +- [Program] | | | 2:While(D 2 + E) | | | F :~ {1 : E} | | | G :~ {1 : 1 + E} | | | Tick(1) | | | 3:While(D 1 + G) | | | NonDet | | | {sample :~ {1/2 : 0;1/2 : 1} | | | G :~ {1 : G + sample} | | | Tick(1)} | | | {Choice | | | 1/2: F :~ {1 : G} | | | G :~ {1 : 1 + G} | | | 1/2: F :~ {1 : F} | | | G :~ {1 : G} | | | Tick(1)} | | | 4:If(G D) Then | | | Skip | | | Else | | | Abort | | | E :~ {1 : 1 + E} | | | H :~ {1 : I} | | | Tick(1) | | | | | +- While.step | | | | | | | +- [Problem] | | | | 2:While(D 2 + E) | | | | F :~ {1 : E} | | | | G :~ {1 : 1 + E} | | | | Tick(1) | | | | 3:While(D 1 + G) | | | | NonDet | | | | {sample :~ {1/2 : 0;1/2 : 1} | | | | G :~ {1 : G + sample} | | | | Tick(1)} | | | | {Choice | | | | 1/2: F :~ {1 : G} | | | | G :~ {1 : 1 + G} | | | | 1/2: F :~ {1 : F} | | | | G :~ {1 : G} | | | | Tick(1)} | | | | 4:If(G D) Then | | | | Skip | | | | Else | | | | Abort | | | | E :~ {1 : 1 + E} | | | | H :~ {1 : I} | | | | Tick(1) | | | | | | | +- [f] | | | | [1 + E D] [1 | ] | | | | | | | +- linear-template | | | | | | | | | `- 2 + 2([-1 + D + -E | -1 + D + -E 0]) + [2 + -D + E | 2 + -D + E 0] | | | | | | | +- [Norms] | | | | [[1 | ],[-1 + D + -E | -1 + D + -E 0],[2 + -D + E | 2 + -D + E 0]] | | | | | | | +- While.step | | | | | | | | | +- [Problem] | | | | | 3:While(D 1 + G) | | | | | NonDet | | | | | {sample :~ {1/2 : 0;1/2 : 1} | | | | | G :~ {1 : G + sample} | | | | | Tick(1)} | | | | | {Choice | | | | | 1/2: F :~ {1 : G} | | | | | G :~ {1 : 1 + G} | | | | | 1/2: F :~ {1 : F} | | | | | G :~ {1 : G} | | | | | Tick(1)} | | | | | | | | | +- [f] | | | | | [G D] [3 + -D + E | 3 + -D + E 0] | | | | | | | | | +- linear-template | | | | | | | | | | | `- 1 + [1 + -D + G | 1 + -D + G 0] + [3 + -D + E | 3 + -D + E 0] + 2([D + -G | D + -G 0]) | | | | | | | | | +- [Norms] | | | | | [[1 | ],[1 + -D + G | 1 + -D + G 0],[3 + -D + E | 3 + -D + E 0],[D + -G | D + -G 0]] | | | | | | | | | +- [Invariant] | | | | | D 1 + G ==> 0 + h([1 | ],sup(1/2[1 + -D + G | 1 + -D + G 0] + 1/2[2 + -D + G | 2 + -D + G 0],1/2[2 + -D + G | 2 + -D + G 0] + 1/2[1 + -D + G | 1 + -D + G 0]),[3 + -D + E | 3 + -D + E 0],sup(1/2[D + -G | D + -G 0] + 1/2[-1 + D + -G | -1 + D + -G 0],1/2[-1 + D + -G | -1 + D + -G 0] + 1/2[D + -G | D + -G 0])) h([1 | ],[1 + -D + G | 1 + -D + G 0],[3 + -D + E | 3 + -D + E 0],[D + -G | D + -G 0]) | | | | | 1 + G 1 + D ==> [G D] [3 + -D + E | 3 + -D + E 0] h([1 | ],[1 + -D + G | 1 + -D + G 0],[3 + -D + E | 3 + -D + E 0],[D + -G | D + -G 0]) | | | | | | | | | `- [3 + -D + E | 3 + -D + E 0] | | | | | | | +- [Invariant] | | | | D 2 + E ==> 0 + h([1 | ],[-2 + D + -E | -2 + D + -E 0],[3 + -D + E | 3 + -D + E 0]) h([1 | ],[-1 + D + -E | -1 + D + -E 0],[2 + -D + E | 2 + -D + E 0]) | | | | 2 + E 1 + D ==> [1 + E D] [1 | ] h([1 | ],[-1 + D + -E | -1 + D + -E 0],[2 + -D + E | 2 + -D + E 0]) | | | | | | | `- [1 | ] | | | | | `- [1 | ] | | | `- [B C] ([1 | ] + 3[-1 + C | -1 + C 0] + [1 + -2(C) + C^2 | -1 + C 0] + [1 | ]) | +- Expected Cost | | | +- [f] | | [B C] ([1 | ] + 3[-1 + C | -1 + C 0] + [1 + -2(C) + C^2 | -1 + C 0] + [1 | ]) | | | +- [Program] | | 0:While(C 1 + B) | | B :~ {1 : 1 + B} | | Tick(1) | | | +- While.step | | | | | +- [Problem] | | | 0:While(C 1 + B) | | | B :~ {1 : 1 + B} | | | Tick(1) | | | | | +- [f] | | | [B C] ([1 | ] + 3[-1 + C | -1 + C 0] + [1 + -2(C) + C^2 | -1 + C 0] + [1 | ]) | | | | | +- linear-template | | | | | | | `- 3 + [-1 + C | -1 + C 0] + [1 + -2(C) + C^2 | -1 + C 0] + 4([1 + B + -C | 1 + B + -C 0]) + 5([-B + C | -B + C 0]) | | | | | +- [Norms] | | | [[1 | ],[-1 + C | -1 + C 0],[1 + -2(C) + C^2 | -1 + C 0],[1 + B + -C | 1 + B + -C 0],[-B + C | -B + C 0]] | | | | | +- [Invariant] | | | C 1 + B ==> 0 + h([1 | ],[-1 + C | -1 + C 0],[1 + -2(C) + C^2 | -1 + C 0],[2 + B + -C | 2 + B + -C 0],[-1 + -B + C | -1 + -B + C 0]) h([1 | ],[-1 + C | -1 + C 0],[1 + -2(C) + C^2 | -1 + C 0],[1 + B + -C | 1 + B + -C 0],[-B + C | -B + C 0]) | | | 1 + B 1 + C ==> [B C] ([1 | ] + 3[-1 + C | -1 + C 0] + [1 + -2(C) + C^2 | -1 + C 0] + [1 | ]) h([1 | ],[-1 + C | -1 + C 0],[1 + -2(C) + C^2 | -1 + C 0],[1 + B + -C | 1 + B + -C 0],[-B + C | -B + C 0]) | | | | | `- 2 + 3[-1 + C | -1 + C 0] + [1 + -2(C) + C^2 | -1 + C 0] | | | `- 2 + 3[-1 + C | -1 + C 0] + [1 + -2(C) + C^2 | -1 + C 0] | `- [1 | ] + [C | C 0] + 2 + 3[-1 + C | -1 + C 0] + [1 + -2(C) + C^2 | -1 + C 0] [Success] [1 | ] + [C | C 0] + 2 + 3[-1 + C | -1 + C 0] + [1 + -2(C) + C^2 | -1 + C 0] Degree: 2