ExecutionLog
|
`- Expected Cost
   |
   +- [f]
   |    0
   |
   +- [Program]
   |    money :~ {1 : 10}
   |    0:While(money  n)
   |        Choice
   |          36/37: Choice
   |                   1/3: Choice
   |                          1/2: sample :~ {1/4 : 3;1/4 : 4;1/4 : 5;1/4 : 6}
   |                               money :~ {1 : money + sample}
   |                          1/2: sample :~ {1/2 : 1;1/2 : 2}
   |                               money :~ {1 : money + sample}
   |                   2/3: Choice
   |                          1/2: Choice
   |                                 1/3: sample :~ {1/4 : 3;1/4 : 4;1/4 : 5;1/4 : 6}
   |                                      money :~ {1 : money + sample}
   |                                 2/3: sample :~ {1/2 : 1;1/2 : 2}
   |                                      money :~ {1 : money + sample}
   |                          1/2: Choice
   |                                 2/3: sample :~ {1/4 : 3;1/4 : 4;1/4 : 5;1/4 : 6}
   |                                      money :~ {1 : money + -sample}
   |                                 1/3: sample :~ {1/6 : 5;1/6 : 6;1/6 : 7;1/6 : 8;1/6 : 9;1/6 : 10}
   |                                      money :~ {1 : money + -sample}
   |          1/37: sample :~ {1/6 : 5;1/6 : 6;1/6 : 7;1/6 : 8;1/6 : 9;1/6 : 10}
   |                money :~ {1 : money + -sample}
   |        Tick(1)
   |
   +- While.step
   |  |
   |  +- [Problem]
   |  |    0:While(money  n)
   |  |        Choice
   |  |          36/37: Choice
   |  |                   1/3: Choice
   |  |                          1/2: sample :~ {1/4 : 3;1/4 : 4;1/4 : 5;1/4 : 6}
   |  |                               money :~ {1 : money + sample}
   |  |                          1/2: sample :~ {1/2 : 1;1/2 : 2}
   |  |                               money :~ {1 : money + sample}
   |  |                   2/3: Choice
   |  |                          1/2: Choice
   |  |                                 1/3: sample :~ {1/4 : 3;1/4 : 4;1/4 : 5;1/4 : 6}
   |  |                                      money :~ {1 : money + sample}
   |  |                                 2/3: sample :~ {1/2 : 1;1/2 : 2}
   |  |                                      money :~ {1 : money + sample}
   |  |                          1/2: Choice
   |  |                                 2/3: sample :~ {1/4 : 3;1/4 : 4;1/4 : 5;1/4 : 6}
   |  |                                      money :~ {1 : money + -sample}
   |  |                                 1/3: sample :~ {1/6 : 5;1/6 : 6;1/6 : 7;1/6 : 8;1/6 : 9;1/6 : 10}
   |  |                                      money :~ {1 : money + -sample}
   |  |          1/37: sample :~ {1/6 : 5;1/6 : 6;1/6 : 7;1/6 : 8;1/6 : 9;1/6 : 10}
   |  |                money :~ {1 : money + -sample}
   |  |        Tick(1)
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- Expected Cost Body
   |  |  |
   |  |  `- [1 | ]
   |  |
   |  +- shift-max-template
   |  |  |
   |  |  `- 1 + [11 + money + -n | 11 + money + -n  0]
   |  |
   |  +- [Norms]
   |  |    [[1 | ],[11 + money + -n | 11 + money + -n  0]]
   |  |
   |  +- [Invariant]
   |  |    money  n ==> [1 | ] + h([1 | ],3/74[14 + money + -n | 14 + money + -n  0] + 3/74[15 + money + -n | 15 + money + -n  0] + 3/74[16 + money + -n | 16 + money + -n  0] + 3/74[17 + money + -n | 17 + money + -n  0] + 3/37[12 + money + -n | 12 + money + -n  0] + 3/37[13 + money + -n | 13 + money + -n  0] + 1/37[14 + money + -n | 14 + money + -n  0] + 1/37[15 + money + -n | 15 + money + -n  0] + 1/37[16 + money + -n | 16 + money + -n  0] + 1/37[17 + money + -n | 17 + money + -n  0] + 4/37[12 + money + -n | 12 + money + -n  0] + 4/37[13 + money + -n | 13 + money + -n  0] + 2/37[8 + money + -n | 8 + money + -n  0] + 2/37[7 + money + -n | 7 + money + -n  0] + 2/37[6 + money + -n | 6 + money + -n  0] + 2/37[5 + money + -n | 5 + money + -n  0] + 2/111[6 + money + -n | 6 + money + -n  0] + 2/111[5 + money + -n | 5 + money + -n  0] + 2/111[4 + money + -n | 4 + money + -n  0] + 2/111[3 + money + -n | 3 + money + -n  0] + 2/111[2 + money + -n | 2 + money + -n  0] + 2/111[1 + money + -n | 1 + money + -n  0] + 1/222[6 + money + -n | 6 + money + -n  0] + 1/222[5 + money + -n | 5 + money + -n  0] + 1/222[4 + money + -n | 4 + money + -n  0] + 1/222[3 + money + -n | 3 + money + -n  0] + 1/222[2 + money + -n | 2 + money + -n  0] + 1/222[1 + money + -n | 1 + money + -n  0])  h([1 | ],[11 + money + -n | 11 + money + -n  0])
   |  |    n  1 + money ==> 0  h([1 | ],[11 + money + -n | 11 + money + -n  0])
   |  |
   |  `- 74/15[11 + money + -n | 11 + money + -n  0]
   |
   `- 74/15[21 + -n | 21 + -n  0]

[Success] 74/15[21 + -n | 21
                  + -n  0]
Degree: 1