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