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

Your formula is not syntactically well-formed: the formulas on both sides of '~>' must be temporal formulas but they are action formulas. Probably the easiest way to rewrite the property is to replace the actions by state predicates, something along the lines of

\A a \in Agent : bid_placed(a) ~> (winner(a) \/ has_withdrawn(a))

where bid_placed and has_withdrawn are state predicates that indicate that an agent has placed some bid or has withdrawn from the auction. You could also write

\A ... : (<><<Bid(a,b)>>_vars) ~> (winner(a) \/ <><<Withdraw(a)>>_vars)

which is equivalent to what you wrote, although this is perhaps not fully obvious. Unfortunately, TLC will (I believe) be unable to check this formula because it is not a "simple temporal formula" in the sense of section 14.2.4 of Specifying Systems.

Incidentally, I presume that `withdrawableBalances' is a constant, not a state variable? For otherwise, first TLC will again not accept the formula and second, the quantifier would take into account only the initial value of the variable.

It so happens that your formula is not a legal TLA formula although it is stuttering invariant and could be admitted in TLA. A long time ago I suggested an extension of TLA that would admit such formulas [1] but it was not found relevant enough in practice.

Stephan

[1] https://members.loria.fr/SMerz/papers/gtla.html

On 4 Dec 2020, at 09:58, Zhao Nan <jonathan.boatl@xxxxxxxxx> wrote:

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.

--
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/EEC4D8F0-FB1B-4E7C-9078-9A15A5B75414%40gmail.com.