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

[Success] 29/3
Degree: 0