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

[Success] 2[n | n  0]
Degree: 1