Re: A spec for a trading algo

[ecurb...@xxxxxxxxx]

Hi Nira,

I am taking a look at your TLA+ code. Thanks for posting it. Do you have some values for the model that you used for the constants?

Regards,
Bruce
On Sunday, November 15, 2015 at 4:41:05 PM UTC+1, Nira Amit wrote:
> Hi all,
> I created a spec of a made-up trading algorithm for a post advocating the use of TLA+ by software designers. The idea is to show that the model-checker can identify behaviors similar to those that happened during the 2010 Flash Crash (namely trading against stub-quotes and volatile prices with a downward trend). But as I myself am quite new to TLA+, it would be reassuring if someone a bit more experienced could have a look to see that the spec makes sense, and that this example is a reasonable representation of TLA's abilities (if only as a "teaser").
> 
> 
> My post is here: https://www.linkedin.com/pulse/lamports-tla-spec-testing-why-youre-using-nira-amit
> And the spec is below. The MyAlgo process "identifies" upward-trends in prices, buys and tries to sell immediately. The Matcher process simulates bids every time MyAlgo wants to sell. There is an invariant checking that at the end of each buy-and-sell session there are enough funds for another round, and it fails when you run TLC (which is what I want).
> I'd appreciate any comments.
> 
> 
> 
> ------------------------------- MODULE Trade -------------------------------
> EXTENDS Integers, Sequences
> 
> 
> Min(m, n) == IF m < n THEN m ELSE n
> Max(m, n) == IF m < n THEN n ELSE m
> 
> 
> SetMax(S) == CHOOSE i \in S : \A j \in S : i >= j
> CalcAmount(funds, p) == SetMax( { a \in 1..funds: a * p <= funds } )
> MaxBid(S) == CHOOSE b0 \in S : \A bid \in S : b0[1] >= bid[1]
> CalcPrice(p, c, up) == IF up THEN c + p ELSE Max(p - c, 1) 
> 
> 
> CONSTANTS Buyers, PPrice, PAmount, PriceChanges, Amounts
> 
> 
> ASSUME /\ Buyers \in Nat \ {0}
>        /\ PPrice \in Nat \ {0}
>        /\ PAmount \in Nat \ {0}
>        /\ PriceChanges \in SUBSET (Nat \ {0})
>        /\ Amounts \in SUBSET (Nat \ {0})
>        
> (*****************************************************************************
> --algorithm Trader {
> 
> 
>     variable b = 0,           \* This variable controls the alternation between "our" actions and the "market's" actions 
>     price = PPrice,           \* The latest price of the stock 
>     amount = PAmount,         \* The amount of stocks we currently hold
>     worth = PAmount * PPrice, \* Our total worth at the beginning of a round
>     gains = 0,                \* Total gains at the end of a round
>     sold = FALSE;             \* whether or not we managed to sell in the previous tick 
>     
>     macro PlaceBid(bids) {
>         with ( c \in PriceChanges, higher \in BOOLEAN, num \in Amounts ) {
>             bids := bids \cup {<< CalcPrice(price, c, higher), num>>}; 
>         } 
>     }
>     
>     macro PlaceMMBid(bids) {
>         either PlaceBid(bids) 
>         or with ( num \in Amounts ) {
>             bids := bids \cup {<< CalcPrice(price, price-1, FALSE), num>>}
>         }
>     }
>     
>     process (MyAlgo = 0) { 
>         sell: while (TRUE) { 
>             await b = 0 ;      \* alternation flag - wait for your turn
>             if (amount = 0) {  \* whenever we're done selling - assume we identified an up-trend and start another round
>                 with (c \in PriceChanges) {
>                     with ( pprice = c + price ) {  \* new price increased by some c
>                         amount := CalcAmount(gains, pprice);
>                         worth := gains;            \* current total worth of our assets
>                         gains := gains - (amount * pprice);  \* remember the "change" left after buying stocks
>                         price := 1 + pprice  \* try to sell higher
>                     }
>                 }
>             } else {
>                 if (\neg sold) { price := Max(price - 1, 1); }  \* if we couldn't sell anything - lower the price
>             };
>             b := 1;  \* pass the turn
>         }
>     }
>     
>     fair process (Matcher = 1)  
>         variables bids, i;
>     {   buy: while (TRUE) {
>             await b = 1 ;    \* alternation flag - wait for your turn
>             if (amount > 0) {    \* if the trader is selling, create some bids 
>                 sold := FALSE; bids := {}; i := 0;
>                 FillBook: while (i < Buyers) {
>                     either { \* bid some price on some amount
>                         PlaceBid(bids);
>                         i := i+1
>                     }
>                     or { i := i+1 } \* no bid from this buyer
>                 };
>                 PlaceMMBid(bids); \* at least one bid, from market-maker
>             
>                 match: while (amount > 0 /\ \E b1 \in bids : b1[1] >= price) {  \* sell to any bidder with matching price
>                     with ( b0 = MaxBid(bids) ) {
>                         with ( num = Min(amount, b0[2]) ) {
>                             bids := bids \ {b0};
>                             amount := amount - num;
>                             gains := gains + (b0[1] * num); 
>                             sold := TRUE;
>                         }
>                     }
>                 }
>             };
>             release: b := 0;  \* pass the turn  
>         } 
>     }
> }
> 
> 
> ******************************************************************************)
> \* BEGIN TRANSLATION
> ...
> \* END TRANSLATION
> 
> 
> 
> \* Invariant: after each selling round there are enough funds to buy at least one more stock
> NotBroke == (amount = 0) => (\A c \in PriceChanges : gains >= price + c)
> =============================================================================