ExecutionLog
|
`- Expected Cost
   |
   +- [f]
   |    0
   |
   +- [Program]
   |    Tick(1)
   |    0:While(x  1)
   |        s :~ {1 : y}
   |        Choice
   |          1/2: x :~ {1 : x}
   |          1/2: x :~ {1 : -1 + x}
   |        Tick(1)
   |        1:While(y  1 + x)
   |            y :~ {1 : -1 + y}
   |            Tick(1)
   |        y :~ {1 : s}
   |        Tick(1)
   |
   +- While.step
   |  |
   |  +- [Problem]
   |  |    0:While(x  1)
   |  |        s :~ {1 : y}
   |  |        Choice
   |  |          1/2: x :~ {1 : x}
   |  |          1/2: x :~ {1 : -1 + x}
   |  |        Tick(1)
   |  |        1:While(y  1 + x)
   |  |            y :~ {1 : -1 + y}
   |  |            Tick(1)
   |  |        y :~ {1 : s}
   |  |        Tick(1)
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- Expected Cost Body
   |  |  |
   |  |  +- Expected Cost
   |  |  |  |
   |  |  |  +- [f]
   |  |  |  |    0
   |  |  |  |
   |  |  |  +- [Program]
   |  |  |  |    1:While(y  1 + x)
   |  |  |  |        y :~ {1 : -1 + y}
   |  |  |  |        Tick(1)
   |  |  |  |
   |  |  |  +- While.step
   |  |  |  |  |
   |  |  |  |  +- [Problem]
   |  |  |  |  |    1:While(y  1 + x)
   |  |  |  |  |        y :~ {1 : -1 + y}
   |  |  |  |  |        Tick(1)
   |  |  |  |  |
   |  |  |  |  +- [f]
   |  |  |  |  |    0
   |  |  |  |  |
   |  |  |  |  +- Expected Cost Body
   |  |  |  |  |  |
   |  |  |  |  |  `- [1 | ]
   |  |  |  |  |
   |  |  |  |  +- linear-template
   |  |  |  |  |  |
   |  |  |  |  |  `- 1 + [-x + y | -x + y  0]
   |  |  |  |  |
   |  |  |  |  +- [Norms]
   |  |  |  |  |    [[1 | ],[-x + y | -x + y  0]]
   |  |  |  |  |
   |  |  |  |  +- [Invariant]
   |  |  |  |  |    y  1 + x ==> [1 | ] + h([1 | ],[-1 + -x + y | -1 + -x + y  0])  h([1 | ],[-x + y | -x + y  0])
   |  |  |  |  |    1 + x  1 + y ==> 0  h([1 | ],[-x + y | -x + y  0])
   |  |  |  |  |
   |  |  |  |  `- [-x + y | -x + y  0]
   |  |  |  |
   |  |  |  `- [-x + y | -x + y  0]
   |  |  |
   |  |  +- Expected Cost
   |  |  |  |
   |  |  |  +- [f]
   |  |  |  |    0
   |  |  |  |
   |  |  |  +- [Program]
   |  |  |  |    y :~ {1 : s}
   |  |  |  |    Tick(1)
   |  |  |  |
   |  |  |  `- [1 | ]
   |  |  |
   |  |  +- Expected Cost
   |  |  |  |
   |  |  |  +- [f]
   |  |  |  |    [1 | ]
   |  |  |  |
   |  |  |  +- [Program]
   |  |  |  |    1:While(y  1 + x)
   |  |  |  |        y :~ {1 : -1 + y}
   |  |  |  |        Tick(1)
   |  |  |  |
   |  |  |  `- [1 | ]
   |  |  |
   |  |  `- 1/2 + 1/2[-x + y | -x + y  0] + 1/2 + 1/2 + 1/2[1 + -x + y | 1 + -x + y  0] + 1/2
   |  |
   |  +- mixed-lin-template
   |  |  |
   |  |  `- 1 + [1 + -x + y | 1 + -x + y  0] + [1 + -x + y | 1 + -x + y  0][x | x  0] + [-x + y | -x + y  0] + [-x + y | -x + y  0][x | x  0] + 2([x | x  0]) + [x | x  0]^2
   |  |
   |  +- [Norms]
   |  |    [[1 | ],[1 + -x + y | 1 + -x + y  0],[x + xy + -x^2 | 1 + -x + y  0   x  0],[-x + y | -x + y  0],[xy + -x^2 | -x + y  0   x  0],[x | x  0],[x^2 | x  0]]
   |  |
   |  +- [Invariant]
   |  |    x  1 ==> 1/2 + 1/2[-x + y | -x + y  0] + 1/2 + 1/2 + 1/2[1 + -x + y | 1 + -x + y  0] + 1/2 + h([1 | ],1/2[1 + -x + y | 1 + -x + y  0] + 1/2[2 + -x + y | 2 + -x + y  0],1/2[x + xy + -x^2 | 1 + -x + y  0   x  0] + 1/2[-2 + 3(x) + xy + -x^2 + -y | -1 + x  0   2 + -x + y  0],1/2[-x + y | -x + y  0] + 1/2[1 + -x + y | 1 + -x + y  0],1/2[xy + -x^2 | -x + y  0   x  0] + 1/2[-1 + 2(x) + xy + -x^2 + -y | -1 + x  0   1 + -x + y  0],1/2[x | x  0] + 1/2[-1 + x | -1 + x  0],1/2[x^2 | x  0] + 1/2[1 + -2(x) + x^2 | -1 + x  0])  h([1 | ],[1 + -x + y | 1 + -x + y  0],[x + xy + -x^2 | 1 + -x + y  0   x  0],[-x + y | -x + y  0],[xy + -x^2 | -x + y  0   x  0],[x | x  0],[x^2 | x  0])
   |  |    1  1 + x ==> 0  h([1 | ],[1 + -x + y | 1 + -x + y  0],[x + xy + -x^2 | 1 + -x + y  0   x  0],[-x + y | -x + y  0],[xy + -x^2 | -x + y  0   x  0],[x | x  0],[x^2 | x  0])
   |  |
   |  `- 2[xy + -x^2 | -x + y  0   x  0] + 4[x | x  0] + [x^2 | x  0]
   |
   `- [1 | ] + 2[xy + -x^2 | -x + y  0   x  0] + 4[x | x  0] + [x^2 | x  0]

[Success] [1 | ] + 2[xy
                        + -x^2 | -x + y  0   x  0]
                     + 4[x | x  0] + [x^2 | x  0]
Degree: 2