ExecutionLog | `- Expected Cost | +- [f] | 0 | +- [Program] | z :~ {1 : 0} | 0:While(sPrice 1 + minPrice) | Choice | 1/4: sPrice :~ {1 : 1 + sPrice} | 3/4: sPrice :~ {1 : -1 + sPrice} | numShares :~ {1/6 : -2;1/6 : -1;1/6 : 0;1/6 : 1;1/6 : 2;1/6 : 3} | 1:While(numShares 1) | numShares :~ {1 : -1 + numShares} | z :~ {1 : sPrice + z} | 2:While(0 1 + numShares) | numShares :~ {1 : 1 + numShares} | z :~ {1 : -sPrice + z} | Tick(z) | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | 0:While(sPrice 1 + minPrice) | | Choice | | 1/4: sPrice :~ {1 : 1 + sPrice} | | 3/4: sPrice :~ {1 : -1 + sPrice} | | numShares :~ {1/6 : -2;1/6 : -1;1/6 : 0;1/6 : 1;1/6 : 2;1/6 : 3} | | 1:While(numShares 1) | | numShares :~ {1 : -1 + numShares} | | z :~ {1 : sPrice + z} | | 2:While(0 1 + numShares) | | numShares :~ {1 : 1 + numShares} | | z :~ {1 : -sPrice + z} | | | `- 0 | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | Tick(z) | | | `- [z | z 0] | +- Expected Cost | | | +- [f] | | [z | z 0] | | | +- [Program] | | 0:While(sPrice 1 + minPrice) | | Choice | | 1/4: sPrice :~ {1 : 1 + sPrice} | | 3/4: sPrice :~ {1 : -1 + sPrice} | | numShares :~ {1/6 : -2;1/6 : -1;1/6 : 0;1/6 : 1;1/6 : 2;1/6 : 3} | | 1:While(numShares 1) | | numShares :~ {1 : -1 + numShares} | | z :~ {1 : sPrice + z} | | 2:While(0 1 + numShares) | | numShares :~ {1 : 1 + numShares} | | z :~ {1 : -sPrice + z} | | | +- While.step | | | | | +- [Problem] | | | 0:While(sPrice 1 + minPrice) | | | Choice | | | 1/4: sPrice :~ {1 : 1 + sPrice} | | | 3/4: sPrice :~ {1 : -1 + sPrice} | | | numShares :~ {1/6 : -2;1/6 : -1;1/6 : 0;1/6 : 1;1/6 : 2;1/6 : 3} | | | 1:While(numShares 1) | | | numShares :~ {1 : -1 + numShares} | | | z :~ {1 : sPrice + z} | | | 2:While(0 1 + numShares) | | | numShares :~ {1 : 1 + numShares} | | | z :~ {1 : -sPrice + z} | | | | | +- [f] | | | [z | z 0] | | | | | +- While.step | | | | | | | +- [Problem] | | | | 2:While(0 1 + numShares) | | | | numShares :~ {1 : 1 + numShares} | | | | z :~ {1 : -sPrice + z} | | | | | | | +- [f] | | | | [z | z 0] | | | | | | | +- linear-template | | | | | | | | | `- 1 + [-numShares | -numShares 0] + [-numShares | -numShares 0][-sPrice | -sPrice 0] + [z | z 0] | | | | | | | +- [Norms] | | | | [[1 | ],[-numShares | -numShares 0],[numSharessPrice | -numShares 0 -sPrice 0],[z | z 0]] | | | | | | | +- [Invariant] | | | | 0 1 + numShares ==> 0 + h([1 | ],-1[1 + numShares | -1 + -numShares 0],[numSharessPrice + sPrice | -1 + -numShares 0 -sPrice 0],[-sPrice + z | -sPrice + z 0]) h([1 | ],[-numShares | -numShares 0],[numSharessPrice | -numShares 0 -sPrice 0],[z | z 0]) | | | | 1 + numShares 1 ==> [z | z 0] h([1 | ],[-numShares | -numShares 0],[numSharessPrice | -numShares 0 -sPrice 0],[z | z 0]) | | | | | | | `- [numSharessPrice | -numShares 0 -sPrice 0] + [z | z 0] | | | | | +- Expected Cost | | | | | | | +- [f] | | | | [numSharessPrice | -numShares 0 -sPrice 0] | | | | | | | +- [Program] | | | | 1:While(numShares 1) | | | | numShares :~ {1 : -1 + numShares} | | | | z :~ {1 : sPrice + z} | | | | | | | +- While.step | | | | | | | | | +- [Problem] | | | | | 1:While(numShares 1) | | | | | numShares :~ {1 : -1 + numShares} | | | | | z :~ {1 : sPrice + z} | | | | | | | | | +- [f] | | | | | [numSharessPrice | -numShares 0 -sPrice 0] | | | | | | | | | +- linear-template | | | | | | | | | | | `- 1 + [numSharessPrice | -numShares 0 -sPrice 0] + [numShares | numShares 0] + [numShares | numShares 0][-sPrice | -sPrice 0] | | | | | | | | | +- [Norms] | | | | | [[1 | ],[numSharessPrice | -numShares 0 -sPrice 0],[numShares | numShares 0],[-numSharessPrice | numShares 0 -sPrice 0]] | | | | | | | | | +- [Invariant] | | | | | numShares 1 ==> 0 + h([1 | ],[numSharessPrice + -sPrice | 1 + -numShares 0 -sPrice 0],[-1 + numShares | -1 + numShares 0],-1[numSharessPrice + -sPrice | -1 + numShares 0 -sPrice 0]) h([1 | ],[numSharessPrice | -numShares 0 -sPrice 0],[numShares | numShares 0],[-numSharessPrice | numShares 0 -sPrice 0]) | | | | | 1 1 + numShares ==> [numSharessPrice | -numShares 0 -sPrice 0] h([1 | ],[numSharessPrice | -numShares 0 -sPrice 0],[numShares | numShares 0],[-numSharessPrice | numShares 0 -sPrice 0]) | | | | | | | | | `- [numSharessPrice | -numShares 0 -sPrice 0] | | | | | | | `- [numSharessPrice | -numShares 0 -sPrice 0] | | | | | +- Expected Cost | | | | | | | +- [f] | | | | [z | z 0] | | | | | | | +- [Program] | | | | 1:While(numShares 1) | | | | numShares :~ {1 : -1 + numShares} | | | | z :~ {1 : sPrice + z} | | | | | | | +- While.step | | | | | | | | | +- [Problem] | | | | | 1:While(numShares 1) | | | | | numShares :~ {1 : -1 + numShares} | | | | | z :~ {1 : sPrice + z} | | | | | | | | | +- [f] | | | | | [z | z 0] | | | | | | | | | +- linear-template | | | | | | | | | | | `- 1 + [numShares | numShares 0] + [numShares | numShares 0][sPrice | sPrice 0] + [z | z 0] | | | | | | | | | +- [Norms] | | | | | [[1 | ],[numShares | numShares 0],[numSharessPrice | numShares 0 sPrice 0],[z | z 0]] | | | | | | | | | +- [Invariant] | | | | | numShares 1 ==> 0 + h([1 | ],[-1 + numShares | -1 + numShares 0],[numSharessPrice + -sPrice | -1 + numShares 0 sPrice 0],[sPrice + z | sPrice + z 0]) h([1 | ],[numShares | numShares 0],[numSharessPrice | numShares 0 sPrice 0],[z | z 0]) | | | | | 1 1 + numShares ==> [z | z 0] h([1 | ],[numShares | numShares 0],[numSharessPrice | numShares 0 sPrice 0],[z | z 0]) | | | | | | | | | `- [numSharessPrice | numShares 0 sPrice 0] + [z | z 0] | | | | | | | `- [numSharessPrice | numShares 0 sPrice 0] + [z | z 0] | | | | | +- linear-template | | | | | | | `- 1 + [1 + minPrice | 1 + minPrice 0] + [1 + sPrice | 1 + sPrice 0][-minPrice + sPrice | -minPrice + sPrice 0] + [-minPrice + sPrice | -minPrice + sPrice 0] + [z | z 0] | | | | | +- [Norms] | | | [[1 | ],[1 + minPrice | 1 + minPrice 0],[-minPrice + -minPricesPrice + sPrice + sPrice^2 | 1 + sPrice 0 -minPrice + sPrice 0],[-minPrice + sPrice | -minPrice + sPrice 0],[z | z 0]] | | | | | +- [Invariant] | | | minPrice 0 sPrice 1 + minPrice ==> 0 + h([1 | ],[1 + minPrice | 1 + minPrice 0],1/4[2 + -2(minPrice) + -minPricesPrice + 3(sPrice) + sPrice^2 | 1 + -minPrice + sPrice 0 2 + sPrice 0] + 3/4[-minPricesPrice + -sPrice + sPrice^2 | -1 + -minPrice + sPrice 0 sPrice 0],1/4[1 + -minPrice + sPrice | 1 + -minPrice + sPrice 0] + 3/4[-1 + -minPrice + sPrice | -1 + -minPrice + sPrice 0],-1/12[1 + sPrice | -1 + -sPrice 0] + 1/24[z | z 0] + -1/24[1 + sPrice | -1 + -sPrice 0] + 1/24[z | z 0] + 1/24[z | z 0] + 1/24[1 + sPrice | 1 + sPrice 0] + 1/24[z | z 0] + 1/12[1 + sPrice | 1 + sPrice 0] + 1/24[z | z 0] + 1/8[1 + sPrice | 1 + sPrice 0] + 1/24[z | z 0] + -1/4[-1 + sPrice | 1 + -sPrice 0] + 1/8[z | z 0] + -1/8[-1 + sPrice | 1 + -sPrice 0] + 1/8[z | z 0] + 1/8[z | z 0] + 1/8[-1 + sPrice | -1 + sPrice 0] + 1/8[z | z 0] + 1/4[-1 + sPrice | -1 + sPrice 0] + 1/8[z | z 0] + 3/8[-1 + sPrice | -1 + sPrice 0] + 1/8[z | z 0]) h([1 | ],[1 + minPrice | 1 + minPrice 0],[-minPrice + -minPricesPrice + sPrice + sPrice^2 | 1 + sPrice 0 -minPrice + sPrice 0],[-minPrice + sPrice | -minPrice + sPrice 0],[z | z 0]) | | | 1 + minPrice 1 + sPrice minPrice 0 ==> [z | z 0] h([1 | ],[1 + minPrice | 1 + minPrice 0],[-minPrice + -minPricesPrice + sPrice + sPrice^2 | 1 + sPrice 0 -minPrice + sPrice 0],[-minPrice + sPrice | -minPrice + sPrice 0],[z | z 0]) | | | | | `- [minPrice 0] (2[-minPrice + -minPricesPrice + sPrice + sPrice^2 | 1 + sPrice 0 -minPrice + sPrice 0] + [z | z 0]) | | | `- [minPrice 0] (2[-minPrice + -minPricesPrice + sPrice + sPrice^2 | 1 + sPrice 0 -minPrice + sPrice 0] + [z | z 0]) | `- [minPrice 0] 2[-minPrice + -minPricesPrice + sPrice + sPrice^2 | 1 + sPrice 0 -minPrice + sPrice 0] [Success] [minPrice 0] 2[-minPrice + -minPricesPrice + sPrice + sPrice^2 | 1 + sPrice 0 -minPrice + sPrice 0] Degree: 2