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