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

[Success] 5
Degree: 0