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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Fri, 4 Dec 2020 12:26:41 +0100*References*: <1f1a9e8d-88ce-4d5e-9dc5-41ebbae1c071n@googlegroups.com>

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
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. |

**References**:**[tlaplus] How to say "Taking Action A leads to X"?***From:*Zhao Nan

- Prev by Date:
**[tlaplus] How to say "Taking Action A leads to X"?** - Next by Date:
**[tlaplus] A temporal formula to specify that the value of a record does not change** - Previous by thread:
**[tlaplus] How to say "Taking Action A leads to X"?** - Next by thread:
**[tlaplus] A temporal formula to specify that the value of a record does not change** - Index(es):