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").
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)
=============================================================================