ExecutionLog
|
`- Expected Cost
   |
   +- [f]
   |    0
   |
   +- [Program]
   |    0:While(n  1)
   |        i :~ {3/10 : 1;7/10 : 0}
   |        z :~ {1 : 1 + z}
   |        d :~ {2/5 : 1;3/5 : 0}
   |        Tick(1)
   |        1:If(1  1 + d   1  1 + i) Then
   |            g :~ {7/10 : 1;3/10 : 0}
   |            Tick(1)
   |          Else
   |            2:If(1  1 + i   d  1) Then
   |                g :~ {19/20 : 1;1/20 : 0}
   |                Tick(1)
   |              Else
   |                3:If(1  1 + d   i  1) Then
   |                    g :~ {1/10 : 1;9/10 : 0}
   |                    Tick(1)
   |                  Else
   |                    g :~ {1/2 : 1;1/2 : 0}
   |                    Tick(1)
   |        4:If(1  1 + i) Then
   |            s :~ {1/20 : 1;19/20 : 0}
   |            Tick(1)
   |          Else
   |            s :~ {4/5 : 1;1/5 : 0}
   |            Tick(1)
   |        5:If(1  1 + g) Then
   |            l :~ {1/10 : 1;9/10 : 0}
   |            Tick(1)
   |          Else
   |            l :~ {3/5 : 1;2/5 : 0}
   |            Tick(1)
   |        n :~ {1 : -1 + n}
   |
   +- While.step
   |  |
   |  +- [Problem]
   |  |    0:While(n  1)
   |  |        i :~ {3/10 : 1;7/10 : 0}
   |  |        z :~ {1 : 1 + z}
   |  |        d :~ {2/5 : 1;3/5 : 0}
   |  |        Tick(1)
   |  |        1:If(1  1 + d   1  1 + i) Then
   |  |            g :~ {7/10 : 1;3/10 : 0}
   |  |            Tick(1)
   |  |          Else
   |  |            2:If(1  1 + i   d  1) Then
   |  |                g :~ {19/20 : 1;1/20 : 0}
   |  |                Tick(1)
   |  |              Else
   |  |                3:If(1  1 + d   i  1) Then
   |  |                    g :~ {1/10 : 1;9/10 : 0}
   |  |                    Tick(1)
   |  |                  Else
   |  |                    g :~ {1/2 : 1;1/2 : 0}
   |  |                    Tick(1)
   |  |        4:If(1  1 + i) Then
   |  |            s :~ {1/20 : 1;19/20 : 0}
   |  |            Tick(1)
   |  |          Else
   |  |            s :~ {4/5 : 1;1/5 : 0}
   |  |            Tick(1)
   |  |        5:If(1  1 + g) Then
   |  |            l :~ {1/10 : 1;9/10 : 0}
   |  |            Tick(1)
   |  |          Else
   |  |            l :~ {3/5 : 1;2/5 : 0}
   |  |            Tick(1)
   |  |        n :~ {1 : -1 + n}
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- Expected Cost Body
   |  |  |
   |  |  `- 4
   |  |
   |  +- linear-template
   |  |  |
   |  |  `- 1 + [n | n  0]
   |  |
   |  +- [Norms]
   |  |    [[1 | ],[n | n  0]]
   |  |
   |  +- [Invariant]
   |  |    n  1 ==> 4 + h([1 | ],[-1 + n | -1 + n  0])  h([1 | ],[n | n  0])
   |  |    1  1 + n ==> 0  h([1 | ],[n | n  0])
   |  |
   |  `- 4[n | n  0]
   |
   `- 4[n | n  0]

[Success] 4[n | n  0]
Degree: 1