ExecutionLog
|
`- Expected Cost
   |
   +- [f]
   |    0
   |
   +- [Program]
   |    0:While(n  3 + x)
   |        1:If(m  1 + y) Then
   |            Choice
   |              1/2: y :~ {1 : 1 + y}
   |              1/2: y :~ {1 : y}
   |          Else
   |            Choice
   |              1/4: x :~ {1 : x}
   |              3/4: Choice
   |                     1/3: x :~ {1 : 1 + x}
   |                     2/3: Choice
   |                            1/2: x :~ {1 : 2 + x}
   |                            1/2: x :~ {1 : 3 + x}
   |        Tick(1)
   |
   +- While.step
   |  |
   |  +- [Problem]
   |  |    0:While(n  3 + x)
   |  |        1:If(m  1 + y) Then
   |  |            Choice
   |  |              1/2: y :~ {1 : 1 + y}
   |  |              1/2: y :~ {1 : y}
   |  |          Else
   |  |            Choice
   |  |              1/4: x :~ {1 : x}
   |  |              3/4: Choice
   |  |                     1/3: x :~ {1 : 1 + x}
   |  |                     2/3: Choice
   |  |                            1/2: x :~ {1 : 2 + x}
   |  |                            1/2: x :~ {1 : 3 + x}
   |  |        Tick(1)
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- Expected Cost Body
   |  |  |
   |  |  `- [1 | ]
   |  |
   |  +- conditions-template
   |  |  |
   |  |  `- 1 + [-2 + n + -x | -2 + n + -x  0] + 4([1 + -m + y | 1 + -m + y  0]) + [m + -y | m + -y  0]
   |  |
   |  +- [Norms]
   |  |    [[1 | ],[-2 + n + -x | -2 + n + -x  0],[1 + -m + y | 1 + -m + y  0],[m + -y | m + -y  0]]
   |  |
   |  +- [Invariant]
   |  |    n  3 + x ==> [1 | ] + h([1 | ],ite(m  1 + y,[-2 + n + -x | -2 + n + -x  0],1/4[-2 + n + -x | -2 + n + -x  0] + 1/4[-3 + n + -x | -3 + n + -x  0] + 1/4[-4 + n + -x | -4 + n + -x  0] + 1/4[-5 + n + -x | -5 + n + -x  0]),ite(m  1 + y,1/2[2 + -m + y | 2 + -m + y  0] + 1/2[1 + -m + y | 1 + -m + y  0],[1 + -m + y | 1 + -m + y  0]),ite(m  1 + y,1/2[-1 + m + -y | -1 + m + -y  0] + 1/2[m + -y | m + -y  0],[m + -y | m + -y  0]))  h([1 | ],[-2 + n + -x | -2 + n + -x  0],[1 + -m + y | 1 + -m + y  0],[m + -y | m + -y  0])
   |  |    3 + x  1 + n ==> 0  h([1 | ],[-2 + n + -x | -2 + n + -x  0],[1 + -m + y | 1 + -m + y  0],[m + -y | m + -y  0])
   |  |
   |  `- 4/3[-2 + n + -x | -2 + n + -x  0] + 2[m + -y | m + -y  0]
   |
   `- 4/3[-2 + n + -x | -2 + n + -x  0] + 2[m + -y | m + -y  0]

[Success] 4/3[-2 + n + -x | -2
                + n + -x  0] + 2[m + -y | m
                                    + -y  0]
Degree: 1