ExecutionLog
|
`- Expected Cost
   |
   +- [f]
   |    0
   |
   +- [Program]
   |    0:While(n  1)
   |        h :~ {1 : 0}
   |        t :~ {1 : m}
   |        1:While(t  h)
   |            Choice
   |              3/4: sample :~ {1/3 : 1;1/3 : 2;1/3 : 3}
   |                   h :~ {1 : h + sample}
   |              1/4: Skip
   |            t :~ {1 : 1 + t}
   |            Tick(1)
   |        n :~ {1 : -1 + n}
   |
   +- While.step
   |  |
   |  +- [Problem]
   |  |    0:While(n  1)
   |  |        h :~ {1 : 0}
   |  |        t :~ {1 : m}
   |  |        1:While(t  h)
   |  |            Choice
   |  |              3/4: sample :~ {1/3 : 1;1/3 : 2;1/3 : 3}
   |  |                   h :~ {1 : h + sample}
   |  |              1/4: Skip
   |  |            t :~ {1 : 1 + t}
   |  |            Tick(1)
   |  |        n :~ {1 : -1 + n}
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- Expected Cost Body
   |  |  |
   |  |  +- Expected Cost
   |  |  |  |
   |  |  |  +- [f]
   |  |  |  |    0
   |  |  |  |
   |  |  |  +- [Program]
   |  |  |  |    1:While(t  h)
   |  |  |  |        Choice
   |  |  |  |          3/4: sample :~ {1/3 : 1;1/3 : 2;1/3 : 3}
   |  |  |  |               h :~ {1 : h + sample}
   |  |  |  |          1/4: Skip
   |  |  |  |        t :~ {1 : 1 + t}
   |  |  |  |        Tick(1)
   |  |  |  |
   |  |  |  +- While.step
   |  |  |  |  |
   |  |  |  |  +- [Problem]
   |  |  |  |  |    1:While(t  h)
   |  |  |  |  |        Choice
   |  |  |  |  |          3/4: sample :~ {1/3 : 1;1/3 : 2;1/3 : 3}
   |  |  |  |  |               h :~ {1 : h + sample}
   |  |  |  |  |          1/4: Skip
   |  |  |  |  |        t :~ {1 : 1 + t}
   |  |  |  |  |        Tick(1)
   |  |  |  |  |
   |  |  |  |  +- [f]
   |  |  |  |  |    0
   |  |  |  |  |
   |  |  |  |  +- Expected Cost Body
   |  |  |  |  |  |
   |  |  |  |  |  `- [1 | ]
   |  |  |  |  |
   |  |  |  |  +- linear-template
   |  |  |  |  |  |
   |  |  |  |  |  `- 1 + [1 + -h + t | 1 + -h + t  0]
   |  |  |  |  |
   |  |  |  |  +- [Norms]
   |  |  |  |  |    [[1 | ],[1 + -h + t | 1 + -h + t  0]]
   |  |  |  |  |
   |  |  |  |  +- [Invariant]
   |  |  |  |  |    t  h ==> [1 | ] + h([1 | ],1/4[1 + -h + t | 1 + -h + t  0] + 1/4[-h + t | -h + t  0] + 1/4[-1 + -h + t | -1 + -h + t  0] + 1/4[2 + -h + t | 2 + -h + t  0])  h([1 | ],[1 + -h + t | 1 + -h + t  0])
   |  |  |  |  |    h  1 + t ==> 0  h([1 | ],[1 + -h + t | 1 + -h + t  0])
   |  |  |  |  |
   |  |  |  |  `- 4[1 + -h + t | 1 + -h + t  0]
   |  |  |  |
   |  |  |  `- 4[1 + -h + t | 1 + -h + t  0]
   |  |  |
   |  |  +- Expected Cost
   |  |  |  |
   |  |  |  +- [f]
   |  |  |  |    0
   |  |  |  |
   |  |  |  +- [Program]
   |  |  |  |    n :~ {1 : -1 + n}
   |  |  |  |
   |  |  |  `- 0
   |  |  |
   |  |  +- Expected Cost
   |  |  |  |
   |  |  |  +- [f]
   |  |  |  |    0
   |  |  |  |
   |  |  |  +- [Program]
   |  |  |  |    1:While(t  h)
   |  |  |  |        Choice
   |  |  |  |          3/4: sample :~ {1/3 : 1;1/3 : 2;1/3 : 3}
   |  |  |  |               h :~ {1 : h + sample}
   |  |  |  |          1/4: Skip
   |  |  |  |        t :~ {1 : 1 + t}
   |  |  |  |        Tick(1)
   |  |  |  |
   |  |  |  `- 0
   |  |  |
   |  |  `- 4[1 + m | 1 + m  0]
   |  |
   |  +- mixed-lin-template
   |  |  |
   |  |  `- 1 + [1 + m | 1 + m  0] + [1 + m | 1 + m  0][n | n  0] + 2([n | n  0]) + [n | n  0]^2
   |  |
   |  +- [Norms]
   |  |    [[1 | ],[1 + m | 1 + m  0],[mn + n | 1 + m  0   n  0],[n | n  0],[n^2 | n  0]]
   |  |
   |  +- [Invariant]
   |  |    n  1 ==> 4[1 + m | 1 + m  0] + h([1 | ],[1 + m | 1 + m  0],[-1 + -m + mn + n | -1 + n  0   1 + m  0],[-1 + n | -1 + n  0],[1 + -2(n) + n^2 | -1 + n  0])  h([1 | ],[1 + m | 1 + m  0],[mn + n | 1 + m  0   n  0],[n | n  0],[n^2 | n  0])
   |  |    1  1 + n ==> 0  h([1 | ],[1 + m | 1 + m  0],[mn + n | 1 + m  0   n  0],[n | n  0],[n^2 | n  0])
   |  |
   |  `- 4[mn + n | 1 + m  0   n  0]
   |
   `- 4[mn + n | 1 + m  0   n  0]

[Success] 4[mn + n | 1 + m
              0   n  0]
Degree: 2