ExecutionLog
|
`- Expected Cost
   |
   +- [f]
   |    0
   |
   +- [Program]
   |    0:If(y  10) Then
   |        Skip
   |      Else
   |        Abort
   |    1:While(x + -y  3)
   |        sample :~ {1/16 : 0;4/16 : 1;6/16 : 2;4/16 : 3;1/16 : 4}
   |        y :~ {1 : sample + y}
   |        Tick(3)
   |    2:While(y  10)
   |        Choice
   |          2/3: y :~ {1 : -10 + y}
   |          1/3: y :~ {1 : y}
   |        Tick(1)
   |
   +- Expected Cost
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- [Program]
   |  |    1:While(x + -y  3)
   |  |        sample :~ {1/16 : 0;4/16 : 1;6/16 : 2;4/16 : 3;1/16 : 4}
   |  |        y :~ {1 : sample + y}
   |  |        Tick(3)
   |  |
   |  +- While.step
   |  |  |
   |  |  +- [Problem]
   |  |  |    1:While(x + -y  3)
   |  |  |        sample :~ {1/16 : 0;4/16 : 1;6/16 : 2;4/16 : 3;1/16 : 4}
   |  |  |        y :~ {1 : sample + y}
   |  |  |        Tick(3)
   |  |  |
   |  |  +- [f]
   |  |  |    0
   |  |  |
   |  |  +- Expected Cost Body
   |  |  |  |
   |  |  |  `- 3
   |  |  |
   |  |  +- linear-template
   |  |  |  |
   |  |  |  `- 1 + [-2 + x + -y | -2 + x + -y  0]
   |  |  |
   |  |  +- [Norms]
   |  |  |    [[1 | ],[-2 + x + -y | -2 + x + -y  0]]
   |  |  |
   |  |  +- [Invariant]
   |  |  |    x + -y  3 ==> 3 + h([1 | ],1/16[-2 + x + -y | -2 + x + -y  0] + 1/4[-3 + x + -y | -3 + x + -y  0] + 3/8[-4 + x + -y | -4 + x + -y  0] + 1/4[-5 + x + -y | -5 + x + -y  0] + 1/16[-6 + x + -y | -6 + x + -y  0])  h([1 | ],[-2 + x + -y | -2 + x + -y  0])
   |  |  |    3  1 + x + -y ==> 0  h([1 | ],[-2 + x + -y | -2 + x + -y  0])
   |  |  |
   |  |  `- 16/5[-2 + x + -y | -2 + x + -y  0]
   |  |
   |  `- 16/5[-2 + x + -y | -2 + x + -y  0]
   |
   +- Expected Cost
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- [Program]
   |  |    2:While(y  10)
   |  |        Choice
   |  |          2/3: y :~ {1 : -10 + y}
   |  |          1/3: y :~ {1 : y}
   |  |        Tick(1)
   |  |
   |  +- While.step
   |  |  |
   |  |  +- [Problem]
   |  |  |    2:While(y  10)
   |  |  |        Choice
   |  |  |          2/3: y :~ {1 : -10 + y}
   |  |  |          1/3: y :~ {1 : y}
   |  |  |        Tick(1)
   |  |  |
   |  |  +- [f]
   |  |  |    0
   |  |  |
   |  |  +- Expected Cost Body
   |  |  |  |
   |  |  |  `- [1 | ]
   |  |  |
   |  |  +- linear-template
   |  |  |  |
   |  |  |  `- 1 + [-9 + y | -9 + y  0]
   |  |  |
   |  |  +- [Norms]
   |  |  |    [[1 | ],[-9 + y | -9 + y  0]]
   |  |  |
   |  |  +- [Invariant]
   |  |  |    y  10 ==> [1 | ] + h([1 | ],2/3[-19 + y | -19 + y  0] + 1/3[-9 + y | -9 + y  0])  h([1 | ],[-9 + y | -9 + y  0])
   |  |  |    10  1 + y ==> 0  h([1 | ],[-9 + y | -9 + y  0])
   |  |  |
   |  |  `- 3/2[-9 + y | -9 + y  0]
   |  |
   |  `- 3/2[-9 + y | -9 + y  0]
   |
   +- Expected Cost
   |  |
   |  +- [f]
   |  |    3/2[-9 + y | -9 + y  0]
   |  |
   |  +- [Program]
   |  |    1:While(x + -y  3)
   |  |        sample :~ {1/16 : 0;4/16 : 1;6/16 : 2;4/16 : 3;1/16 : 4}
   |  |        y :~ {1 : sample + y}
   |  |        Tick(3)
   |  |
   |  +- While.step
   |  |  |
   |  |  +- [Problem]
   |  |  |    1:While(x + -y  3)
   |  |  |        sample :~ {1/16 : 0;4/16 : 1;6/16 : 2;4/16 : 3;1/16 : 4}
   |  |  |        y :~ {1 : sample + y}
   |  |  |        Tick(3)
   |  |  |
   |  |  +- [f]
   |  |  |    3/2[-9 + y | -9 + y  0]
   |  |  |
   |  |  +- linear-template
   |  |  |  |
   |  |  |  `- 1 + [-9 + y | -9 + y  0] + 2([-2 + x + -y | -2 + x + -y  0])
   |  |  |
   |  |  +- [Norms]
   |  |  |    [[1 | ],[-9 + y | -9 + y  0],[-2 + x + -y | -2 + x + -y  0]]
   |  |  |
   |  |  +- [Invariant]
   |  |  |    x + -y  3 ==> 0 + h([1 | ],1/16[-9 + y | -9 + y  0] + 1/4[-8 + y | -8 + y  0] + 3/8[-7 + y | -7 + y  0] + 1/4[-6 + y | -6 + y  0] + 1/16[-5 + y | -5 + y  0],1/16[-2 + x + -y | -2 + x + -y  0] + 1/4[-3 + x + -y | -3 + x + -y  0] + 3/8[-4 + x + -y | -4 + x + -y  0] + 1/4[-5 + x + -y | -5 + x + -y  0] + 1/16[-6 + x + -y | -6 + x + -y  0])  h([1 | ],[-9 + y | -9 + y  0],[-2 + x + -y | -2 + x + -y  0])
   |  |  |    3  1 + x + -y ==> 3/2[-9 + y | -9 + y  0]  h([1 | ],[-9 + y | -9 + y  0],[-2 + x + -y | -2 + x + -y  0])
   |  |  |
   |  |  `- 3/2[-9 + y | -9 + y  0] + 16/5[-2 + x + -y | -2 + x + -y  0]
   |  |
   |  `- 3/2[-9 + y | -9 + y  0] + 16/5[-2 + x + -y | -2 + x + -y  0]
   |
   `- [y  10]  (16/5[-2 + x + -y | -2 + x + -y  0] + 3/2[-9 + y | -9 + y  0] + 16/5[-2 + x + -y | -2 + x + -y  0])

[Success] [y  10]  (16/5[-2
                             + x + -y | -2 + x + -y  0]
                       + 3/2[-9 + y | -9 + y  0]
                          + 16/5[-2 + x + -y | -2 + x
                                   + -y  0])
Degree: 1