ExecutionLog
|
`- Expected Cost
   |
   +- [f]
   |    0
   |
   +- [Program]
   |    A :~ {1 : I}
   |    B :~ {1 : 0}
   |    Tick(1)
   |    0:While(C  1 + B)
   |        B :~ {1 : 1 + B}
   |        Tick(1)
   |    1:If(B  C) Then
   |        Skip
   |      Else
   |        Abort
   |    D :~ {1 : C}
   |    E :~ {1 : 0}
   |    Tick(1)
   |    2:While(D  2 + E)
   |        F :~ {1 : E}
   |        G :~ {1 : 1 + E}
   |        Tick(1)
   |        3:While(D  1 + G)
   |            NonDet
   |              {sample :~ {1/2 : 0;1/2 : 1}
   |              G :~ {1 : G + sample}
   |              Tick(1)}
   |              {Choice
   |                 1/2: F :~ {1 : G}
   |                      G :~ {1 : 1 + G}
   |                 1/2: F :~ {1 : F}
   |                      G :~ {1 : G}
   |              Tick(1)}
   |        4:If(G  D) Then
   |            Skip
   |          Else
   |            Abort
   |        E :~ {1 : 1 + E}
   |        H :~ {1 : I}
   |        Tick(1)
   |    5:If(1 + E  D) Then
   |        Skip
   |      Else
   |        Abort
   |    E :~ {1 : 0}
   |    Tick(1)
   |    6:While(D  2 + E)
   |        E :~ {1 : 1 + E}
   |        Tick(1)
   |    Tick(1)
   |
   +- Expected Cost
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- [Program]
   |  |    0:While(C  1 + B)
   |  |        B :~ {1 : 1 + B}
   |  |        Tick(1)
   |  |
   |  +- While.step
   |  |  |
   |  |  +- [Problem]
   |  |  |    0:While(C  1 + B)
   |  |  |        B :~ {1 : 1 + B}
   |  |  |        Tick(1)
   |  |  |
   |  |  +- [f]
   |  |  |    0
   |  |  |
   |  |  +- Expected Cost Body
   |  |  |  |
   |  |  |  `- [1 | ]
   |  |  |
   |  |  +- linear-template
   |  |  |  |
   |  |  |  `- 1 + [-B + C | -B + C  0]
   |  |  |
   |  |  +- [Norms]
   |  |  |    [[1 | ],[-B + C | -B + C  0]]
   |  |  |
   |  |  +- [Invariant]
   |  |  |    C  1 + B ==> [1 | ] + h([1 | ],[-1 + -B + C | -1 + -B + C  0])  h([1 | ],[-B + C | -B + C  0])
   |  |  |    1 + B  1 + C ==> 0  h([1 | ],[-B + C | -B + C  0])
   |  |  |
   |  |  `- [-B + C | -B + C  0]
   |  |
   |  `- [-B + C | -B + C  0]
   |
   +- Expected Cost
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- [Program]
   |  |    1:If(B  C) Then
   |  |        Skip
   |  |      Else
   |  |        Abort
   |  |    D :~ {1 : C}
   |  |    E :~ {1 : 0}
   |  |    Tick(1)
   |  |    2:While(D  2 + E)
   |  |        F :~ {1 : E}
   |  |        G :~ {1 : 1 + E}
   |  |        Tick(1)
   |  |        3:While(D  1 + G)
   |  |            NonDet
   |  |              {sample :~ {1/2 : 0;1/2 : 1}
   |  |              G :~ {1 : G + sample}
   |  |              Tick(1)}
   |  |              {Choice
   |  |                 1/2: F :~ {1 : G}
   |  |                      G :~ {1 : 1 + G}
   |  |                 1/2: F :~ {1 : F}
   |  |                      G :~ {1 : G}
   |  |              Tick(1)}
   |  |        4:If(G  D) Then
   |  |            Skip
   |  |          Else
   |  |            Abort
   |  |        E :~ {1 : 1 + E}
   |  |        H :~ {1 : I}
   |  |        Tick(1)
   |  |    5:If(1 + E  D) Then
   |  |        Skip
   |  |      Else
   |  |        Abort
   |  |    E :~ {1 : 0}
   |  |    Tick(1)
   |  |    6:While(D  2 + E)
   |  |        E :~ {1 : 1 + E}
   |  |        Tick(1)
   |  |    Tick(1)
   |  |
   |  +- Expected Cost
   |  |  |
   |  |  +- [f]
   |  |  |    0
   |  |  |
   |  |  +- [Program]
   |  |  |    2:While(D  2 + E)
   |  |  |        F :~ {1 : E}
   |  |  |        G :~ {1 : 1 + E}
   |  |  |        Tick(1)
   |  |  |        3:While(D  1 + G)
   |  |  |            NonDet
   |  |  |              {sample :~ {1/2 : 0;1/2 : 1}
   |  |  |              G :~ {1 : G + sample}
   |  |  |              Tick(1)}
   |  |  |              {Choice
   |  |  |                 1/2: F :~ {1 : G}
   |  |  |                      G :~ {1 : 1 + G}
   |  |  |                 1/2: F :~ {1 : F}
   |  |  |                      G :~ {1 : G}
   |  |  |              Tick(1)}
   |  |  |        4:If(G  D) Then
   |  |  |            Skip
   |  |  |          Else
   |  |  |            Abort
   |  |  |        E :~ {1 : 1 + E}
   |  |  |        H :~ {1 : I}
   |  |  |        Tick(1)
   |  |  |
   |  |  +- While.step
   |  |  |  |
   |  |  |  +- [Problem]
   |  |  |  |    2:While(D  2 + E)
   |  |  |  |        F :~ {1 : E}
   |  |  |  |        G :~ {1 : 1 + E}
   |  |  |  |        Tick(1)
   |  |  |  |        3:While(D  1 + G)
   |  |  |  |            NonDet
   |  |  |  |              {sample :~ {1/2 : 0;1/2 : 1}
   |  |  |  |              G :~ {1 : G + sample}
   |  |  |  |              Tick(1)}
   |  |  |  |              {Choice
   |  |  |  |                 1/2: F :~ {1 : G}
   |  |  |  |                      G :~ {1 : 1 + G}
   |  |  |  |                 1/2: F :~ {1 : F}
   |  |  |  |                      G :~ {1 : G}
   |  |  |  |              Tick(1)}
   |  |  |  |        4:If(G  D) Then
   |  |  |  |            Skip
   |  |  |  |          Else
   |  |  |  |            Abort
   |  |  |  |        E :~ {1 : 1 + E}
   |  |  |  |        H :~ {1 : I}
   |  |  |  |        Tick(1)
   |  |  |  |
   |  |  |  +- [f]
   |  |  |  |    0
   |  |  |  |
   |  |  |  +- Expected Cost Body
   |  |  |  |  |
   |  |  |  |  +- Expected Cost
   |  |  |  |  |  |
   |  |  |  |  |  +- [f]
   |  |  |  |  |  |    0
   |  |  |  |  |  |
   |  |  |  |  |  +- [Program]
   |  |  |  |  |  |    3:While(D  1 + G)
   |  |  |  |  |  |        NonDet
   |  |  |  |  |  |          {sample :~ {1/2 : 0;1/2 : 1}
   |  |  |  |  |  |          G :~ {1 : G + sample}
   |  |  |  |  |  |          Tick(1)}
   |  |  |  |  |  |          {Choice
   |  |  |  |  |  |             1/2: F :~ {1 : G}
   |  |  |  |  |  |                  G :~ {1 : 1 + G}
   |  |  |  |  |  |             1/2: F :~ {1 : F}
   |  |  |  |  |  |                  G :~ {1 : G}
   |  |  |  |  |  |          Tick(1)}
   |  |  |  |  |  |
   |  |  |  |  |  +- While.step
   |  |  |  |  |  |  |
   |  |  |  |  |  |  +- [Problem]
   |  |  |  |  |  |  |    3:While(D  1 + G)
   |  |  |  |  |  |  |        NonDet
   |  |  |  |  |  |  |          {sample :~ {1/2 : 0;1/2 : 1}
   |  |  |  |  |  |  |          G :~ {1 : G + sample}
   |  |  |  |  |  |  |          Tick(1)}
   |  |  |  |  |  |  |          {Choice
   |  |  |  |  |  |  |             1/2: F :~ {1 : G}
   |  |  |  |  |  |  |                  G :~ {1 : 1 + G}
   |  |  |  |  |  |  |             1/2: F :~ {1 : F}
   |  |  |  |  |  |  |                  G :~ {1 : G}
   |  |  |  |  |  |  |          Tick(1)}
   |  |  |  |  |  |  |
   |  |  |  |  |  |  +- [f]
   |  |  |  |  |  |  |    0
   |  |  |  |  |  |  |
   |  |  |  |  |  |  +- Expected Cost Body
   |  |  |  |  |  |  |  |
   |  |  |  |  |  |  |  `- [1 | ]
   |  |  |  |  |  |  |
   |  |  |  |  |  |  +- linear-template
   |  |  |  |  |  |  |  |
   |  |  |  |  |  |  |  `- 1 + [D + -G | D + -G  0]
   |  |  |  |  |  |  |
   |  |  |  |  |  |  +- [Norms]
   |  |  |  |  |  |  |    [[1 | ],[D + -G | D + -G  0]]
   |  |  |  |  |  |  |
   |  |  |  |  |  |  +- [Invariant]
   |  |  |  |  |  |  |    D  1 + G ==> [1 | ] + h([1 | ],sup(1/2[D + -G | D + -G  0] + 1/2[-1 + D + -G | -1 + D + -G  0],1/2[-1 + D + -G | -1 + D + -G  0] + 1/2[D + -G | D + -G  0]))  h([1 | ],[D + -G | D + -G  0])
   |  |  |  |  |  |  |    1 + G  1 + D ==> 0  h([1 | ],[D + -G | D + -G  0])
   |  |  |  |  |  |  |
   |  |  |  |  |  |  `- 2[D + -G | D + -G  0]
   |  |  |  |  |  |
   |  |  |  |  |  `- 2[D + -G | D + -G  0]
   |  |  |  |  |
   |  |  |  |  +- Expected Cost
   |  |  |  |  |  |
   |  |  |  |  |  +- [f]
   |  |  |  |  |  |    0
   |  |  |  |  |  |
   |  |  |  |  |  +- [Program]
   |  |  |  |  |  |    4:If(G  D) Then
   |  |  |  |  |  |        Skip
   |  |  |  |  |  |      Else
   |  |  |  |  |  |        Abort
   |  |  |  |  |  |    E :~ {1 : 1 + E}
   |  |  |  |  |  |    H :~ {1 : I}
   |  |  |  |  |  |    Tick(1)
   |  |  |  |  |  |
   |  |  |  |  |  `- [G  D]  [1 | ]
   |  |  |  |  |
   |  |  |  |  +- Expected Cost
   |  |  |  |  |  |
   |  |  |  |  |  +- [f]
   |  |  |  |  |  |    [G  D]  [1 | ]
   |  |  |  |  |  |
   |  |  |  |  |  +- [Program]
   |  |  |  |  |  |    3:While(D  1 + G)
   |  |  |  |  |  |        NonDet
   |  |  |  |  |  |          {sample :~ {1/2 : 0;1/2 : 1}
   |  |  |  |  |  |          G :~ {1 : G + sample}
   |  |  |  |  |  |          Tick(1)}
   |  |  |  |  |  |          {Choice
   |  |  |  |  |  |             1/2: F :~ {1 : G}
   |  |  |  |  |  |                  G :~ {1 : 1 + G}
   |  |  |  |  |  |             1/2: F :~ {1 : F}
   |  |  |  |  |  |                  G :~ {1 : G}
   |  |  |  |  |  |          Tick(1)}
   |  |  |  |  |  |
   |  |  |  |  |  +- While.step
   |  |  |  |  |  |  |
   |  |  |  |  |  |  +- [Problem]
   |  |  |  |  |  |  |    3:While(D  1 + G)
   |  |  |  |  |  |  |        NonDet
   |  |  |  |  |  |  |          {sample :~ {1/2 : 0;1/2 : 1}
   |  |  |  |  |  |  |          G :~ {1 : G + sample}
   |  |  |  |  |  |  |          Tick(1)}
   |  |  |  |  |  |  |          {Choice
   |  |  |  |  |  |  |             1/2: F :~ {1 : G}
   |  |  |  |  |  |  |                  G :~ {1 : 1 + G}
   |  |  |  |  |  |  |             1/2: F :~ {1 : F}
   |  |  |  |  |  |  |                  G :~ {1 : G}
   |  |  |  |  |  |  |          Tick(1)}
   |  |  |  |  |  |  |
   |  |  |  |  |  |  +- [f]
   |  |  |  |  |  |  |    [G  D]  [1 | ]
   |  |  |  |  |  |  |
   |  |  |  |  |  |  +- linear-template
   |  |  |  |  |  |  |  |
   |  |  |  |  |  |  |  `- 2 + [1 + -D + G | 1 + -D + G  0] + 2([D + -G | D + -G  0])
   |  |  |  |  |  |  |
   |  |  |  |  |  |  +- [Norms]
   |  |  |  |  |  |  |    [[1 | ],[1 + -D + G | 1 + -D + G  0],[D + -G | D + -G  0]]
   |  |  |  |  |  |  |
   |  |  |  |  |  |  +- [Invariant]
   |  |  |  |  |  |  |    D  1 + G ==> 0 + h([1 | ],sup(1/2[1 + -D + G | 1 + -D + G  0] + 1/2[2 + -D + G | 2 + -D + G  0],1/2[2 + -D + G | 2 + -D + G  0] + 1/2[1 + -D + G | 1 + -D + G  0]),sup(1/2[D + -G | D + -G  0] + 1/2[-1 + D + -G | -1 + D + -G  0],1/2[-1 + D + -G | -1 + D + -G  0] + 1/2[D + -G | D + -G  0]))  h([1 | ],[1 + -D + G | 1 + -D + G  0],[D + -G | D + -G  0])
   |  |  |  |  |  |  |    1 + G  1 + D ==> [G  D]  [1 | ]  h([1 | ],[1 + -D + G | 1 + -D + G  0],[D + -G | D + -G  0])
   |  |  |  |  |  |  |
   |  |  |  |  |  |  `- [1 | ]
   |  |  |  |  |  |
   |  |  |  |  |  `- [1 | ]
   |  |  |  |  |
   |  |  |  |  `- [1 | ] + 2[-1 + D + -E | -1 + D + -E  0] + [1 | ]
   |  |  |  |
   |  |  |  +- mixed-iteration-template
   |  |  |  |  |
   |  |  |  |  `- [-1 + D + -E | -1 + D + -E  0] + [-1 + D + -E | -1 + D + -E  0]^2
   |  |  |  |
   |  |  |  +- [Norms]
   |  |  |  |    [[-1 + D + -E | -1 + D + -E  0],[1 + -2(D) + -2(DE) + D^2 + 2(E) + E^2 | -1 + D + -E  0]]
   |  |  |  |
   |  |  |  +- While.step
   |  |  |  |  |
   |  |  |  |  +- [Problem]
   |  |  |  |  |    3:While(D  1 + G)
   |  |  |  |  |        NonDet
   |  |  |  |  |          {sample :~ {1/2 : 0;1/2 : 1}
   |  |  |  |  |          G :~ {1 : G + sample}
   |  |  |  |  |          Tick(1)}
   |  |  |  |  |          {Choice
   |  |  |  |  |             1/2: F :~ {1 : G}
   |  |  |  |  |                  G :~ {1 : 1 + G}
   |  |  |  |  |             1/2: F :~ {1 : F}
   |  |  |  |  |                  G :~ {1 : G}
   |  |  |  |  |          Tick(1)}
   |  |  |  |  |
   |  |  |  |  +- [f]
   |  |  |  |  |    [G  D]  [4 + -4(D) + -2(DE) + D^2 + 4(E) + E^2 | -2 + D + -E  0]
   |  |  |  |  |
   |  |  |  |  +- linear-template
   |  |  |  |  |  |
   |  |  |  |  |  `- 1 + [4 + -4(D) + -2(DE) + D^2 + 4(E) + E^2 | -2 + D + -E  0] + [1 + -D + G | 1 + -D + G  0] + 2([D + -G | D + -G  0])
   |  |  |  |  |
   |  |  |  |  +- [Norms]
   |  |  |  |  |    [[1 | ],[4 + -4(D) + -2(DE) + D^2 + 4(E) + E^2 | -2 + D + -E  0],[1 + -D + G | 1 + -D + G  0],[D + -G | D + -G  0]]
   |  |  |  |  |
   |  |  |  |  +- [Invariant]
   |  |  |  |  |    D  1 + G ==> 0 + h([1 | ],[4 + -4(D) + -2(DE) + D^2 + 4(E) + E^2 | -2 + D + -E  0],sup(1/2[1 + -D + G | 1 + -D + G  0] + 1/2[2 + -D + G | 2 + -D + G  0],1/2[2 + -D + G | 2 + -D + G  0] + 1/2[1 + -D + G | 1 + -D + G  0]),sup(1/2[D + -G | D + -G  0] + 1/2[-1 + D + -G | -1 + D + -G  0],1/2[-1 + D + -G | -1 + D + -G  0] + 1/2[D + -G | D + -G  0]))  h([1 | ],[4 + -4(D) + -2(DE) + D^2 + 4(E) + E^2 | -2 + D + -E  0],[1 + -D + G | 1 + -D + G  0],[D + -G | D + -G  0])
   |  |  |  |  |    1 + G  1 + D ==> [G  D]  [4 + -4(D) + -2(DE) + D^2 + 4(E) + E^2 | -2 + D + -E  0]  h([1 | ],[4 + -4(D) + -2(DE) + D^2 + 4(E) + E^2 | -2 + D + -E  0],[1 + -D + G | 1 + -D + G  0],[D + -G | D + -G  0])
   |  |  |  |  |
   |  |  |  |  `- [4 + -4(D) + -2(DE) + D^2 + 4(E) + E^2 | -2 + D + -E  0]
   |  |  |  |
   |  |  |  +- [Invariant]
   |  |  |  |    D  2 + E ==> [1 | ] + 2[-1 + D + -E | -1 + D + -E  0] + [1 | ] + h([-2 + D + -E | -2 + D + -E  0],[4 + -4(D) + -2(DE) + D^2 + 4(E) + E^2 | -2 + D + -E  0])  h([-1 + D + -E | -1 + D + -E  0],[1 + -2(D) + -2(DE) + D^2 + 2(E) + E^2 | -1 + D + -E  0])
   |  |  |  |    2 + E  1 + D ==> 0  h([-1 + D + -E | -1 + D + -E  0],[1 + -2(D) + -2(DE) + D^2 + 2(E) + E^2 | -1 + D + -E  0])
   |  |  |  |
   |  |  |  `- 3[-1 + D + -E | -1 + D + -E  0] + [1 + -2(D) + -2(DE) + D^2 + 2(E) + E^2 | -1 + D + -E  0]
   |  |  |
   |  |  `- 3[-1 + D + -E | -1 + D + -E  0] + [1 + -2(D) + -2(DE) + D^2 + 2(E) + E^2 | -1 + D + -E  0]
   |  |
   |  +- Expected Cost
   |  |  |
   |  |  +- [f]
   |  |  |    0
   |  |  |
   |  |  +- [Program]
   |  |  |    5:If(1 + E  D) Then
   |  |  |        Skip
   |  |  |      Else
   |  |  |        Abort
   |  |  |    E :~ {1 : 0}
   |  |  |    Tick(1)
   |  |  |    6:While(D  2 + E)
   |  |  |        E :~ {1 : 1 + E}
   |  |  |        Tick(1)
   |  |  |    Tick(1)
   |  |  |
   |  |  +- Expected Cost
   |  |  |  |
   |  |  |  +- [f]
   |  |  |  |    0
   |  |  |  |
   |  |  |  +- [Program]
   |  |  |  |    6:While(D  2 + E)
   |  |  |  |        E :~ {1 : 1 + E}
   |  |  |  |        Tick(1)
   |  |  |  |
   |  |  |  +- While.step
   |  |  |  |  |
   |  |  |  |  +- [Problem]
   |  |  |  |  |    6:While(D  2 + E)
   |  |  |  |  |        E :~ {1 : 1 + E}
   |  |  |  |  |        Tick(1)
   |  |  |  |  |
   |  |  |  |  +- [f]
   |  |  |  |  |    0
   |  |  |  |  |
   |  |  |  |  +- Expected Cost Body
   |  |  |  |  |  |
   |  |  |  |  |  `- [1 | ]
   |  |  |  |  |
   |  |  |  |  +- linear-template
   |  |  |  |  |  |
   |  |  |  |  |  `- 1 + [-1 + D + -E | -1 + D + -E  0]
   |  |  |  |  |
   |  |  |  |  +- [Norms]
   |  |  |  |  |    [[1 | ],[-1 + D + -E | -1 + D + -E  0]]
   |  |  |  |  |
   |  |  |  |  +- [Invariant]
   |  |  |  |  |    D  2 + E ==> [1 | ] + h([1 | ],[-2 + D + -E | -2 + D + -E  0])  h([1 | ],[-1 + D + -E | -1 + D + -E  0])
   |  |  |  |  |    2 + E  1 + D ==> 0  h([1 | ],[-1 + D + -E | -1 + D + -E  0])
   |  |  |  |  |
   |  |  |  |  `- [-1 + D + -E | -1 + D + -E  0]
   |  |  |  |
   |  |  |  `- [-1 + D + -E | -1 + D + -E  0]
   |  |  |
   |  |  +- Expected Cost
   |  |  |  |
   |  |  |  +- [f]
   |  |  |  |    0
   |  |  |  |
   |  |  |  +- [Program]
   |  |  |  |    Tick(1)
   |  |  |  |
   |  |  |  `- [1 | ]
   |  |  |
   |  |  +- Expected Cost
   |  |  |  |
   |  |  |  +- [f]
   |  |  |  |    [1 | ]
   |  |  |  |
   |  |  |  +- [Program]
   |  |  |  |    6:While(D  2 + E)
   |  |  |  |        E :~ {1 : 1 + E}
   |  |  |  |        Tick(1)
   |  |  |  |
   |  |  |  `- [1 | ]
   |  |  |
   |  |  `- [1 + E  D]  ([1 | ] + [-1 + D | -1 + D  0] + [1 | ])
   |  |
   |  +- Expected Cost
   |  |  |
   |  |  +- [f]
   |  |  |    [1 + E  D]  ([1 | ] + [-1 + D | -1 + D  0] + [1 | ])
   |  |  |
   |  |  +- [Program]
   |  |  |    2:While(D  2 + E)
   |  |  |        F :~ {1 : E}
   |  |  |        G :~ {1 : 1 + E}
   |  |  |        Tick(1)
   |  |  |        3:While(D  1 + G)
   |  |  |            NonDet
   |  |  |              {sample :~ {1/2 : 0;1/2 : 1}
   |  |  |              G :~ {1 : G + sample}
   |  |  |              Tick(1)}
   |  |  |              {Choice
   |  |  |                 1/2: F :~ {1 : G}
   |  |  |                      G :~ {1 : 1 + G}
   |  |  |                 1/2: F :~ {1 : F}
   |  |  |                      G :~ {1 : G}
   |  |  |              Tick(1)}
   |  |  |        4:If(G  D) Then
   |  |  |            Skip
   |  |  |          Else
   |  |  |            Abort
   |  |  |        E :~ {1 : 1 + E}
   |  |  |        H :~ {1 : I}
   |  |  |        Tick(1)
   |  |  |
   |  |  +- While.step
   |  |  |  |
   |  |  |  +- [Problem]
   |  |  |  |    2:While(D  2 + E)
   |  |  |  |        F :~ {1 : E}
   |  |  |  |        G :~ {1 : 1 + E}
   |  |  |  |        Tick(1)
   |  |  |  |        3:While(D  1 + G)
   |  |  |  |            NonDet
   |  |  |  |              {sample :~ {1/2 : 0;1/2 : 1}
   |  |  |  |              G :~ {1 : G + sample}
   |  |  |  |              Tick(1)}
   |  |  |  |              {Choice
   |  |  |  |                 1/2: F :~ {1 : G}
   |  |  |  |                      G :~ {1 : 1 + G}
   |  |  |  |                 1/2: F :~ {1 : F}
   |  |  |  |                      G :~ {1 : G}
   |  |  |  |              Tick(1)}
   |  |  |  |        4:If(G  D) Then
   |  |  |  |            Skip
   |  |  |  |          Else
   |  |  |  |            Abort
   |  |  |  |        E :~ {1 : 1 + E}
   |  |  |  |        H :~ {1 : I}
   |  |  |  |        Tick(1)
   |  |  |  |
   |  |  |  +- [f]
   |  |  |  |    [1 + E  D]  ([1 | ] + [-1 + D | -1 + D  0] + [1 | ])
   |  |  |  |
   |  |  |  +- linear-template
   |  |  |  |  |
   |  |  |  |  `- 3 + [-1 + D | -1 + D  0] + 4([-1 + D + -E | -1 + D + -E  0]) + 3([2 + -D + E | 2 + -D + E  0])
   |  |  |  |
   |  |  |  +- [Norms]
   |  |  |  |    [[1 | ],[-1 + D | -1 + D  0],[-1 + D + -E | -1 + D + -E  0],[2 + -D + E | 2 + -D + E  0]]
   |  |  |  |
   |  |  |  +- While.step
   |  |  |  |  |
   |  |  |  |  +- [Problem]
   |  |  |  |  |    3:While(D  1 + G)
   |  |  |  |  |        NonDet
   |  |  |  |  |          {sample :~ {1/2 : 0;1/2 : 1}
   |  |  |  |  |          G :~ {1 : G + sample}
   |  |  |  |  |          Tick(1)}
   |  |  |  |  |          {Choice
   |  |  |  |  |             1/2: F :~ {1 : G}
   |  |  |  |  |                  G :~ {1 : 1 + G}
   |  |  |  |  |             1/2: F :~ {1 : F}
   |  |  |  |  |                  G :~ {1 : G}
   |  |  |  |  |          Tick(1)}
   |  |  |  |  |
   |  |  |  |  +- [f]
   |  |  |  |  |    [G  D]  [3 + -D + E | 3 + -D + E  0]
   |  |  |  |  |
   |  |  |  |  +- linear-template
   |  |  |  |  |  |
   |  |  |  |  |  `- 1 + [1 + -D + G | 1 + -D + G  0] + [3 + -D + E | 3 + -D + E  0] + 2([D + -G | D + -G  0])
   |  |  |  |  |
   |  |  |  |  +- [Norms]
   |  |  |  |  |    [[1 | ],[1 + -D + G | 1 + -D + G  0],[3 + -D + E | 3 + -D + E  0],[D + -G | D + -G  0]]
   |  |  |  |  |
   |  |  |  |  +- [Invariant]
   |  |  |  |  |    D  1 + G ==> 0 + h([1 | ],sup(1/2[1 + -D + G | 1 + -D + G  0] + 1/2[2 + -D + G | 2 + -D + G  0],1/2[2 + -D + G | 2 + -D + G  0] + 1/2[1 + -D + G | 1 + -D + G  0]),[3 + -D + E | 3 + -D + E  0],sup(1/2[D + -G | D + -G  0] + 1/2[-1 + D + -G | -1 + D + -G  0],1/2[-1 + D + -G | -1 + D + -G  0] + 1/2[D + -G | D + -G  0]))  h([1 | ],[1 + -D + G | 1 + -D + G  0],[3 + -D + E | 3 + -D + E  0],[D + -G | D + -G  0])
   |  |  |  |  |    1 + G  1 + D ==> [G  D]  [3 + -D + E | 3 + -D + E  0]  h([1 | ],[1 + -D + G | 1 + -D + G  0],[3 + -D + E | 3 + -D + E  0],[D + -G | D + -G  0])
   |  |  |  |  |
   |  |  |  |  `- [3 + -D + E | 3 + -D + E  0]
   |  |  |  |
   |  |  |  +- [Invariant]
   |  |  |  |    D  2 + E ==> 0 + h([1 | ],[-1 + D | -1 + D  0],[-2 + D + -E | -2 + D + -E  0],[3 + -D + E | 3 + -D + E  0])  h([1 | ],[-1 + D | -1 + D  0],[-1 + D + -E | -1 + D + -E  0],[2 + -D + E | 2 + -D + E  0])
   |  |  |  |    2 + E  1 + D ==> [1 + E  D]  ([1 | ] + [-1 + D | -1 + D  0] + [1 | ])  h([1 | ],[-1 + D | -1 + D  0],[-1 + D + -E | -1 + D + -E  0],[2 + -D + E | 2 + -D + E  0])
   |  |  |  |
   |  |  |  `- 2 + [-1 + D | -1 + D  0]
   |  |  |
   |  |  `- 2 + [-1 + D | -1 + D  0]
   |  |
   |  `- [B  C]  ([1 | ] + 3[-1 + C | -1 + C  0] + [1 + -2(C) + C^2 | -1 + C  0] + 2 + [-1 + C | -1 + C  0])
   |
   +- Expected Cost
   |  |
   |  +- [f]
   |  |    [B  C]  ([1 | ] + 3[-1 + C | -1 + C  0] + [1 + -2(C) + C^2 | -1 + C  0] + 2 + [-1 + C | -1 + C  0])
   |  |
   |  +- [Program]
   |  |    0:While(C  1 + B)
   |  |        B :~ {1 : 1 + B}
   |  |        Tick(1)
   |  |
   |  +- While.step
   |  |  |
   |  |  +- [Problem]
   |  |  |    0:While(C  1 + B)
   |  |  |        B :~ {1 : 1 + B}
   |  |  |        Tick(1)
   |  |  |
   |  |  +- [f]
   |  |  |    [B  C]  ([1 | ] + 3[-1 + C | -1 + C  0] + [1 + -2(C) + C^2 | -1 + C  0] + 2 + [-1 + C | -1 + C  0])
   |  |  |
   |  |  +- linear-template
   |  |  |  |
   |  |  |  `- 3 + 2([-1 + C | -1 + C  0]) + [1 + -2(C) + C^2 | -1 + C  0] + 5([1 + B + -C | 1 + B + -C  0]) + 6([-B + C | -B + C  0])
   |  |  |
   |  |  +- [Norms]
   |  |  |    [[1 | ],[-1 + C | -1 + C  0],[1 + -2(C) + C^2 | -1 + C  0],[1 + B + -C | 1 + B + -C  0],[-B + C | -B + C  0]]
   |  |  |
   |  |  +- [Invariant]
   |  |  |    C  1 + B ==> 0 + h([1 | ],[-1 + C | -1 + C  0],[1 + -2(C) + C^2 | -1 + C  0],[2 + B + -C | 2 + B + -C  0],[-1 + -B + C | -1 + -B + C  0])  h([1 | ],[-1 + C | -1 + C  0],[1 + -2(C) + C^2 | -1 + C  0],[1 + B + -C | 1 + B + -C  0],[-B + C | -B + C  0])
   |  |  |    1 + B  1 + C ==> [B  C]  ([1 | ] + 3[-1 + C | -1 + C  0] + [1 + -2(C) + C^2 | -1 + C  0] + 2 + [-1 + C | -1 + C  0])  h([1 | ],[-1 + C | -1 + C  0],[1 + -2(C) + C^2 | -1 + C  0],[1 + B + -C | 1 + B + -C  0],[-B + C | -B + C  0])
   |  |  |
   |  |  `- 3 + 4[-1 + C | -1 + C  0] + [1 + -2(C) + C^2 | -1 + C  0]
   |  |
   |  `- 3 + 4[-1 + C | -1 + C  0] + [1 + -2(C) + C^2 | -1 + C  0]
   |
   `- [1 | ] + [C | C  0] + 3 + 4[-1 + C | -1 + C  0] + [1 + -2(C) + C^2 | -1 + C  0]

[Success] [1 | ] + [C | C  0]
                     + 3 + 4[-1 + C | -1 + C  0]
                        + [1 + -2(C) + C^2 | -1 + C
                            0]
Degree: 2