ExecutionLog
|
`- Expected Cost
   |
   +- [f]
   |    0
   |
   +- [Program]
   |    0:While(l  8)
   |        sample :~ {1/3 : 6;1/3 : 7;1/3 : 8}
   |        l :~ {1 : l + -sample}
   |        Tick(10)
   |    1:While(l  1)
   |        l :~ {1 : -1 + l}
   |        Tick(1)
   |
   +- Expected Cost
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- [Program]
   |  |    0:While(l  8)
   |  |        sample :~ {1/3 : 6;1/3 : 7;1/3 : 8}
   |  |        l :~ {1 : l + -sample}
   |  |        Tick(10)
   |  |
   |  +- While.step
   |  |  |
   |  |  +- [Problem]
   |  |  |    0:While(l  8)
   |  |  |        sample :~ {1/3 : 6;1/3 : 7;1/3 : 8}
   |  |  |        l :~ {1 : l + -sample}
   |  |  |        Tick(10)
   |  |  |
   |  |  +- [f]
   |  |  |    0
   |  |  |
   |  |  +- Expected Cost Body
   |  |  |  |
   |  |  |  `- 10
   |  |  |
   |  |  +- linear-template
   |  |  |  |
   |  |  |  `- 1 + [-7 + l | -7 + l  0]
   |  |  |
   |  |  +- [Norms]
   |  |  |    [[1 | ],[-7 + l | -7 + l  0]]
   |  |  |
   |  |  +- [Invariant]
   |  |  |    l  8 ==> 10 + h([1 | ],1/3[-13 + l | -13 + l  0] + 1/3[-14 + l | -14 + l  0] + 1/3[-15 + l | -15 + l  0])  h([1 | ],[-7 + l | -7 + l  0])
   |  |  |    8  1 + l ==> 0  h([1 | ],[-7 + l | -7 + l  0])
   |  |  |
   |  |  `- 10[-7 + l | -7 + l  0]
   |  |
   |  `- 10[-7 + l | -7 + l  0]
   |
   +- Expected Cost
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- [Program]
   |  |    1:While(l  1)
   |  |        l :~ {1 : -1 + l}
   |  |        Tick(1)
   |  |
   |  +- While.step
   |  |  |
   |  |  +- [Problem]
   |  |  |    1:While(l  1)
   |  |  |        l :~ {1 : -1 + l}
   |  |  |        Tick(1)
   |  |  |
   |  |  +- [f]
   |  |  |    0
   |  |  |
   |  |  +- Expected Cost Body
   |  |  |  |
   |  |  |  `- [1 | ]
   |  |  |
   |  |  +- linear-template
   |  |  |  |
   |  |  |  `- 1 + [l | l  0]
   |  |  |
   |  |  +- [Norms]
   |  |  |    [[1 | ],[l | l  0]]
   |  |  |
   |  |  +- [Invariant]
   |  |  |    l  1 ==> [1 | ] + h([1 | ],[-1 + l | -1 + l  0])  h([1 | ],[l | l  0])
   |  |  |    1  1 + l ==> 0  h([1 | ],[l | l  0])
   |  |  |
   |  |  `- [l | l  0]
   |  |
   |  `- [l | l  0]
   |
   +- Expected Cost
   |  |
   |  +- [f]
   |  |    [l | l  0]
   |  |
   |  +- [Program]
   |  |    0:While(l  8)
   |  |        sample :~ {1/3 : 6;1/3 : 7;1/3 : 8}
   |  |        l :~ {1 : l + -sample}
   |  |        Tick(10)
   |  |
   |  +- While.step
   |  |  |
   |  |  +- [Problem]
   |  |  |    0:While(l  8)
   |  |  |        sample :~ {1/3 : 6;1/3 : 7;1/3 : 8}
   |  |  |        l :~ {1 : l + -sample}
   |  |  |        Tick(10)
   |  |  |
   |  |  +- [f]
   |  |  |    [l | l  0]
   |  |  |
   |  |  +- linear-template
   |  |  |  |
   |  |  |  `- 1 + 2([-7 + l | -7 + l  0]) + [l | l  0]
   |  |  |
   |  |  +- [Norms]
   |  |  |    [[1 | ],[-7 + l | -7 + l  0],[l | l  0]]
   |  |  |
   |  |  +- [Invariant]
   |  |  |    l  8 ==> 0 + h([1 | ],1/3[-13 + l | -13 + l  0] + 1/3[-14 + l | -14 + l  0] + 1/3[-15 + l | -15 + l  0],1/3[-6 + l | -6 + l  0] + 1/3[-7 + l | -7 + l  0] + 1/3[-8 + l | -8 + l  0])  h([1 | ],[-7 + l | -7 + l  0],[l | l  0])
   |  |  |    8  1 + l ==> [l | l  0]  h([1 | ],[-7 + l | -7 + l  0],[l | l  0])
   |  |  |
   |  |  `- 7
   |  |
   |  `- 7
   |
   `- 10[-7 + l | -7 + l  0] + 7

[Success] 10[-7 + l | -7 + l
               0] + 7
Degree: 1