ExecutionLog | `- Expected Cost | +- [f] | 0 | +- [Program] | Tick(1) | A :~ {1 : 0} | D :~ {1 : 0} | 0:While(E 1 + D) | Tick(1) | Choice | 3/4: D :~ {1 : 1 + D} | 1/4: D :~ {1 : -1 + D} | Tick(1) | F :~ {1 : 0} | 1:While(E 1 + F) | Tick(1) | Choice | 3/4: F :~ {1 : 1 + F} | 1/4: F :~ {1 : -1 + F} | Tick(1) | G :~ {1 : 0} | 2:While(E 1 + G) | Tick(1) | Choice | 3/4: G :~ {1 : 1 + G} | 1/4: G :~ {1 : -1 + G} | Tick(1) | A :~ {1 : 0} | 3:While(E 1 + A) | Tick(1) | Choice | 3/4: A :~ {1 : 1 + A} | 1/4: A :~ {1 : -1 + A} | Tick(1) | H :~ {1 : 0} | 4:While(E 1 + H) | Tick(1) | Choice | 3/4: H :~ {1 : 1 + H} | 1/4: H :~ {1 : -1 + H} | Tick(1) | I :~ {1 : 0} | 5:While(E 1 + I) | Tick(1) | Choice | 3/4: I :~ {1 : 1 + I} | 1/4: I :~ {1 : -1 + I} | Tick(1) | J :~ {1 : 0} | 6:While(E 1 + J) | Choice | 3/4: J :~ {1 : 1 + J} | 1/4: J :~ {1 : -1 + J} | Tick(1) | A :~ {1 : 0} | 7:While(E 1 + A) | Tick(1) | Choice | 3/4: A :~ {1 : 1 + A} | 1/4: A :~ {1 : -1 + A} | Tick(1) | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | 0:While(E 1 + D) | | Tick(1) | | Choice | | 3/4: D :~ {1 : 1 + D} | | 1/4: D :~ {1 : -1 + D} | | | +- While.step | | | | | +- [Problem] | | | 0:While(E 1 + D) | | | Tick(1) | | | Choice | | | 3/4: D :~ {1 : 1 + D} | | | 1/4: D :~ {1 : -1 + D} | | | | | +- [f] | | | 0 | | | | | +- Expected Cost Body | | | | | | | `- [1 | ] | | | | | +- linear-template | | | | | | | `- 1 + [-D + E | -D + E 0] | | | | | +- [Norms] | | | [[1 | ],[-D + E | -D + E 0]] | | | | | +- [Invariant] | | | E 1 + D ==> [1 | ] + h([1 | ],3/4[-1 + -D + E | -1 + -D + E 0] + 1/4[1 + -D + E | 1 + -D + E 0]) h([1 | ],[-D + E | -D + E 0]) | | | 1 + D 1 + E ==> 0 h([1 | ],[-D + E | -D + E 0]) | | | | | `- 2[-D + E | -D + E 0] | | | `- 2[-D + E | -D + E 0] | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | Tick(1) | | F :~ {1 : 0} | | 1:While(E 1 + F) | | Tick(1) | | Choice | | 3/4: F :~ {1 : 1 + F} | | 1/4: F :~ {1 : -1 + F} | | Tick(1) | | G :~ {1 : 0} | | 2:While(E 1 + G) | | Tick(1) | | Choice | | 3/4: G :~ {1 : 1 + G} | | 1/4: G :~ {1 : -1 + G} | | Tick(1) | | A :~ {1 : 0} | | 3:While(E 1 + A) | | Tick(1) | | Choice | | 3/4: A :~ {1 : 1 + A} | | 1/4: A :~ {1 : -1 + A} | | Tick(1) | | H :~ {1 : 0} | | 4:While(E 1 + H) | | Tick(1) | | Choice | | 3/4: H :~ {1 : 1 + H} | | 1/4: H :~ {1 : -1 + H} | | Tick(1) | | I :~ {1 : 0} | | 5:While(E 1 + I) | | Tick(1) | | Choice | | 3/4: I :~ {1 : 1 + I} | | 1/4: I :~ {1 : -1 + I} | | Tick(1) | | J :~ {1 : 0} | | 6:While(E 1 + J) | | Choice | | 3/4: J :~ {1 : 1 + J} | | 1/4: J :~ {1 : -1 + J} | | Tick(1) | | A :~ {1 : 0} | | 7:While(E 1 + A) | | Tick(1) | | Choice | | 3/4: A :~ {1 : 1 + A} | | 1/4: A :~ {1 : -1 + A} | | Tick(1) | | | +- Expected Cost | | | | | +- [f] | | | 0 | | | | | +- [Program] | | | 1:While(E 1 + F) | | | Tick(1) | | | Choice | | | 3/4: F :~ {1 : 1 + F} | | | 1/4: F :~ {1 : -1 + F} | | | | | +- While.step | | | | | | | +- [Problem] | | | | 1:While(E 1 + F) | | | | Tick(1) | | | | Choice | | | | 3/4: F :~ {1 : 1 + F} | | | | 1/4: F :~ {1 : -1 + F} | | | | | | | +- [f] | | | | 0 | | | | | | | +- Expected Cost Body | | | | | | | | | `- [1 | ] | | | | | | | +- linear-template | | | | | | | | | `- 1 + [E + -F | E + -F 0] | | | | | | | +- [Norms] | | | | [[1 | ],[E + -F | E + -F 0]] | | | | | | | +- [Invariant] | | | | E 1 + F ==> [1 | ] + h([1 | ],3/4[-1 + E + -F | -1 + E + -F 0] + 1/4[1 + E + -F | 1 + E + -F 0]) h([1 | ],[E + -F | E + -F 0]) | | | | 1 + F 1 + E ==> 0 h([1 | ],[E + -F | E + -F 0]) | | | | | | | `- 2[E + -F | E + -F 0] | | | | | `- 2[E + -F | E + -F 0] | | | +- Expected Cost | | | | | +- [f] | | | 0 | | | | | +- [Program] | | | Tick(1) | | | G :~ {1 : 0} | | | 2:While(E 1 + G) | | | Tick(1) | | | Choice | | | 3/4: G :~ {1 : 1 + G} | | | 1/4: G :~ {1 : -1 + G} | | | Tick(1) | | | A :~ {1 : 0} | | | 3:While(E 1 + A) | | | Tick(1) | | | Choice | | | 3/4: A :~ {1 : 1 + A} | | | 1/4: A :~ {1 : -1 + A} | | | Tick(1) | | | H :~ {1 : 0} | | | 4:While(E 1 + H) | | | Tick(1) | | | Choice | | | 3/4: H :~ {1 : 1 + H} | | | 1/4: H :~ {1 : -1 + H} | | | Tick(1) | | | I :~ {1 : 0} | | | 5:While(E 1 + I) | | | Tick(1) | | | Choice | | | 3/4: I :~ {1 : 1 + I} | | | 1/4: I :~ {1 : -1 + I} | | | Tick(1) | | | J :~ {1 : 0} | | | 6:While(E 1 + J) | | | Choice | | | 3/4: J :~ {1 : 1 + J} | | | 1/4: J :~ {1 : -1 + J} | | | Tick(1) | | | A :~ {1 : 0} | | | 7:While(E 1 + A) | | | Tick(1) | | | Choice | | | 3/4: A :~ {1 : 1 + A} | | | 1/4: A :~ {1 : -1 + A} | | | Tick(1) | | | | | +- Expected Cost | | | | | | | +- [f] | | | | 0 | | | | | | | +- [Program] | | | | 2:While(E 1 + G) | | | | Tick(1) | | | | Choice | | | | 3/4: G :~ {1 : 1 + G} | | | | 1/4: G :~ {1 : -1 + G} | | | | | | | +- While.step | | | | | | | | | +- [Problem] | | | | | 2:While(E 1 + G) | | | | | Tick(1) | | | | | Choice | | | | | 3/4: G :~ {1 : 1 + G} | | | | | 1/4: G :~ {1 : -1 + G} | | | | | | | | | +- [f] | | | | | 0 | | | | | | | | | +- Expected Cost Body | | | | | | | | | | | `- [1 | ] | | | | | | | | | +- linear-template | | | | | | | | | | | `- 1 + [E + -G | E + -G 0] | | | | | | | | | +- [Norms] | | | | | [[1 | ],[E + -G | E + -G 0]] | | | | | | | | | +- [Invariant] | | | | | E 1 + G ==> [1 | ] + h([1 | ],3/4[-1 + E + -G | -1 + E + -G 0] + 1/4[1 + E + -G | 1 + E + -G 0]) h([1 | ],[E + -G | E + -G 0]) | | | | | 1 + G 1 + E ==> 0 h([1 | ],[E + -G | E + -G 0]) | | | | | | | | | `- 2[E + -G | E + -G 0] | | | | | | | `- 2[E + -G | E + -G 0] | | | | | +- Expected Cost | | | | | | | +- [f] | | | | 0 | | | | | | | +- [Program] | | | | Tick(1) | | | | A :~ {1 : 0} | | | | 3:While(E 1 + A) | | | | Tick(1) | | | | Choice | | | | 3/4: A :~ {1 : 1 + A} | | | | 1/4: A :~ {1 : -1 + A} | | | | Tick(1) | | | | H :~ {1 : 0} | | | | 4:While(E 1 + H) | | | | Tick(1) | | | | Choice | | | | 3/4: H :~ {1 : 1 + H} | | | | 1/4: H :~ {1 : -1 + H} | | | | Tick(1) | | | | I :~ {1 : 0} | | | | 5:While(E 1 + I) | | | | Tick(1) | | | | Choice | | | | 3/4: I :~ {1 : 1 + I} | | | | 1/4: I :~ {1 : -1 + I} | | | | Tick(1) | | | | J :~ {1 : 0} | | | | 6:While(E 1 + J) | | | | Choice | | | | 3/4: J :~ {1 : 1 + J} | | | | 1/4: J :~ {1 : -1 + J} | | | | Tick(1) | | | | A :~ {1 : 0} | | | | 7:While(E 1 + A) | | | | Tick(1) | | | | Choice | | | | 3/4: A :~ {1 : 1 + A} | | | | 1/4: A :~ {1 : -1 + A} | | | | Tick(1) | | | | | | | +- Expected Cost | | | | | | | | | +- [f] | | | | | 0 | | | | | | | | | +- [Program] | | | | | 3:While(E 1 + A) | | | | | Tick(1) | | | | | Choice | | | | | 3/4: A :~ {1 : 1 + A} | | | | | 1/4: A :~ {1 : -1 + A} | | | | | | | | | +- While.step | | | | | | | | | | | +- [Problem] | | | | | | 3:While(E 1 + A) | | | | | | Tick(1) | | | | | | Choice | | | | | | 3/4: A :~ {1 : 1 + A} | | | | | | 1/4: A :~ {1 : -1 + A} | | | | | | | | | | | +- [f] | | | | | | 0 | | | | | | | | | | | +- Expected Cost Body | | | | | | | | | | | | | `- [1 | ] | | | | | | | | | | | +- linear-template | | | | | | | | | | | | | `- 1 + [-A + E | -A + E 0] | | | | | | | | | | | +- [Norms] | | | | | | [[1 | ],[-A + E | -A + E 0]] | | | | | | | | | | | +- [Invariant] | | | | | | E 1 + A ==> [1 | ] + h([1 | ],3/4[-1 + -A + E | -1 + -A + E 0] + 1/4[1 + -A + E | 1 + -A + E 0]) h([1 | ],[-A + E | -A + E 0]) | | | | | | 1 + A 1 + E ==> 0 h([1 | ],[-A + E | -A + E 0]) | | | | | | | | | | | `- 2[-A + E | -A + E 0] | | | | | | | | | `- 2[-A + E | -A + E 0] | | | | | | | +- Expected Cost | | | | | | | | | +- [f] | | | | | 0 | | | | | | | | | +- [Program] | | | | | Tick(1) | | | | | H :~ {1 : 0} | | | | | 4:While(E 1 + H) | | | | | Tick(1) | | | | | Choice | | | | | 3/4: H :~ {1 : 1 + H} | | | | | 1/4: H :~ {1 : -1 + H} | | | | | Tick(1) | | | | | I :~ {1 : 0} | | | | | 5:While(E 1 + I) | | | | | Tick(1) | | | | | Choice | | | | | 3/4: I :~ {1 : 1 + I} | | | | | 1/4: I :~ {1 : -1 + I} | | | | | Tick(1) | | | | | J :~ {1 : 0} | | | | | 6:While(E 1 + J) | | | | | Choice | | | | | 3/4: J :~ {1 : 1 + J} | | | | | 1/4: J :~ {1 : -1 + J} | | | | | Tick(1) | | | | | A :~ {1 : 0} | | | | | 7:While(E 1 + A) | | | | | Tick(1) | | | | | Choice | | | | | 3/4: A :~ {1 : 1 + A} | | | | | 1/4: A :~ {1 : -1 + A} | | | | | Tick(1) | | | | | | | | | +- Expected Cost | | | | | | | | | | | +- [f] | | | | | | 0 | | | | | | | | | | | +- [Program] | | | | | | 4:While(E 1 + H) | | | | | | Tick(1) | | | | | | Choice | | | | | | 3/4: H :~ {1 : 1 + H} | | | | | | 1/4: H :~ {1 : -1 + H} | | | | | | | | | | | +- While.step | | | | | | | | | | | | | +- [Problem] | | | | | | | 4:While(E 1 + H) | | | | | | | Tick(1) | | | | | | | Choice | | | | | | | 3/4: H :~ {1 : 1 + H} | | | | | | | 1/4: H :~ {1 : -1 + H} | | | | | | | | | | | | | +- [f] | | | | | | | 0 | | | | | | | | | | | | | +- Expected Cost Body | | | | | | | | | | | | | | | `- [1 | ] | | | | | | | | | | | | | +- linear-template | | | | | | | | | | | | | | | `- 1 + [E + -H | E + -H 0] | | | | | | | | | | | | | +- [Norms] | | | | | | | [[1 | ],[E + -H | E + -H 0]] | | | | | | | | | | | | | +- [Invariant] | | | | | | | E 1 + H ==> [1 | ] + h([1 | ],3/4[-1 + E + -H | -1 + E + -H 0] + 1/4[1 + E + -H | 1 + E + -H 0]) h([1 | ],[E + -H | E + -H 0]) | | | | | | | 1 + H 1 + E ==> 0 h([1 | ],[E + -H | E + -H 0]) | | | | | | | | | | | | | `- 2[E + -H | E + -H 0] | | | | | | | | | | | `- 2[E + -H | E + -H 0] | | | | | | | | | +- Expected Cost | | | | | | | | | | | +- [f] | | | | | | 0 | | | | | | | | | | | +- [Program] | | | | | | Tick(1) | | | | | | I :~ {1 : 0} | | | | | | 5:While(E 1 + I) | | | | | | Tick(1) | | | | | | Choice | | | | | | 3/4: I :~ {1 : 1 + I} | | | | | | 1/4: I :~ {1 : -1 + I} | | | | | | Tick(1) | | | | | | J :~ {1 : 0} | | | | | | 6:While(E 1 + J) | | | | | | Choice | | | | | | 3/4: J :~ {1 : 1 + J} | | | | | | 1/4: J :~ {1 : -1 + J} | | | | | | Tick(1) | | | | | | A :~ {1 : 0} | | | | | | 7:While(E 1 + A) | | | | | | Tick(1) | | | | | | Choice | | | | | | 3/4: A :~ {1 : 1 + A} | | | | | | 1/4: A :~ {1 : -1 + A} | | | | | | Tick(1) | | | | | | | | | | | +- Expected Cost | | | | | | | | | | | | | +- [f] | | | | | | | 0 | | | | | | | | | | | | | +- [Program] | | | | | | | 5:While(E 1 + I) | | | | | | | Tick(1) | | | | | | | Choice | | | | | | | 3/4: I :~ {1 : 1 + I} | | | | | | | 1/4: I :~ {1 : -1 + I} | | | | | | | | | | | | | +- While.step | | | | | | | | | | | | | | | +- [Problem] | | | | | | | | 5:While(E 1 + I) | | | | | | | | Tick(1) | | | | | | | | Choice | | | | | | | | 3/4: I :~ {1 : 1 + I} | | | | | | | | 1/4: I :~ {1 : -1 + I} | | | | | | | | | | | | | | | +- [f] | | | | | | | | 0 | | | | | | | | | | | | | | | +- Expected Cost Body | | | | | | | | | | | | | | | | | `- [1 | ] | | | | | | | | | | | | | | | +- linear-template | | | | | | | | | | | | | | | | | `- 1 + [E + -I | E + -I 0] | | | | | | | | | | | | | | | +- [Norms] | | | | | | | | [[1 | ],[E + -I | E + -I 0]] | | | | | | | | | | | | | | | +- [Invariant] | | | | | | | | E 1 + I ==> [1 | ] + h([1 | ],3/4[-1 + E + -I | -1 + E + -I 0] + 1/4[1 + E + -I | 1 + E + -I 0]) h([1 | ],[E + -I | E + -I 0]) | | | | | | | | 1 + I 1 + E ==> 0 h([1 | ],[E + -I | E + -I 0]) | | | | | | | | | | | | | | | `- 2[E + -I | E + -I 0] | | | | | | | | | | | | | `- 2[E + -I | E + -I 0] | | | | | | | | | | | +- Expected Cost | | | | | | | | | | | | | +- [f] | | | | | | | 0 | | | | | | | | | | | | | +- [Program] | | | | | | | Tick(1) | | | | | | | J :~ {1 : 0} | | | | | | | 6:While(E 1 + J) | | | | | | | Choice | | | | | | | 3/4: J :~ {1 : 1 + J} | | | | | | | 1/4: J :~ {1 : -1 + J} | | | | | | | Tick(1) | | | | | | | A :~ {1 : 0} | | | | | | | 7:While(E 1 + A) | | | | | | | Tick(1) | | | | | | | Choice | | | | | | | 3/4: A :~ {1 : 1 + A} | | | | | | | 1/4: A :~ {1 : -1 + A} | | | | | | | Tick(1) | | | | | | | | | | | | | +- Expected Cost | | | | | | | | | | | | | | | +- [f] | | | | | | | | 0 | | | | | | | | | | | | | | | +- [Program] | | | | | | | | 6:While(E 1 + J) | | | | | | | | Choice | | | | | | | | 3/4: J :~ {1 : 1 + J} | | | | | | | | 1/4: J :~ {1 : -1 + J} | | | | | | | | | | | | | | | `- 0 | | | | | | | | | | | | | +- Expected Cost | | | | | | | | | | | | | | | +- [f] | | | | | | | | 0 | | | | | | | | | | | | | | | +- [Program] | | | | | | | | Tick(1) | | | | | | | | A :~ {1 : 0} | | | | | | | | 7:While(E 1 + A) | | | | | | | | Tick(1) | | | | | | | | Choice | | | | | | | | 3/4: A :~ {1 : 1 + A} | | | | | | | | 1/4: A :~ {1 : -1 + A} | | | | | | | | Tick(1) | | | | | | | | | | | | | | | +- Expected Cost | | | | | | | | | | | | | | | | | +- [f] | | | | | | | | | 0 | | | | | | | | | | | | | | | | | +- [Program] | | | | | | | | | 7:While(E 1 + A) | | | | | | | | | Tick(1) | | | | | | | | | Choice | | | | | | | | | 3/4: A :~ {1 : 1 + A} | | | | | | | | | 1/4: A :~ {1 : -1 + A} | | | | | | | | | | | | | | | | | +- While.step | | | | | | | | | | | | | | | | | | | +- [Problem] | | | | | | | | | | 7:While(E 1 + A) | | | | | | | | | | Tick(1) | | | | | | | | | | Choice | | | | | | | | | | 3/4: A :~ {1 : 1 + A} | | | | | | | | | | 1/4: A :~ {1 : -1 + A} | | | | | | | | | | | | | | | | | | | +- [f] | | | | | | | | | | 0 | | | | | | | | | | | | | | | | | | | +- Expected Cost Body | | | | | | | | | | | | | | | | | | | | | `- [1 | ] | | | | | | | | | | | | | | | | | | | +- linear-template | | | | | | | | | | | | | | | | | | | | | `- 1 + [-A + E | -A + E 0] | | | | | | | | | | | | | | | | | | | +- [Norms] | | | | | | | | | | [[1 | ],[-A + E | -A + E 0]] | | | | | | | | | | | | | | | | | | | +- [Invariant] | | | | | | | | | | E 1 + A ==> [1 | ] + h([1 | ],3/4[-1 + -A + E | -1 + -A + E 0] + 1/4[1 + -A + E | 1 + -A + E 0]) h([1 | ],[-A + E | -A + E 0]) | | | | | | | | | | 1 + A 1 + E ==> 0 h([1 | ],[-A + E | -A + E 0]) | | | | | | | | | | | | | | | | | | | `- 2[-A + E | -A + E 0] | | | | | | | | | | | | | | | | | `- 2[-A + E | -A + E 0] | | | | | | | | | | | | | | | +- Expected Cost | | | | | | | | | | | | | | | | | +- [f] | | | | | | | | | 0 | | | | | | | | | | | | | | | | | +- [Program] | | | | | | | | | Tick(1) | | | | | | | | | | | | | | | | | `- [1 | ] | | | | | | | | | | | | | | | +- Expected Cost | | | | | | | | | | | | | | | | | +- [f] | | | | | | | | | [1 | ] | | | | | | | | | | | | | | | | | +- [Program] | | | | | | | | | 7:While(E 1 + A) | | | | | | | | | Tick(1) | | | | | | | | | Choice | | | | | | | | | 3/4: A :~ {1 : 1 + A} | | | | | | | | | 1/4: A :~ {1 : -1 + A} | | | | | | | | | | | | | | | | | `- [1 | ] | | | | | | | | | | | | | | | `- [1 | ] + 2[E | E 0] + [1 | ] | | | | | | | | | | | | | +- Expected Cost | | | | | | | | | | | | | | | +- [f] | | | | | | | | [1 | ] + 2[E | E 0] + [1 | ] | | | | | | | | | | | | | | | +- [Program] | | | | | | | | 6:While(E 1 + J) | | | | | | | | Choice | | | | | | | | 3/4: J :~ {1 : 1 + J} | | | | | | | | 1/4: J :~ {1 : -1 + J} | | | | | | | | | | | | | | | `- [1 | ] + 2[E | E 0] + [1 | ] | | | | | | | | | | | | | `- [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] | | | | | | | | | | | +- Expected Cost | | | | | | | | | | | | | +- [f] | | | | | | | [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] | | | | | | | | | | | | | +- [Program] | | | | | | | 5:While(E 1 + I) | | | | | | | Tick(1) | | | | | | | Choice | | | | | | | 3/4: I :~ {1 : 1 + I} | | | | | | | 1/4: I :~ {1 : -1 + I} | | | | | | | | | | | | | `- [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] | | | | | | | | | | | `- [1 | ] + 2[E | E 0] + [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] | | | | | | | | | +- Expected Cost | | | | | | | | | | | +- [f] | | | | | | [1 | ] + 2[E | E 0] + [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] | | | | | | | | | | | +- [Program] | | | | | | 4:While(E 1 + H) | | | | | | Tick(1) | | | | | | Choice | | | | | | 3/4: H :~ {1 : 1 + H} | | | | | | 1/4: H :~ {1 : -1 + H} | | | | | | | | | | | `- [1 | ] + 2[E | E 0] + [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] | | | | | | | | | `- [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] | | | | | | | +- Expected Cost | | | | | | | | | +- [f] | | | | | [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] | | | | | | | | | +- [Program] | | | | | 3:While(E 1 + A) | | | | | Tick(1) | | | | | Choice | | | | | 3/4: A :~ {1 : 1 + A} | | | | | 1/4: A :~ {1 : -1 + A} | | | | | | | | | `- [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] | | | | | | | `- [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] | | | | | +- Expected Cost | | | | | | | +- [f] | | | | [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] | | | | | | | +- [Program] | | | | 2:While(E 1 + G) | | | | Tick(1) | | | | Choice | | | | 3/4: G :~ {1 : 1 + G} | | | | 1/4: G :~ {1 : -1 + G} | | | | | | | `- [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] | | | | | `- [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] | | | +- Expected Cost | | | | | +- [f] | | | [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] | | | | | +- [Program] | | | 1:While(E 1 + F) | | | Tick(1) | | | Choice | | | 3/4: F :~ {1 : 1 + F} | | | 1/4: F :~ {1 : -1 + F} | | | | | `- [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] | | | `- [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] | +- Expected Cost | | | +- [f] | | [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] | | | +- [Program] | | 0:While(E 1 + D) | | Tick(1) | | Choice | | 3/4: D :~ {1 : 1 + D} | | 1/4: D :~ {1 : -1 + D} | | | `- [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] | `- [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] [Success] [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + 2[E | E 0] + [1 | ] + [1 | ] + 2[E | E 0] + [1 | ] Degree: 1