ExecutionLog
|
`- Expected Cost
   |
   +- [f]
   |    0
   |
   +- [Program]
   |    0:If(X  1) Then
   |        Skip
   |      Else
   |        Abort
   |    Tick(1)
   |    1:While(X  1)
   |        Choice
   |          1/2: X :~ {1 : X}
   |               Tick(1)
   |          1/2: Choice
   |                 1/2: X :~ {1 : 1 + X}
   |                 1/2: X :~ {1 : X}
   |               Tick(1)
   |               TEMP :~ {1 : 1}
   |               Y :~ {1 : 1}
   |               2:While(TEMP  1)
   |                   NonDet
   |                     {Y :~ {1 : 1 + Y}}
   |                     {TEMP :~ {1 : 0}}
   |               X :~ {1 : X + -Y}
   |               Tick(1)
   |
   +- While.step
   |  |
   |  +- [Problem]
   |  |    1:While(X  1)
   |  |        Choice
   |  |          1/2: X :~ {1 : X}
   |  |               Tick(1)
   |  |          1/2: Choice
   |  |                 1/2: X :~ {1 : 1 + X}
   |  |                 1/2: X :~ {1 : X}
   |  |               Tick(1)
   |  |               TEMP :~ {1 : 1}
   |  |               Y :~ {1 : 1}
   |  |               2:While(TEMP  1)
   |  |                   NonDet
   |  |                     {Y :~ {1 : 1 + Y}}
   |  |                     {TEMP :~ {1 : 0}}
   |  |               X :~ {1 : X + -Y}
   |  |               Tick(1)
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- Expected Cost Body
   |  |  |
   |  |  +- Expected Cost
   |  |  |  |
   |  |  |  +- [f]
   |  |  |  |    0
   |  |  |  |
   |  |  |  +- [Program]
   |  |  |  |    2:While(TEMP  1)
   |  |  |  |        NonDet
   |  |  |  |          {Y :~ {1 : 1 + Y}}
   |  |  |  |          {TEMP :~ {1 : 0}}
   |  |  |  |
   |  |  |  `- 0
   |  |  |
   |  |  +- Expected Cost
   |  |  |  |
   |  |  |  +- [f]
   |  |  |  |    0
   |  |  |  |
   |  |  |  +- [Program]
   |  |  |  |    X :~ {1 : X + -Y}
   |  |  |  |    Tick(1)
   |  |  |  |
   |  |  |  `- [1 | ]
   |  |  |
   |  |  +- Expected Cost
   |  |  |  |
   |  |  |  +- [f]
   |  |  |  |    [1 | ]
   |  |  |  |
   |  |  |  +- [Program]
   |  |  |  |    2:While(TEMP  1)
   |  |  |  |        NonDet
   |  |  |  |          {Y :~ {1 : 1 + Y}}
   |  |  |  |          {TEMP :~ {1 : 0}}
   |  |  |  |
   |  |  |  `- [1 | ]
   |  |  |
   |  |  `- 3/2
   |  |
   |  +- linear-template
   |  |  |
   |  |  `- 1 + [X | X  0]
   |  |
   |  +- [Norms]
   |  |    [[1 | ],[X | X  0]]
   |  |
   |  +- While.step
   |  |  |
   |  |  +- [Problem]
   |  |  |    2:While(TEMP  1)
   |  |  |        NonDet
   |  |  |          {Y :~ {1 : 1 + Y}}
   |  |  |          {TEMP :~ {1 : 0}}
   |  |  |
   |  |  +- [f]
   |  |  |    [X + -Y | X + -Y  0]
   |  |  |
   |  |  +- linear-template
   |  |  |  |
   |  |  |  `- 1 + 2([TEMP | TEMP  0]) + [X + -Y | X + -Y  0]
   |  |  |
   |  |  +- [Norms]
   |  |  |    [[1 | ],[TEMP | TEMP  0],[X + -Y | X + -Y  0]]
   |  |  |
   |  |  +- [Invariant]
   |  |  |    TEMP  1 ==> 0 + h([1 | ],[TEMP | TEMP  0],sup([-1 + X + -Y | -1 + X + -Y  0],[X + -Y | X + -Y  0]))  h([1 | ],[TEMP | TEMP  0],[X + -Y | X + -Y  0])
   |  |  |    1  1 + TEMP ==> [X + -Y | X + -Y  0]  h([1 | ],[TEMP | TEMP  0],[X + -Y | X + -Y  0])
   |  |  |
   |  |  `- [X + -Y | X + -Y  0]
   |  |
   |  +- [Invariant]
   |  |    X  1 ==> 3/2 + h([1 | ],1/2[X | X  0] + 1/4[X | X  0] + 1/4[-1 + X | -1 + X  0])  h([1 | ],[X | X  0])
   |  |    1  1 + X ==> 0  h([1 | ],[X | X  0])
   |  |
   |  `- 6[X | X  0]
   |
   `- [X  1]  ([1 | ] + 6[X | X  0])

[Success] [X  1]  ([1 | ]
                      + 6[X | X  0])
Degree: 1