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