ExecutionLog | `- Expected Cost | +- [f] | 0 | +- [Program] | 0:While(x 1) | Choice | 1/3: x :~ {1 : 1 + x} | 2/3: x :~ {1 : -1 + x} | 1:While(x 1) | Choice | 1/4: x :~ {1 : 1 + x} | 3/4: x :~ {1 : -1 + x} | Tick(1) | +- While.step | | | +- [Problem] | | 0:While(x 1) | | Choice | | 1/3: x :~ {1 : 1 + x} | | 2/3: x :~ {1 : -1 + x} | | 1:While(x 1) | | Choice | | 1/4: x :~ {1 : 1 + x} | | 3/4: x :~ {1 : -1 + x} | | Tick(1) | | | +- [f] | | 0 | | | +- Expected Cost Body | | | | | +- While.step | | | | | | | +- [Problem] | | | | 1:While(x 1) | | | | Choice | | | | 1/4: x :~ {1 : 1 + x} | | | | 3/4: x :~ {1 : -1 + x} | | | | Tick(1) | | | | | | | +- [f] | | | | 0 | | | | | | | +- Expected Cost Body | | | | | | | | | `- [1 | ] | | | | | | | +- linear-template | | | | | | | | | `- 1 + [x | x 0] | | | | | | | +- [Norms] | | | | [[1 | ],[x | x 0]] | | | | | | | +- [Invariant] | | | | x 1 ==> [1 | ] + h([1 | ],1/4[1 + x | 1 + x 0] + 3/4[-1 + x | -1 + x 0]) h([1 | ],[x | x 0]) | | | | 1 1 + x ==> 0 h([1 | ],[x | x 0]) | | | | | | | `- 2[x | x 0] | | | | | `- 2/3[1 + x | 1 + x 0] + 4/3[-1 + x | -1 + x 0] | | | +- linear-template | | | | | `- 1 + [-1 + x | -1 + x 0] + [1 + x | 1 + x 0] + [x | x 0] | | | +- [Norms] | | [[1 | ],[-1 + x | -1 + x 0],[1 + x | 1 + x 0],[x | x 0]] | | | +- While.step | | | | | +- [Problem] | | | 1:While(x 1) | | | Choice | | | 1/4: x :~ {1 : 1 + x} | | | 3/4: x :~ {1 : -1 + x} | | | Tick(1) | | | | | +- [f] | | | [-1 + x | -1 + x 0] | | | | | +- linear-template | | | | | | | `- 1 + [-1 + x | -1 + x 0] + 2([x | x 0]) | | | | | +- [Norms] | | | [[1 | ],[-1 + x | -1 + x 0],[x | x 0]] | | | | | +- [Invariant] | | | x 1 ==> 0 + h([1 | ],1/4[x | x 0] + 3/4[-2 + x | -2 + x 0],1/4[1 + x | 1 + x 0] + 3/4[-1 + x | -1 + x 0]) h([1 | ],[-1 + x | -1 + x 0],[x | x 0]) | | | 1 1 + x ==> [-1 + x | -1 + x 0] h([1 | ],[-1 + x | -1 + x 0],[x | x 0]) | | | | | `- 0 | | | +- While.step | | | | | +- [Problem] | | | 1:While(x 1) | | | Choice | | | 1/4: x :~ {1 : 1 + x} | | | 3/4: x :~ {1 : -1 + x} | | | Tick(1) | | | | | +- [f] | | | [1 + x | 1 + x 0] | | | | | +- linear-template | | | | | | | `- 1 + [1 + x | 1 + x 0] + 2([x | x 0]) | | | | | +- [Norms] | | | [[1 | ],[1 + x | 1 + x 0],[x | x 0]] | | | | | +- [Invariant] | | | x 1 ==> 0 + h([1 | ],1/4[2 + x | 2 + x 0] + 3/4[x | x 0],1/4[1 + x | 1 + x 0] + 3/4[-1 + x | -1 + x 0]) h([1 | ],[1 + x | 1 + x 0],[x | x 0]) | | | 1 1 + x ==> [1 + x | 1 + x 0] h([1 | ],[1 + x | 1 + x 0],[x | x 0]) | | | | | `- [1 | ] | | | +- While.step | | | | | +- [Problem] | | | 1:While(x 1) | | | Choice | | | 1/4: x :~ {1 : 1 + x} | | | 3/4: x :~ {1 : -1 + x} | | | Tick(1) | | | | | +- [f] | | | [x | x 0] | | | | | +- linear-template | | | | | | | `- 1 + 3([x | x 0]) | | | | | +- [Norms] | | | [[1 | ],[x | x 0]] | | | | | +- [Invariant] | | | x 1 ==> 0 + h([1 | ],1/4[1 + x | 1 + x 0] + 3/4[-1 + x | -1 + x 0]) h([1 | ],[x | x 0]) | | | 1 1 + x ==> [x | x 0] h([1 | ],[x | x 0]) | | | | | `- 0 | | | +- [Invariant] | | x 1 ==> 2/3[1 + x | 1 + x 0] + 4/3[-1 + x | -1 + x 0] + h([1 | ],0,[1 | ],0) h([1 | ],[-1 + x | -1 + x 0],[1 + x | 1 + x 0],[x | x 0]) | | 1 1 + x ==> 0 h([1 | ],[-1 + x | -1 + x 0],[1 + x | 1 + x 0],[x | x 0]) | | | `- 2[1 + x | 1 + x 0] | `- 2[1 + x | 1 + x 0] [Success] 2[1 + x | 1 + x 0] Degree: 1