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