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

[Zhao Nan <jonathan.boatl@xxxxxxxxx>]

   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)?

-- 
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1f1a9e8d-88ce-4d5e-9dc5-41ebbae1c071n%40googlegroups.com.