Hi,
I'm relatively new to TLA+. I'm practicing. Currently, I want to specify an auction. My spec has 4 actions:
- Tick, advancing the clock
- Bid(a,b) which is enabled if Agent a makes a bid b higher than the current highest bid
- Close, which is enabled if the clock value is large enough
- Withdraw(a), which lets an unsuccessful bidder a retrieve their funds
My goal is formulating (and hopefully eventually proving) the following main property:
"If someone makes a bid, they will eventually either (1) be able to retrieve their funds, or (2) be the winner of the auction."
My idea was writing something like this:
Main == \A a \in Agents : \A b \in 1..withdrawableBalances[a] : <<Bid(a,b)>>_vars ~> ((winner(a) \/ <<OAWithdraw(a)>>_vars))
However, the TLA toolbox reports "Action used where only temporal formula or state predicate allowed."
What's my mistake here? How do I express that if an action is "taken", it will lead to something else happening (either a state or another action being taken, with appropriate fairness spec)?