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

[Success] 2[1 + x | 1 + x  0]
Degree: 1