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