Expected Cost
|
+- [f]
|    0
|
+- [Program]
|    0:While(x ≥ 1)
|        Tick(1)
|        x :~ {1 : -1 + x}
|        NonDet
|          {y :~ {1 : 1 + y}}
|          {1:While(y ≥ 1)
|               Tick(1)
|               y :~ {1 : -1 + y}}
|
+- While.step
|  |
|  +- [Problem]
|  |    0:While(x ≥ 1)
|  |        Tick(1)
|  |        x :~ {1 : -1 + x}
|  |        NonDet
|  |          {y :~ {1 : 1 + y}}
|  |          {1:While(y ≥ 1)
|  |               Tick(1)
|  |               y :~ {1 : -1 + y}}
|  |
|  +- [f]
|  |    0
|  |
|  +- Expected Cost Body
|  |  |
|  |  +- While.step
|  |  |  |
|  |  |  +- [Problem]
|  |  |  |    1:While(y ≥ 1)
|  |  |  |        Tick(1)
|  |  |  |        y :~ {1 : -1 + y}
|  |  |  |
|  |  |  +- [f]
|  |  |  |    0
|  |  |  |
|  |  |  +- Expected Cost Body
|  |  |  |  |
|  |  |  |  `- [1 | ⊤]
|  |  |  |
|  |  |  +- linear-template
|  |  |  |  |
|  |  |  |  `- 1 + [y | y ≥ 0]
|  |  |  |
|  |  |  +- [Norms]
|  |  |  |    [[1 | ⊤],[y | y ≥ 0]]
|  |  |  |
|  |  |  +- [Invariant]
|  |  |  |    y ≥ 1 ==> [1 | ⊤] + h([1 | ⊤],[-1 + y | -1 + y ≥ 0]) ≼ h([1 | ⊤],[y | y ≥ 0])
|  |  |  |    1 ≥ 1 + y ==> 0 ≼ h([1 | ⊤],[y | y ≥ 0])
|  |  |  |
|  |  |  `- [y | y ≥ 0]
|  |  |
|  |  `- [1 | ⊤] + [y | y ≥ 0]
|  |
|  +- mixed-lin-template
|  |  |
|  |  `- 1 + 2·([x | x ≥ 0]) + [x | x ≥ 0]·[y | y ≥ 0] + [x | x ≥ 0]^2 + [y | y ≥ 0]
|  |
|  +- [Norms]
|  |    [[1 | ⊤],[x | x ≥ 0],[x·y | x ≥ 0 ∧  y ≥ 0],[x^2 | x ≥ 0],[y | y ≥ 0]]
|  |
|  +- While.step
|  |  |
|  |  +- [Problem]
|  |  |    1:While(y ≥ 1)
|  |  |        Tick(1)
|  |  |        y :~ {1 : -1 + y}
|  |  |
|  |  +- [f]
|  |  |    [x·y | x ≥ 0 ∧  y ≥ 0]
|  |  |
|  |  +- linear-template
|  |  |  |
|  |  |  `- 1 + [-x | -x ≥ 0]·[y | y ≥ 0] + [x·y | x ≥ 0 ∧  y ≥ 0] + [y | y ≥ 0]
|  |  |
|  |  +- [Norms]
|  |  |    [[1 | ⊤],[-x·y | -x ≥ 0 ∧  y ≥ 0],[x·y | x ≥ 0 ∧  y ≥ 0],[y | y ≥ 0]]
|  |  |
|  |  +- [Invariant]
|  |  |    y ≥ 1 ==> 0 + h([1 | ⊤],-1·[-x + x·y | -1 + y ≥ 0 ∧  -x ≥ 0],[-x + x·y | -1 + y ≥ 0 ∧  x ≥ 0],[-1 + y | -1 + y ≥ 0]) ≼ h([1 | ⊤],[-x·y | -x ≥ 0 ∧  y ≥ 0],[x·y | x ≥ 0 ∧  y ≥ 0],[y | y ≥ 0])
|  |  |    1 ≥ 1 + y ==> [x·y | x ≥ 0 ∧  y ≥ 0] ≼ h([1 | ⊤],[-x·y | -x ≥ 0 ∧  y ≥ 0],[x·y | x ≥ 0 ∧  y ≥ 0],[y | y ≥ 0])
|  |  |
|  |  `- [x·y | x ≥ 0 ∧  y ≥ 0]
|  |
|  +- [Invariant]
|  |    x ≥ 1 ==> [1 | ⊤] + [y | y ≥ 0] + h([1 | ⊤],[-1 + x | -1 + x ≥ 0],sup([-1 + x + x·y + -y | -1 + x ≥ 0 ∧  1 + y ≥ 0],[x·y + -y | -1 + x ≥ 0 ∧  y ≥ 0]),[1 + -2·(x) + x^2 | -1 + x ≥ 0],[1 + y | 1 + y ≥ 0]) ≼ h([1 | ⊤],[x | x ≥ 0],[x·y | x ≥ 0 ∧  y ≥ 0],[x^2 | x ≥ 0],[y | y ≥ 0])
|  |    1 ≥ 1 + x ==> 0 ≼ h([1 | ⊤],[x | x ≥ 0],[x·y | x ≥ 0 ∧  y ≥ 0],[x^2 | x ≥ 0],[y | y ≥ 0])
|  |
|  `- 1/2·[x | x ≥ 0] + [x·y | x ≥ 0 ∧  y ≥ 0] + 1/2·[x^2 | x ≥ 0]
|
`- 1/2·[x | x ≥ 0] + [x·y | x ≥ 0 ∧  y ≥ 0] + 1/2·[x^2 | x ≥ 0]