# [tlaplus] How to say "Taking Action A leads to X"?

Hi,
I'm relatively new to TLA+. I'm practicing. Currently, I want to specify an auction. My spec has 4 actions:
- 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)?

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.