Expected Cost | +- [f] | 0 | +- [Program] | x :~ {1 : 0} | y :~ {1 : 0} | eX :~ {1 : 0} | eY :~ {1 : 0} | dx :~ {1 : 0} | dy :~ {1 : 0} | dxc :~ {1 : 0} | dyc :~ {1 : 0} | 0:While(n ≥ 1) | dx :~ {1 : 0} | dy :~ {1 : 0} | Choice | 1/10: cmd :~ {1 : 0} | 9/10: Choice | 1/9: cmd :~ {1 : 1} | 8/9: Choice | 1/8: cmd :~ {1 : 2} | 7/8: Choice | 1/7: cmd :~ {1 : 3} | 6/7: Choice | 1/6: cmd :~ {1 : 4} | 5/6: Choice | 1/5: cmd :~ {1 : 5} | 4/5: Choice | 1/4: cmd :~ {1 : 6} | 3/4: Choice | 1/3: cmd :~ {1 : 7} | 2/3: cmd :~ {1 : 8} | 1:If(0 ≥ cmd ∧ cmd ≥ 0) Then | n :~ {1 : -1 + n} | Else | 2:If(1 ≥ cmd ∧ cmd ≥ 1) Then | n :~ {1 : -2 + n} | Else | 3:If(2 ≥ cmd ∧ cmd ≥ 2) Then | n :~ {1 : -3 + n} | Else | 4:If(3 ≥ cmd ∧ cmd ≥ 3) Then | n :~ {1 : -4 + n} | Else | 5:If(4 ≥ cmd ∧ cmd ≥ 4) Then | n :~ {1 : -5 + n} | Else | 6:If(5 ≥ cmd ∧ cmd ≥ 5) Then | n :~ {1 : -6 + n} | Else | 7:If(6 ≥ cmd ∧ cmd ≥ 6) Then | n :~ {1 : -7 + n} | Else | 8:If(7 ≥ cmd ∧ cmd ≥ 7) Then | n :~ {1 : -8 + n} | Else | n :~ {1 : n} | Tick(1) | +- While.step | | | +- [Problem] | | 0:While(n ≥ 1) | | dx :~ {1 : 0} | | dy :~ {1 : 0} | | Choice | | 1/10: cmd :~ {1 : 0} | | 9/10: Choice | | 1/9: cmd :~ {1 : 1} | | 8/9: Choice | | 1/8: cmd :~ {1 : 2} | | 7/8: Choice | | 1/7: cmd :~ {1 : 3} | | 6/7: Choice | | 1/6: cmd :~ {1 : 4} | | 5/6: Choice | | 1/5: cmd :~ {1 : 5} | | 4/5: Choice | | 1/4: cmd :~ {1 : 6} | | 3/4: Choice | | 1/3: cmd :~ {1 : 7} | | 2/3: cmd :~ {1 : 8} | | 1:If(0 ≥ cmd ∧ cmd ≥ 0) Then | | n :~ {1 : -1 + n} | | Else | | 2:If(1 ≥ cmd ∧ cmd ≥ 1) Then | | n :~ {1 : -2 + n} | | Else | | 3:If(2 ≥ cmd ∧ cmd ≥ 2) Then | | n :~ {1 : -3 + n} | | Else | | 4:If(3 ≥ cmd ∧ cmd ≥ 3) Then | | n :~ {1 : -4 + n} | | Else | | 5:If(4 ≥ cmd ∧ cmd ≥ 4) Then | | n :~ {1 : -5 + n} | | Else | | 6:If(5 ≥ cmd ∧ cmd ≥ 5) Then | | n :~ {1 : -6 + n} | | Else | | 7:If(6 ≥ cmd ∧ cmd ≥ 6) Then | | n :~ {1 : -7 + n} | | Else | | 8:If(7 ≥ cmd ∧ cmd ≥ 7) Then | | n :~ {1 : -8 + n} | | Else | | n :~ {1 : n} | | Tick(1) | | | +- [f] | | 0 | | | +- Expected Cost Body | | | | | `- [1 | ⊤] | | | +- linear-template | | | | | `- 1 + [n | n ≥ 0] | | | +- [Norms] | | [[1 | ⊤],[n | n ≥ 0]] | | | +- [Invariant] | | n ≥ 1 ==> [1 | ⊤] + h([1 | ⊤],1/10·[-1 + n | -1 + n ≥ 0] + 1/10·[-2 + n | -2 + n ≥ 0] + 1/10·[-3 + n | -3 + n ≥ 0] + 1/10·[-4 + n | -4 + n ≥ 0] + 1/10·[-5 + n | -5 + n ≥ 0] + 1/10·[-6 + n | -6 + n ≥ 0] + 1/10·[-7 + n | -7 + n ≥ 0] + 1/10·[-8 + n | -8 + n ≥ 0] + 1/5·[n | n ≥ 0]) ≼ h([1 | ⊤],[n | n ≥ 0]) | | 1 ≥ 1 + n ==> 0 ≼ h([1 | ⊤],[n | n ≥ 0]) | | | `- 5/4·[n | n ≥ 0] | `- 5/4·[n | n ≥ 0]