Expected Cost | +- [f] | 0 | +- [Program] | 0:If(y ≥ 0) Then | Skip | Else | Abort | 1:While(0 ≥ 1 + n) | Choice | 9/10: n :~ {1 : 1 + n} | 1/10: Skip | Tick(9) | NonDet | {2:While(y ≥ 100) | Choice | 1/2: y :~ {1 : -100 + y} | 1/2: y :~ {1 : -90 + y} | Tick(5)} | {Skip} | y :~ {1 : 1000 + y} | +- While.step | | | +- [Problem] | | 1:While(0 ≥ 1 + n) | | Choice | | 9/10: n :~ {1 : 1 + n} | | 1/10: Skip | | Tick(9) | | NonDet | | {2:While(y ≥ 100) | | Choice | | 1/2: y :~ {1 : -100 + y} | | 1/2: y :~ {1 : -90 + y} | | Tick(5)} | | {Skip} | | y :~ {1 : 1000 + y} | | | +- [f] | | 0 | | | +- Expected Cost Body | | | | | +- Expected Cost | | | | | | | +- [f] | | | | 0 | | | | | | | +- [Program] | | | | NonDet | | | | {2:While(y ≥ 100) | | | | Choice | | | | 1/2: y :~ {1 : -100 + y} | | | | 1/2: y :~ {1 : -90 + y} | | | | Tick(5)} | | | | {Skip} | | | | | | | +- While.step | | | | | | | | | +- [Problem] | | | | | 2:While(y ≥ 100) | | | | | Choice | | | | | 1/2: y :~ {1 : -100 + y} | | | | | 1/2: y :~ {1 : -90 + y} | | | | | Tick(5) | | | | | | | | | +- [f] | | | | | 0 | | | | | | | | | +- Expected Cost Body | | | | | | | | | | | `- 5 | | | | | | | | | +- linear-template | | | | | | | | | | | `- 1 + [-99 + y | -99 + y ≥ 0] | | | | | | | | | +- [Norms] | | | | | [[1 | ⊤],[-99 + y | -99 + y ≥ 0]] | | | | | | | | | +- [Invariant] | | | | | y ≥ 100 ==> 5 + h([1 | ⊤],1/2·[-199 + y | -199 + y ≥ 0] + 1/2·[-189 + y | -189 + y ≥ 0]) ≼ h([1 | ⊤],[-99 + y | -99 + y ≥ 0]) | | | | | 100 ≥ 1 + y ==> 0 ≼ h([1 | ⊤],[-99 + y | -99 + y ≥ 0]) | | | | | | | | | `- 5·[-99 + y | -99 + y ≥ 0] | | | | | | | `- 5·[-99 + y | -99 + y ≥ 0] | | | | | +- Expected Cost | | | | | | | +- [f] | | | | 0 | | | | | | | +- [Program] | | | | y :~ {1 : 1000 + y} | | | | | | | `- 0 | | | | | +- Expected Cost | | | | | | | +- [f] | | | | 0 | | | | | | | +- [Program] | | | | NonDet | | | | {2:While(y ≥ 100) | | | | Choice | | | | 1/2: y :~ {1 : -100 + y} | | | | 1/2: y :~ {1 : -90 + y} | | | | Tick(5)} | | | | {Skip} | | | | | | | `- 0 | | | | | `- 81/10 + 9/2·[-99 + y | -99 + y ≥ 0] + 9/10 + 1/2·[-99 + y | -99 + y ≥ 0] | | | +- mixed-lin-template | | | | | `- 1 + 2·([-99 + y | -99 + y ≥ 0]) + 2·([-99 + y | -99 + y ≥ 0]·[-n | -n ≥ 0]) + 2·([-n | -n ≥ 0]) + [-n | -n ≥ 0]^2 | | | +- [Norms] | | [[1 | ⊤],[-99 + y | -99 + y ≥ 0],[99·(n) + -n·y | -99 + y ≥ 0 ∧ -n ≥ 0],[-n | -n ≥ 0],[n^2 | -n ≥ 0]] | | | +- While.step | | | | | +- [Problem] | | | 2:While(y ≥ 100) | | | Choice | | | 1/2: y :~ {1 : -100 + y} | | | 1/2: y :~ {1 : -90 + y} | | | Tick(5) | | | | | +- [f] | | | [-901·(n) + -n·y | 901 + y ≥ 0 ∧ -n ≥ 0] | | | | | +- linear-template | | | | | | | `- 1 + [-99 + y | -99 + y ≥ 0] + [-99 + y | -99 + y ≥ 0]·[100·(n) | 100·(n) ≥ 0] + [-901·(n) + -n·y | 901 + y ≥ 0 ∧ -n ≥ 0] | | | | | +- [Norms] | | | [[1 | ⊤],[-99 + y | -99 + y ≥ 0],[-9900·(n) + 100·(n·y) | -99 + y ≥ 0 ∧ 100·(n) ≥ 0],[-901·(n) + -n·y | 901 + y ≥ 0 ∧ -n ≥ 0]] | | | | | +- [Invariant] | | | y ≥ 100 ==> 0 + h([1 | ⊤],1/2·[-199 + y | -199 + y ≥ 0] + 1/2·[-189 + y | -189 + y ≥ 0],50·[-199·(n) + n·y | -199 + y ≥ 0 ∧ 100·(n) ≥ 0] + 50·[-189·(n) + n·y | -189 + y ≥ 0 ∧ 100·(n) ≥ 0],1/2·[-801·(n) + -n·y | 801 + y ≥ 0 ∧ -n ≥ 0] + 1/2·[-811·(n) + -n·y | 811 + y ≥ 0 ∧ -n ≥ 0]) ≼ h([1 | ⊤],[-99 + y | -99 + y ≥ 0],[-9900·(n) + 100·(n·y) | -99 + y ≥ 0 ∧ 100·(n) ≥ 0],[-901·(n) + -n·y | 901 + y ≥ 0 ∧ -n ≥ 0]) | | | 100 ≥ 1 + y ==> [-901·(n) + -n·y | 901 + y ≥ 0 ∧ -n ≥ 0] ≼ h([1 | ⊤],[-99 + y | -99 + y ≥ 0],[-9900·(n) + 100·(n·y) | -99 + y ≥ 0 ∧ 100·(n) ≥ 0],[-901·(n) + -n·y | 901 + y ≥ 0 ∧ -n ≥ 0]) | | | | | `- [-901·(n) + -n·y | 901 + y ≥ 0 ∧ -n ≥ 0] | | | +- [Invariant] | | 0 ≥ 1 + n ==> 81/10 + 9/2·[-99 + y | -99 + y ≥ 0] + 9/10 + 1/2·[-99 + y | -99 + y ≥ 0] + h([1 | ⊤],sup(900,9/10·[901 + y | 901 + y ≥ 0]) + sup(100,1/10·[901 + y | 901 + y ≥ 0]),9/10·[-901 + -901·(n) + -n·y + -y | -1 + -n ≥ 0 ∧ 901 + y ≥ 0] + 1/10·[-901·(n) + -n·y | 901 + y ≥ 0 ∧ -n ≥ 0],-9/10·[1 + n | -1 + -n ≥ 0] + -1/10·[n | -n ≥ 0],9/10·[1 + 2·(n) + n^2 | -1 + -n ≥ 0] + 1/10·[n^2 | -n ≥ 0]) ≼ h([1 | ⊤],[-99 + y | -99 + y ≥ 0],[99·(n) + -n·y | -99 + y ≥ 0 ∧ -n ≥ 0],[-n | -n ≥ 0],[n^2 | -n ≥ 0]) | | 1 + n ≥ 1 ==> 0 ≼ h([1 | ⊤],[-99 + y | -99 + y ≥ 0],[99·(n) + -n·y | -99 + y ≥ 0 ∧ -n ≥ 0],[-n | -n ≥ 0],[n^2 | -n ≥ 0]) | | | `- 50/9·[99·(n) + -n·y | -99 + y ≥ 0 ∧ -n ≥ 0] + 250000/81·[n^2 | -n ≥ 0] | `- [y ≥ 0] · (50/9·[99·(n) + -n·y | -99 + y ≥ 0 ∧ -n ≥ 0] + 250000/81·[n^2 | -n ≥ 0])