ExecutionLog | `- Expected Cost | +- [f] | 0 | +- [Program] | fast :~ {1 : 10} | medium :~ {1 : 3} | slow :~ {1 : 1} | volMeasured :~ {1 : 0} | sample :~ {1/2 : 0;1/2 : 1} | volMeasured :~ {1 : sample + volMeasured} | 0:While(volToFill volMeasured) | 1:If(fast + volMeasured 1 + volToFill) Then | sample :~ {1/2 : 9;1/2 : 10} | volMeasured :~ {1 : sample + volMeasured} | Else | 2:If(medium + volMeasured 1 + volToFill) Then | sample :~ {1/3 : 2;1/3 : 3;1/3 : 4} | volMeasured :~ {1 : sample + volMeasured} | Else | sample :~ {1/3 : 0;1/3 : 1;1/3 : 2} | volMeasured :~ {1 : sample + volMeasured} | sample :~ {1/2 : 0;1/2 : 1} | volMeasured :~ {1 : sample + volMeasured} | Tick(1) | +- While.step | | | +- [Problem] | | 0:While(volToFill volMeasured) | | 1:If(fast + volMeasured 1 + volToFill) Then | | sample :~ {1/2 : 9;1/2 : 10} | | volMeasured :~ {1 : sample + volMeasured} | | Else | | 2:If(medium + volMeasured 1 + volToFill) Then | | sample :~ {1/3 : 2;1/3 : 3;1/3 : 4} | | volMeasured :~ {1 : sample + volMeasured} | | Else | | sample :~ {1/3 : 0;1/3 : 1;1/3 : 2} | | volMeasured :~ {1 : sample + volMeasured} | | sample :~ {1/2 : 0;1/2 : 1} | | volMeasured :~ {1 : sample + 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] [Success] 3/5[1 + volToFill | 1 + volToFill 0] + 3/5[volToFill | volToFill 0] Degree: 1