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]