ExecutionLog | `- 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} | sample :~ {1/3 : -1;1/3 : 0;1/3 : 1} | mt :~ {1 : mt + sample} | 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} | | sample :~ {1/3 : -1;1/3 : 0;1/3 : 1} | | mt :~ {1 : mt + sample} | | 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} | | | | sample :~ {1/3 : -1;1/3 : 0;1/3 : 1} | | | | mt :~ {1 : mt + sample} | | | | 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] [Success] 21/10[1 + t | 1 + t 0] + [mt + -st | mt + -st 0] Degree: 1