Expected Cost | +- [f] | 0 | +- [Program] | 0:While(t ≥ 0) | 1:While(mt ≥ 1 + st) | mt :~ {1 : -1 + mt} | Tick(1) | 2:If(mt ≥ st ∧ st ≥ mt) Then | Skip | Else | Abort | Choice | 1/10: mt :~ {1 : 1 + mt} | 9/10: Choice | 7/9: mt :~ {1 : 2 + mt} | 2/9: mt :~ {1 : 3 + mt} | r :~ {1/3 : 0;1/3 : 1;1/3 : 2} | mt :~ {1 : -1 + mt + r} | t :~ {1 : -5 + t} | +- While.step | | | +- [Problem] | | 0:While(t ≥ 0) | | 1:While(mt ≥ 1 + st) | | mt :~ {1 : -1 + mt} | | Tick(1) | | 2:If(mt ≥ st ∧ st ≥ mt) Then | | Skip | | Else | | Abort | | Choice | | 1/10: mt :~ {1 : 1 + mt} | | 9/10: Choice | | 7/9: mt :~ {1 : 2 + mt} | | 2/9: mt :~ {1 : 3 + mt} | | r :~ {1/3 : 0;1/3 : 1;1/3 : 2} | | mt :~ {1 : -1 + mt + r} | | t :~ {1 : -5 + t} | | | +- [f] | | 0 | | | +- Expected Cost Body | | | | | +- Expected Cost | | | | | | | +- [f] | | | | 0 | | | | | | | +- [Program] | | | | 1:While(mt ≥ 1 + st) | | | | mt :~ {1 : -1 + mt} | | | | Tick(1) | | | | | | | +- While.step | | | | | | | | | +- [Problem] | | | | | 1:While(mt ≥ 1 + st) | | | | | mt :~ {1 : -1 + mt} | | | | | Tick(1) | | | | | | | | | +- [f] | | | | | 0 | | | | | | | | | +- Expected Cost Body | | | | | | | | | | | `- [1 | ⊤] | | | | | | | | | +- linear-template | | | | | | | | | | | `- 1 + [mt + -st | mt + -st ≥ 0] | | | | | | | | | +- [Norms] | | | | | [[1 | ⊤],[mt + -st | mt + -st ≥ 0]] | | | | | | | | | +- [Invariant] | | | | | mt ≥ 1 + st ==> [1 | ⊤] + h([1 | ⊤],[-1 + mt + -st | -1 + mt + -st ≥ 0]) ≼ h([1 | ⊤],[mt + -st | mt + -st ≥ 0]) | | | | | 1 + st ≥ 1 + mt ==> 0 ≼ h([1 | ⊤],[mt + -st | mt + -st ≥ 0]) | | | | | | | | | `- [mt + -st | mt + -st ≥ 0] | | | | | | | `- [mt + -st | mt + -st ≥ 0] | | | | | +- Expected Cost | | | | | | | +- [f] | | | | 0 | | | | | | | +- [Program] | | | | 2:If(mt ≥ st ∧ st ≥ mt) Then | | | | Skip | | | | Else | | | | Abort | | | | Choice | | | | 1/10: mt :~ {1 : 1 + mt} | | | | 9/10: Choice | | | | 7/9: mt :~ {1 : 2 + mt} | | | | 2/9: mt :~ {1 : 3 + mt} | | | | r :~ {1/3 : 0;1/3 : 1;1/3 : 2} | | | | mt :~ {1 : -1 + mt + r} | | | | t :~ {1 : -5 + t} | | | | | | | `- 0 | | | | | +- Expected Cost | | | | | | | +- [f] | | | | 0 | | | | | | | +- [Program] | | | | 1:While(mt ≥ 1 + st) | | | | mt :~ {1 : -1 + mt} | | | | Tick(1) | | | | | | | `- 0 | | | | | `- [mt + -st | mt + -st ≥ 0] | | | +- linear-template | | | | | `- 1 + [1 + t | 1 + t ≥ 0] + [mt + -st | mt + -st ≥ 0] | | | +- [Norms] | | [[1 | ⊤],[1 + t | 1 + t ≥ 0],[mt + -st | mt + -st ≥ 0]] | | | +- While.step | | | | | +- [Problem] | | | 1:While(mt ≥ 1 + st) | | | mt :~ {1 : -1 + mt} | | | Tick(1) | | | | | +- [f] | | | [mt ≥ st ∧ st ≥ mt] · [-4 + t | -4 + t ≥ 0] | | | | | +- linear-template | | | | | | | `- 1 + [-4 + t | -4 + t ≥ 0] + [1 + -mt + st | 1 + -mt + st ≥ 0] + [1 + mt + -st | 1 + mt + -st ≥ 0] + 2·([mt + -st | mt + -st ≥ 0]) | | | | | +- [Norms] | | | [[1 | ⊤],[-4 + t | -4 + t ≥ 0],[1 + -mt + st | 1 + -mt + st ≥ 0],[1 + mt + -st | 1 + mt + -st ≥ 0],[mt + -st | mt + -st ≥ 0]] | | | | | +- [Invariant] | | | mt ≥ 1 + st ==> 0 + h([1 | ⊤],[-4 + t | -4 + t ≥ 0],[2 + -mt + st | 2 + -mt + st ≥ 0],[mt + -st | mt + -st ≥ 0],[-1 + mt + -st | -1 + mt + -st ≥ 0]) ≼ h([1 | ⊤],[-4 + t | -4 + t ≥ 0],[1 + -mt + st | 1 + -mt + st ≥ 0],[1 + mt + -st | 1 + mt + -st ≥ 0],[mt + -st | mt + -st ≥ 0]) | | | 1 + st ≥ 1 + mt ==> [mt ≥ st ∧ st ≥ mt] · [-4 + t | -4 + t ≥ 0] ≼ h([1 | ⊤],[-4 + t | -4 + t ≥ 0],[1 + -mt + st | 1 + -mt + st ≥ 0],[1 + mt + -st | 1 + mt + -st ≥ 0],[mt + -st | mt + -st ≥ 0]) | | | | | `- [-4 + t | -4 + t ≥ 0] | | | +- While.step | | | | | +- [Problem] | | | 1:While(mt ≥ 1 + st) | | | mt :~ {1 : -1 + mt} | | | Tick(1) | | | | | +- [f] | | | [mt ≥ st ∧ st ≥ mt] · (1/30·[mt + -st | mt + -st ≥ 0] + 1/30·[1 + mt + -st | 1 + mt + -st ≥ 0] + 1/30·[2 + mt + -st | 2 + mt + -st ≥ 0] + 7/30·[1 + mt + -st | 1 + mt + -st ≥ 0] + 7/30·[2 + mt + -st | 2 + mt + -st ≥ 0] + 7/30·[3 + mt + -st | 3 + mt + -st ≥ 0] + 1/15·[2 + mt + -st | 2 + mt + -st ≥ 0] + 1/15·[3 + mt + -st | 3 + mt + -st ≥ 0] + 1/15·[4 + mt + -st | 4 + mt + -st ≥ 0]) | | | | | +- linear-template | | | | | | | `- 1 + 9·([1 + -mt + st | 1 + -mt + st ≥ 0]) + 11·([1 + mt + -st | 1 + mt + -st ≥ 0]) + 3·([2 + mt + -st | 2 + mt + -st ≥ 0]) + 2·([3 + mt + -st | 3 + mt + -st ≥ 0]) + [4 + mt + -st | 4 + mt + -st ≥ 0] + 11·([mt + -st | mt + -st ≥ 0]) | | | | | +- [Norms] | | | [[1 | ⊤],[1 + -mt + st | 1 + -mt + st ≥ 0],[1 + mt + -st | 1 + mt + -st ≥ 0],[2 + mt + -st | 2 + mt + -st ≥ 0],[3 + mt + -st | 3 + mt + -st ≥ 0],[4 + mt + -st | 4 + mt + -st ≥ 0],[mt + -st | mt + -st ≥ 0]] | | | | | +- [Invariant] | | | mt ≥ 1 + st ==> 0 + h([1 | ⊤],[2 + -mt + st | 2 + -mt + st ≥ 0],[mt + -st | mt + -st ≥ 0],[1 + mt + -st | 1 + mt + -st ≥ 0],[2 + mt + -st | 2 + mt + -st ≥ 0],[3 + mt + -st | 3 + mt + -st ≥ 0],[-1 + mt + -st | -1 + mt + -st ≥ 0]) ≼ h([1 | ⊤],[1 + -mt + st | 1 + -mt + st ≥ 0],[1 + mt + -st | 1 + mt + -st ≥ 0],[2 + mt + -st | 2 + mt + -st ≥ 0],[3 + mt + -st | 3 + mt + -st ≥ 0],[4 + mt + -st | 4 + mt + -st ≥ 0],[mt + -st | mt + -st ≥ 0]) | | | 1 + st ≥ 1 + mt ==> [mt ≥ st ∧ st ≥ mt] · (1/30·[mt + -st | mt + -st ≥ 0] + 1/30·[1 + mt + -st | 1 + mt + -st ≥ 0] + 1/30·[2 + mt + -st | 2 + mt + -st ≥ 0] + 7/30·[1 + mt + -st | 1 + mt + -st ≥ 0] + 7/30·[2 + mt + -st | 2 + mt + -st ≥ 0] + 7/30·[3 + mt + -st | 3 + mt + -st ≥ 0] + 1/15·[2 + mt + -st | 2 + mt + -st ≥ 0] + 1/15·[3 + mt + -st | 3 + mt + -st ≥ 0] + 1/15·[4 + mt + -st | 4 + mt + -st ≥ 0]) ≼ h([1 | ⊤],[1 + -mt + st | 1 + -mt + st ≥ 0],[1 + mt + -st | 1 + mt + -st ≥ 0],[2 + mt + -st | 2 + mt + -st ≥ 0],[3 + mt + -st | 3 + mt + -st ≥ 0],[4 + mt + -st | 4 + mt + -st ≥ 0],[mt + -st | mt + -st ≥ 0]) | | | | | `- 21/10 | | | +- [Invariant] | | t ≥ 0 ==> [mt + -st | mt + -st ≥ 0] + h([1 | ⊤],[-4 + t | -4 + t ≥ 0],21/10) ≼ h([1 | ⊤],[1 + t | 1 + t ≥ 0],[mt + -st | mt + -st ≥ 0]) | | 0 ≥ 1 + t ==> 0 ≼ h([1 | ⊤],[1 + t | 1 + t ≥ 0],[mt + -st | mt + -st ≥ 0]) | | | `- 21/10·[1 + t | 1 + t ≥ 0] + [mt + -st | mt + -st ≥ 0] | `- 21/10·[1 + t | 1 + t ≥ 0] + [mt + -st | mt + -st ≥ 0]