ExecutionLog
|
`- Expected Cost
   |
   +- [f]
   |    0
   |
   +- [Program]
   |    x :~ {1 : 0}
   |    y :~ {1 : 0}
   |    eX :~ {1 : 0}
   |    eY :~ {1 : 0}
   |    dx :~ {1 : 0}
   |    dy :~ {1 : 0}
   |    dxc :~ {1 : 0}
   |    dyc :~ {1 : 0}
   |    0:While(N  1)
   |        dx :~ {1 : 0}
   |        dy :~ {1 : 0}
   |        Choice
   |          1/10: cmd :~ {1 : 0}
   |          9/10: Choice
   |                  1/9: cmd :~ {1 : 1}
   |                  8/9: Choice
   |                         1/8: cmd :~ {1 : 2}
   |                         7/8: Choice
   |                                1/7: cmd :~ {1 : 3}
   |                                6/7: Choice
   |                                       1/6: cmd :~ {1 : 4}
   |                                       5/6: Choice
   |                                              1/5: cmd :~ {1 : 5}
   |                                              4/5: Choice
   |                                                     1/4: cmd :~ {1 : 6}
   |                                                     3/4: Choice
   |                                                            1/3: cmd :~ {1 : 7}
   |                                                            2/3: cmd :~ {1 : 8}
   |        1:If(0  cmd   cmd  0) Then
   |            N :~ {1 : -1 + N}
   |          Else
   |            2:If(1  cmd   cmd  1) Then
   |                N :~ {1 : -2 + N}
   |              Else
   |                3:If(2  cmd   cmd  2) Then
   |                    N :~ {1 : -3 + N}
   |                  Else
   |                    4:If(3  cmd   cmd  3) Then
   |                        N :~ {1 : -4 + N}
   |                      Else
   |                        5:If(4  cmd   cmd  4) Then
   |                            N :~ {1 : -5 + N}
   |                          Else
   |                            6:If(5  cmd   cmd  5) Then
   |                                N :~ {1 : -6 + N}
   |                              Else
   |                                7:If(6  cmd   cmd  6) Then
   |                                    N :~ {1 : -7 + N}
   |                                  Else
   |                                    8:If(7  cmd   cmd  7) Then
   |                                        N :~ {1 : -8 + N}
   |                                      Else
   |                                        N :~ {1 : N}
   |        Tick(1)
   |
   +- While.step
   |  |
   |  +- [Problem]
   |  |    0:While(N  1)
   |  |        dx :~ {1 : 0}
   |  |        dy :~ {1 : 0}
   |  |        Choice
   |  |          1/10: cmd :~ {1 : 0}
   |  |          9/10: Choice
   |  |                  1/9: cmd :~ {1 : 1}
   |  |                  8/9: Choice
   |  |                         1/8: cmd :~ {1 : 2}
   |  |                         7/8: Choice
   |  |                                1/7: cmd :~ {1 : 3}
   |  |                                6/7: Choice
   |  |                                       1/6: cmd :~ {1 : 4}
   |  |                                       5/6: Choice
   |  |                                              1/5: cmd :~ {1 : 5}
   |  |                                              4/5: Choice
   |  |                                                     1/4: cmd :~ {1 : 6}
   |  |                                                     3/4: Choice
   |  |                                                            1/3: cmd :~ {1 : 7}
   |  |                                                            2/3: cmd :~ {1 : 8}
   |  |        1:If(0  cmd   cmd  0) Then
   |  |            N :~ {1 : -1 + N}
   |  |          Else
   |  |            2:If(1  cmd   cmd  1) Then
   |  |                N :~ {1 : -2 + N}
   |  |              Else
   |  |                3:If(2  cmd   cmd  2) Then
   |  |                    N :~ {1 : -3 + N}
   |  |                  Else
   |  |                    4:If(3  cmd   cmd  3) Then
   |  |                        N :~ {1 : -4 + N}
   |  |                      Else
   |  |                        5:If(4  cmd   cmd  4) Then
   |  |                            N :~ {1 : -5 + N}
   |  |                          Else
   |  |                            6:If(5  cmd   cmd  5) Then
   |  |                                N :~ {1 : -6 + N}
   |  |                              Else
   |  |                                7:If(6  cmd   cmd  6) Then
   |  |                                    N :~ {1 : -7 + N}
   |  |                                  Else
   |  |                                    8:If(7  cmd   cmd  7) Then
   |  |                                        N :~ {1 : -8 + N}
   |  |                                      Else
   |  |                                        N :~ {1 : N}
   |  |        Tick(1)
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- Expected Cost Body
   |  |  |
   |  |  `- [1 | ]
   |  |
   |  +- linear-template
   |  |  |
   |  |  `- 1 + [N | N  0]
   |  |
   |  +- [Norms]
   |  |    [[1 | ],[N | N  0]]
   |  |
   |  +- [Invariant]
   |  |    N  1 ==> [1 | ] + h([1 | ],1/10[-1 + N | -1 + N  0] + 1/10[-2 + N | -2 + N  0] + 1/10[-3 + N | -3 + N  0] + 1/10[-4 + N | -4 + N  0] + 1/10[-5 + N | -5 + N  0] + 1/10[-6 + N | -6 + N  0] + 1/10[-7 + N | -7 + N  0] + 1/10[-8 + N | -8 + N  0] + 1/5[N | N  0])  h([1 | ],[N | N  0])
   |  |    1  1 + N ==> 0  h([1 | ],[N | N  0])
   |  |
   |  `- 5/4[N | N  0]
   |
   `- 5/4[N | N  0]

[Success] 5/4[N | N  0]
Degree: 1