Expected Cost | +- [f] | 0 | +- [Program] | fast :~ {1 : 10} | medium :~ {1 : 3} | slow :~ {1 : 1} | volMeasured :~ {1 : 0} | r :~ {1/2 : 0;1/2 : 1} | volMeasured :~ {1 : r + volMeasured} | 0:While(volToFill ≥ volMeasured) | 1:If(fast + volMeasured ≥ 1 + volToFill) Then | r :~ {1/2 : 9;1/2 : 10} | volMeasured :~ {1 : r + volMeasured} | Else | 2:If(medium + volMeasured ≥ 1 + volToFill) Then | r :~ {1/3 : 2;1/3 : 3;1/3 : 4} | volMeasured :~ {1 : r + volMeasured} | Else | r :~ {1/3 : 0;1/3 : 1;1/3 : 2} | volMeasured :~ {1 : r + volMeasured} | r :~ {1/2 : 0;1/2 : 1} | volMeasured :~ {1 : r + volMeasured} | Tick(1) | +- While.step | | | +- [Problem] | | 0:While(volToFill ≥ volMeasured) | | 1:If(fast + volMeasured ≥ 1 + volToFill) Then | | r :~ {1/2 : 9;1/2 : 10} | | volMeasured :~ {1 : r + volMeasured} | | Else | | 2:If(medium + volMeasured ≥ 1 + volToFill) Then | | r :~ {1/3 : 2;1/3 : 3;1/3 : 4} | | volMeasured :~ {1 : r + volMeasured} | | Else | | r :~ {1/3 : 0;1/3 : 1;1/3 : 2} | | volMeasured :~ {1 : r + volMeasured} | | r :~ {1/2 : 0;1/2 : 1} | | volMeasured :~ {1 : r + volMeasured} | | Tick(1) | | | +- [f] | | 0 | | | +- Expected Cost Body | | | | | `- [1 | ⊤] | | | +- linear-template | | | | | `- 1 + [1 + -volMeasured + volToFill | 1 + -volMeasured + volToFill ≥ 0] | | | +- [Norms] | | [[1 | ⊤],[1 + -volMeasured + volToFill | 1 + -volMeasured + volToFill ≥ 0]] | | | +- [Invariant] | | volToFill ≥ volMeasured ==> [1 | ⊤] + h([1 | ⊤],ite(fast + volMeasured ≥ 1 + volToFill,1/4·[-8 + -volMeasured + volToFill | -8 + -volMeasured + volToFill ≥ 0] + 1/4·[-9 + -volMeasured + volToFill | -9 + -volMeasured + volToFill ≥ 0] + 1/4·[-9 + -volMeasured + volToFill | -9 + -volMeasured + volToFill ≥ 0] + 1/4·[-10 + -volMeasured + volToFill | -10 + -volMeasured + volToFill ≥ 0],ite(medium + volMeasured ≥ 1 + volToFill,1/6·[-1 + -volMeasured + volToFill | -1 + -volMeasured + volToFill ≥ 0] + 1/6·[-2 + -volMeasured + volToFill | -2 + -volMeasured + volToFill ≥ 0] + 1/6·[-2 + -volMeasured + volToFill | -2 + -volMeasured + volToFill ≥ 0] + 1/6·[-3 + -volMeasured + volToFill | -3 + -volMeasured + volToFill ≥ 0] + 1/6·[-3 + -volMeasured + volToFill | -3 + -volMeasured + volToFill ≥ 0] + 1/6·[-4 + -volMeasured + volToFill | -4 + -volMeasured + volToFill ≥ 0],1/6·[1 + -volMeasured + volToFill | 1 + -volMeasured + volToFill ≥ 0] + 1/6·[-volMeasured + volToFill | -volMeasured + volToFill ≥ 0] + 1/6·[-volMeasured + volToFill | -volMeasured + volToFill ≥ 0] + 1/6·[-1 + -volMeasured + volToFill | -1 + -volMeasured + volToFill ≥ 0] + 1/6·[-1 + -volMeasured + volToFill | -1 + -volMeasured + volToFill ≥ 0] + 1/6·[-2 + -volMeasured + volToFill | -2 + -volMeasured + volToFill ≥ 0]))) ≼ h([1 | ⊤],[1 + -volMeasured + volToFill | 1 + -volMeasured + volToFill ≥ 0]) | | volMeasured ≥ 1 + volToFill ==> 0 ≼ h([1 | ⊤],[1 + -volMeasured + volToFill | 1 + -volMeasured + volToFill ≥ 0]) | | | `- 6/5·[1 + -volMeasured + volToFill | 1 + -volMeasured + volToFill ≥ 0] | `- 3/5·[1 + volToFill | 1 + volToFill ≥ 0] + 3/5·[volToFill | volToFill ≥ 0]