[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# Re: A spec for a trading algo

Hello Stephan,
thanks for your comments, I changed the spec accordingly. I used constant sets of price-changes and amounts to make the scenario I was looking for easier to produce, but anyway I don't show the error trace in the post so it doesn't matter.

Cheers.

------------------------------- MODULE Trade -------------------------------
EXTENDS Integers, Sequences, TLC

Min(m, n) == IF m < n THEN m ELSE n
Max(m, n) == IF m < n THEN n ELSE m

\* Operators for calculating the amount of equities we can afford to buy
SetMax(S) == CHOOSE i \in S : \A j \in S : i >= j
CalcAmount(funds, p) == LET S == { a \in 1..funds: a * p <= funds } IN
(IF S = {} THEN 0 ELSE SetMax(S))

\* Operator for choosing the highest bidder, should not get here if there are no bids
MaxBid(S) == CHOOSE b0 \in S : \A bid \in S : b0.bprice >= bid.bprice

\* Bid price can be higher or lower than current price
CalcPrice(p, c, up) == IF up THEN c + p ELSE Max(p - c, 1)

CONSTANTS Buyers,  \* The number of potential buyers in the simulation
PPrice,  \* The initial price of the equity
PAmount  \* The initial amount we trade

ASSUME /\ Buyers \in Nat \ {0}
/\ PPrice \in Nat \ {0}
/\ PAmount \in 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
priceChanges = 1..price,   \* Possible price changes - for this test limit to at most a 100% change during a round
amounts = 1..amount;       \* Possible bid amounts - only relevant amounts, for efficiency

macro PlaceBid(bids) {
with ( c \in priceChanges, higher \in BOOLEAN, num \in amounts ) {
bids := bids \cup { [bprice |-> CalcPrice(price, c, higher), bamount |-> num] };
}
}

macro PlaceMMBid(bids) {
either PlaceBid(bids)
or with ( num \in amounts ) {
bids := bids \cup { [bprice |-> CalcPrice(price, price-1, FALSE), bamount |-> num] }
}
}

process (MyAlgo = 0) {
sell: while (TRUE) {
await b = 0 ;                                      \* alternation flag - wait for your turn
if (amount = 0) {                                  \* done selling - 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
}
};
if (amount > 0) {                              \* make sure we managed to buy
priceChanges := 1..price;                  \* limit to at most a 100% change during a round
amounts := 1..amount;                      \* only relevant bid amounts
goto trade
}
else { goto broke }
} else {
if (\neg sold) {                               \* if we couldn't sell anything - lower the price
price := Max(price - 1, 1);
}
};
trade: b := 1;                                     \* pass the turn
};
broke: print ("Out of funds");
}

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

\* sell to any bidder with matching price
match: while (amount > 0 /\ \E b1 \in bids : b1.bprice >= price) {
with ( b0 = MaxBid(bids) ) {
with ( num = Min(amount, b0.bamount) ) {
bids := bids \ {b0};
amount := amount - num;
gains := gains + (b0.bprice * num);
sold := TRUE;
}
}
}
};
release: b := 0;  \* pass the turn
}
}
}

******************************************************************************)