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

[Success] 3/2[1 + -2(n) + n^2
               | -1 + n  0]
Degree: 2