ExecutionLog
|
`- Expected Cost
   |
   +- [f]
   |    0
   |
   +- [Program]
   |    0:While(n  1 + d)
   |        1:If(x  1) Then
   |            2:If(y  1) Then
   |                Choice
   |                  1/4: x :~ {1 : 2 + x}
   |                       d :~ {1 : 2 + d}
   |                  3/4: Choice
   |                         1/3: y :~ {1 : 2 + y}
   |                              d :~ {1 : 2 + d}
   |                         2/3: Choice
   |                                1/2: x :~ {1 : -1 + x}
   |                                     d :~ {1 : -1 + d}
   |                                1/2: y :~ {1 : -1 + y}
   |                                     d :~ {1 : -1 + d}
   |              Else
   |                3:If(0  1 + y) Then
   |                    Choice
   |                      1/4: x :~ {1 : 2 + x}
   |                           d :~ {1 : 2 + d}
   |                      3/4: Choice
   |                             1/3: y :~ {1 : 1 + y}
   |                                  d :~ {1 : -1 + d}
   |                             2/3: Choice
   |                                    1/2: x :~ {1 : -1 + x}
   |                                         d :~ {1 : -1 + d}
   |                                    1/2: y :~ {1 : -2 + y}
   |                                         d :~ {1 : 2 + d}
   |                  Else
   |                    Choice
   |                      1/4: x :~ {1 : 2 + x}
   |                           d :~ {1 : 2 + d}
   |                      3/4: Choice
   |                             1/3: y :~ {1 : 1 + y}
   |                                  d :~ {1 : 1 + d}
   |                             2/3: Choice
   |                                    1/2: x :~ {1 : -1 + x}
   |                                         d :~ {1 : -1 + d}
   |                                    1/2: y :~ {1 : -1 + y}
   |                                         d :~ {1 : 1 + d}
   |          Else
   |            4:If(0  1 + x) Then
   |                5:If(y  1) Then
   |                    Choice
   |                      1/4: x :~ {1 : 1 + x}
   |                           d :~ {1 : -1 + d}
   |                      3/4: Choice
   |                             1/3: y :~ {1 : 2 + y}
   |                                  d :~ {1 : 2 + d}
   |                             2/3: Choice
   |                                    1/2: x :~ {1 : -2 + x}
   |                                         d :~ {1 : 2 + d}
   |                                    1/2: y :~ {1 : -1 + y}
   |                                         d :~ {1 : -1 + d}
   |                  Else
   |                    6:If(0  1 + y) Then
   |                        Choice
   |                          1/4: x :~ {1 : 1 + x}
   |                               d :~ {1 : -1 + d}
   |                          3/4: Choice
   |                                 1/3: y :~ {1 : 1 + y}
   |                                      d :~ {1 : -1 + d}
   |                                 2/3: Choice
   |                                        1/2: x :~ {1 : -2 + x}
   |                                             d :~ {1 : 2 + d}
   |                                        1/2: y :~ {1 : -2 + y}
   |                                             d :~ {1 : 2 + d}
   |                      Else
   |                        Choice
   |                          1/4: x :~ {1 : 1 + x}
   |                               d :~ {1 : -1 + d}
   |                          3/4: Choice
   |                                 1/3: y :~ {1 : 1 + y}
   |                                      d :~ {1 : 1 + d}
   |                                 2/3: Choice
   |                                        1/2: x :~ {1 : -2 + x}
   |                                             d :~ {1 : 2 + d}
   |                                        1/2: y :~ {1 : -1 + y}
   |                                             d :~ {1 : 1 + d}
   |              Else
   |                7:If(y  1) Then
   |                    Choice
   |                      1/4: x :~ {1 : 1 + x}
   |                           d :~ {1 : 1 + d}
   |                      3/4: Choice
   |                             1/3: y :~ {1 : 2 + y}
   |                                  d :~ {1 : 2 + d}
   |                             2/3: Choice
   |                                    1/2: x :~ {1 : -1 + x}
   |                                         d :~ {1 : 1 + d}
   |                                    1/2: y :~ {1 : -1 + y}
   |                                         d :~ {1 : -1 + d}
   |                  Else
   |                    8:If(0  1 + y) Then
   |                        Choice
   |                          1/4: x :~ {1 : 1 + x}
   |                               d :~ {1 : 1 + d}
   |                          3/4: Choice
   |                                 1/3: y :~ {1 : 1 + y}
   |                                      d :~ {1 : -1 + d}
   |                                 2/3: Choice
   |                                        1/2: x :~ {1 : -1 + x}
   |                                             d :~ {1 : 1 + d}
   |                                        1/2: y :~ {1 : -2 + y}
   |                                             d :~ {1 : 2 + d}
   |                      Else
   |                        Choice
   |                          1/4: x :~ {1 : 1 + x}
   |                               d :~ {1 : 1 + d}
   |                          3/4: Choice
   |                                 1/3: y :~ {1 : 1 + y}
   |                                      d :~ {1 : 1 + d}
   |                                 2/3: Choice
   |                                        1/2: x :~ {1 : -1 + x}
   |                                             d :~ {1 : 1 + d}
   |                                        1/2: y :~ {1 : -1 + y}
   |                                             d :~ {1 : 1 + d}
   |        Tick(1)
   |
   +- While.step
   |  |
   |  +- [Problem]
   |  |    0:While(n  1 + d)
   |  |        1:If(x  1) Then
   |  |            2:If(y  1) Then
   |  |                Choice
   |  |                  1/4: x :~ {1 : 2 + x}
   |  |                       d :~ {1 : 2 + d}
   |  |                  3/4: Choice
   |  |                         1/3: y :~ {1 : 2 + y}
   |  |                              d :~ {1 : 2 + d}
   |  |                         2/3: Choice
   |  |                                1/2: x :~ {1 : -1 + x}
   |  |                                     d :~ {1 : -1 + d}
   |  |                                1/2: y :~ {1 : -1 + y}
   |  |                                     d :~ {1 : -1 + d}
   |  |              Else
   |  |                3:If(0  1 + y) Then
   |  |                    Choice
   |  |                      1/4: x :~ {1 : 2 + x}
   |  |                           d :~ {1 : 2 + d}
   |  |                      3/4: Choice
   |  |                             1/3: y :~ {1 : 1 + y}
   |  |                                  d :~ {1 : -1 + d}
   |  |                             2/3: Choice
   |  |                                    1/2: x :~ {1 : -1 + x}
   |  |                                         d :~ {1 : -1 + d}
   |  |                                    1/2: y :~ {1 : -2 + y}
   |  |                                         d :~ {1 : 2 + d}
   |  |                  Else
   |  |                    Choice
   |  |                      1/4: x :~ {1 : 2 + x}
   |  |                           d :~ {1 : 2 + d}
   |  |                      3/4: Choice
   |  |                             1/3: y :~ {1 : 1 + y}
   |  |                                  d :~ {1 : 1 + d}
   |  |                             2/3: Choice
   |  |                                    1/2: x :~ {1 : -1 + x}
   |  |                                         d :~ {1 : -1 + d}
   |  |                                    1/2: y :~ {1 : -1 + y}
   |  |                                         d :~ {1 : 1 + d}
   |  |          Else
   |  |            4:If(0  1 + x) Then
   |  |                5:If(y  1) Then
   |  |                    Choice
   |  |                      1/4: x :~ {1 : 1 + x}
   |  |                           d :~ {1 : -1 + d}
   |  |                      3/4: Choice
   |  |                             1/3: y :~ {1 : 2 + y}
   |  |                                  d :~ {1 : 2 + d}
   |  |                             2/3: Choice
   |  |                                    1/2: x :~ {1 : -2 + x}
   |  |                                         d :~ {1 : 2 + d}
   |  |                                    1/2: y :~ {1 : -1 + y}
   |  |                                         d :~ {1 : -1 + d}
   |  |                  Else
   |  |                    6:If(0  1 + y) Then
   |  |                        Choice
   |  |                          1/4: x :~ {1 : 1 + x}
   |  |                               d :~ {1 : -1 + d}
   |  |                          3/4: Choice
   |  |                                 1/3: y :~ {1 : 1 + y}
   |  |                                      d :~ {1 : -1 + d}
   |  |                                 2/3: Choice
   |  |                                        1/2: x :~ {1 : -2 + x}
   |  |                                             d :~ {1 : 2 + d}
   |  |                                        1/2: y :~ {1 : -2 + y}
   |  |                                             d :~ {1 : 2 + d}
   |  |                      Else
   |  |                        Choice
   |  |                          1/4: x :~ {1 : 1 + x}
   |  |                               d :~ {1 : -1 + d}
   |  |                          3/4: Choice
   |  |                                 1/3: y :~ {1 : 1 + y}
   |  |                                      d :~ {1 : 1 + d}
   |  |                                 2/3: Choice
   |  |                                        1/2: x :~ {1 : -2 + x}
   |  |                                             d :~ {1 : 2 + d}
   |  |                                        1/2: y :~ {1 : -1 + y}
   |  |                                             d :~ {1 : 1 + d}
   |  |              Else
   |  |                7:If(y  1) Then
   |  |                    Choice
   |  |                      1/4: x :~ {1 : 1 + x}
   |  |                           d :~ {1 : 1 + d}
   |  |                      3/4: Choice
   |  |                             1/3: y :~ {1 : 2 + y}
   |  |                                  d :~ {1 : 2 + d}
   |  |                             2/3: Choice
   |  |                                    1/2: x :~ {1 : -1 + x}
   |  |                                         d :~ {1 : 1 + d}
   |  |                                    1/2: y :~ {1 : -1 + y}
   |  |                                         d :~ {1 : -1 + d}
   |  |                  Else
   |  |                    8:If(0  1 + y) Then
   |  |                        Choice
   |  |                          1/4: x :~ {1 : 1 + x}
   |  |                               d :~ {1 : 1 + d}
   |  |                          3/4: Choice
   |  |                                 1/3: y :~ {1 : 1 + y}
   |  |                                      d :~ {1 : -1 + d}
   |  |                                 2/3: Choice
   |  |                                        1/2: x :~ {1 : -1 + x}
   |  |                                             d :~ {1 : 1 + d}
   |  |                                        1/2: y :~ {1 : -2 + y}
   |  |                                             d :~ {1 : 2 + d}
   |  |                      Else
   |  |                        Choice
   |  |                          1/4: x :~ {1 : 1 + x}
   |  |                               d :~ {1 : 1 + d}
   |  |                          3/4: Choice
   |  |                                 1/3: y :~ {1 : 1 + y}
   |  |                                      d :~ {1 : 1 + d}
   |  |                                 2/3: Choice
   |  |                                        1/2: x :~ {1 : -1 + x}
   |  |                                             d :~ {1 : 1 + d}
   |  |                                        1/2: y :~ {1 : -1 + y}
   |  |                                             d :~ {1 : 1 + d}
   |  |        Tick(1)
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- Expected Cost Body
   |  |  |
   |  |  `- [1 | ]
   |  |
   |  +- shift-avg-template
   |  |  |
   |  |  `- 1 + [1 + -d + n | 1 + -d + n  0]
   |  |
   |  +- [Norms]
   |  |    [[1 | ],[1 + -d + n | 1 + -d + n  0]]
   |  |
   |  +- [Invariant]
   |  |    n  1 + d ==> [1 | ] + h([1 | ],ite(x  1,ite(y  1,1/4[-1 + -d + n | -1 + -d + n  0] + 1/4[-1 + -d + n | -1 + -d + n  0] + 1/2[2 + -d + n | 2 + -d + n  0],ite(0  1 + y,1/4[-1 + -d + n | -1 + -d + n  0] + 1/4[2 + -d + n | 2 + -d + n  0] + 1/4[2 + -d + n | 2 + -d + n  0] + 1/4[-1 + -d + n | -1 + -d + n  0],1/4[-1 + -d + n | -1 + -d + n  0] + 1/4[-d + n | -d + n  0] + 1/4[2 + -d + n | 2 + -d + n  0] + 1/4[-d + n | -d + n  0])),ite(0  1 + x,ite(y  1,1/4[2 + -d + n | 2 + -d + n  0] + 1/4[-1 + -d + n | -1 + -d + n  0] + 1/4[-1 + -d + n | -1 + -d + n  0] + 1/4[2 + -d + n | 2 + -d + n  0],ite(0  1 + y,1/4[2 + -d + n | 2 + -d + n  0] + 1/4[2 + -d + n | 2 + -d + n  0] + 1/2[-1 + -d + n | -1 + -d + n  0],1/4[2 + -d + n | 2 + -d + n  0] + 1/4[-d + n | -d + n  0] + 1/4[-1 + -d + n | -1 + -d + n  0] + 1/4[-d + n | -d + n  0])),ite(y  1,1/4[-d + n | -d + n  0] + 1/4[-1 + -d + n | -1 + -d + n  0] + 1/4[-d + n | -d + n  0] + 1/4[2 + -d + n | 2 + -d + n  0],ite(0  1 + y,1/4[-d + n | -d + n  0] + 1/4[2 + -d + n | 2 + -d + n  0] + 1/4[-d + n | -d + n  0] + 1/4[-1 + -d + n | -1 + -d + n  0],[-d + n | -d + n  0])))))  h([1 | ],[1 + -d + n | 1 + -d + n  0])
   |  |    1 + d  1 + n ==> 0  h([1 | ],[1 + -d + n | 1 + -d + n  0])
   |  |
   |  `- 2[1 + -d + n | 1 + -d + n  0]
   |
   `- 2[1 + -d + n | 1 + -d + n  0]

[Success] 2[1 + -d + n | 1 + -d
              + n  0]
Degree: 1