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

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

   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.