Expected Cost | +- [f] | 0 | +- [Program] | 0:While(n ≥ 1) | i :~ {3/10 : 1;7/10 : 0} | Tick(1) | d :~ {2/5 : 1;3/5 : 0} | Tick(1) | 1:If(1 ≥ 1 + d ∧ 1 ≥ 1 + i) Then | g :~ {7/10 : 1;3/10 : 0} | Tick(1) | Else | 2:If(1 ≥ 1 + i ∧ d ≥ 1) Then | g :~ {19/20 : 1;1/20 : 0} | Tick(1) | Else | 3:If(1 ≥ 1 + d ∧ i ≥ 1) Then | g :~ {1/10 : 1;9/10 : 0} | Tick(1) | Else | g :~ {1/2 : 1;1/2 : 0} | Tick(1) | 4:If(1 ≥ 1 + i) Then | s :~ {1/20 : 1;19/20 : 0} | Tick(1) | Else | s :~ {4/5 : 1;1/5 : 0} | Tick(1) | 5:If(1 ≥ 1 + g) Then | l :~ {1/10 : 1;9/10 : 0} | Tick(1) | Else | l :~ {3/5 : 1;2/5 : 0} | Tick(1) | n :~ {1 : -1 + n} | +- While.step | | | +- [Problem] | | 0:While(n ≥ 1) | | i :~ {3/10 : 1;7/10 : 0} | | Tick(1) | | d :~ {2/5 : 1;3/5 : 0} | | Tick(1) | | 1:If(1 ≥ 1 + d ∧ 1 ≥ 1 + i) Then | | g :~ {7/10 : 1;3/10 : 0} | | Tick(1) | | Else | | 2:If(1 ≥ 1 + i ∧ d ≥ 1) Then | | g :~ {19/20 : 1;1/20 : 0} | | Tick(1) | | Else | | 3:If(1 ≥ 1 + d ∧ i ≥ 1) Then | | g :~ {1/10 : 1;9/10 : 0} | | Tick(1) | | Else | | g :~ {1/2 : 1;1/2 : 0} | | Tick(1) | | 4:If(1 ≥ 1 + i) Then | | s :~ {1/20 : 1;19/20 : 0} | | Tick(1) | | Else | | s :~ {4/5 : 1;1/5 : 0} | | Tick(1) | | 5:If(1 ≥ 1 + g) Then | | l :~ {1/10 : 1;9/10 : 0} | | Tick(1) | | Else | | l :~ {3/5 : 1;2/5 : 0} | | Tick(1) | | n :~ {1 : -1 + n} | | | +- [f] | | 0 | | | +- Expected Cost Body | | | | | `- 5 | | | +- linear-template | | | | | `- 1 + [n | n ≥ 0] | | | +- [Norms] | | [[1 | ⊤],[n | n ≥ 0]] | | | +- [Invariant] | | n ≥ 1 ==> 5 + h([1 | ⊤],[-1 + n | -1 + n ≥ 0]) ≼ h([1 | ⊤],[n | n ≥ 0]) | | 1 ≥ 1 + n ==> 0 ≼ h([1 | ⊤],[n | n ≥ 0]) | | | `- 5·[n | n ≥ 0] | `- 5·[n | n ≥ 0]