Expected Cost | +- [f] | 0 | +- [Program] | money :~ {1 : 10000} | 0:While(money ≥ n) | Choice | 36/37: Choice | 1/3: Choice | 1/2: r :~ {1/4 : 3;1/4 : 4;1/4 : 5;1/4 : 6} | money :~ {1 : money + r} | 1/2: r :~ {1/2 : 1;1/2 : 2} | money :~ {1 : money + r} | 2/3: Choice | 1/2: Choice | 1/3: r :~ {1/4 : 3;1/4 : 4;1/4 : 5;1/4 : 6} | money :~ {1 : money + r} | 2/3: r :~ {1/2 : 1;1/2 : 2} | money :~ {1 : money + r} | 1/2: Choice | 2/3: r :~ {1/4 : 3;1/4 : 4;1/4 : 5;1/4 : 6} | money :~ {1 : money + -r} | 1/3: r :~ {1/6 : 5;1/6 : 6;1/6 : 7;1/6 : 8;1/6 : 9;1/6 : 10} | money :~ {1 : money + -r} | 1/37: r :~ {1/6 : 5;1/6 : 6;1/6 : 7;1/6 : 8;1/6 : 9;1/6 : 10} | money :~ {1 : money + -r} | Tick(1) | +- While.step | | | +- [Problem] | | 0:While(money ≥ n) | | Choice | | 36/37: Choice | | 1/3: Choice | | 1/2: r :~ {1/4 : 3;1/4 : 4;1/4 : 5;1/4 : 6} | | money :~ {1 : money + r} | | 1/2: r :~ {1/2 : 1;1/2 : 2} | | money :~ {1 : money + r} | | 2/3: Choice | | 1/2: Choice | | 1/3: r :~ {1/4 : 3;1/4 : 4;1/4 : 5;1/4 : 6} | | money :~ {1 : money + r} | | 2/3: r :~ {1/2 : 1;1/2 : 2} | | money :~ {1 : money + r} | | 1/2: Choice | | 2/3: r :~ {1/4 : 3;1/4 : 4;1/4 : 5;1/4 : 6} | | money :~ {1 : money + -r} | | 1/3: r :~ {1/6 : 5;1/6 : 6;1/6 : 7;1/6 : 8;1/6 : 9;1/6 : 10} | | money :~ {1 : money + -r} | | 1/37: r :~ {1/6 : 5;1/6 : 6;1/6 : 7;1/6 : 8;1/6 : 9;1/6 : 10} | | money :~ {1 : money + -r} | | 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·[10011 + -n | 10011 + -n ≥ 0]