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
}
}
}
******************************************************************************)