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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Fri, 27 Jul 2018 14:55:08 +0200*References*: <84a13c5d-0399-44b8-9ed1-a0020bc56801@googlegroups.com>

Hello Pascal, you are completely right: P ~> Q is shorthand for [](P => <>Q), and your semantic intuitions are correct. For more details on the semantics of TLA, you may want to look at [1]. In fact, the equivalence holds not just for state predicates P and Q, but even if P and Q are arbitrary temporal formulas. Equivalences such as this one are not typically checked using TLC, although you could create a spec in which P and Q are just Boolean variables that can change values non-deterministically and then verify the two implications separately. Regards, Stephan [1] https://members.loria.fr/SMerz/papers/tla+logic2008.html > On 27 Jul 2018, at 14:47, pascal.s...@xxxxxxxxx wrote: > > Hi, newbie here. > > I was playing around with "~>" and wondering if it can be defined in terms of "[]" and "<>". > > So I came up with this: I think "P ~> Q" is equivalent to "[](P => <>Q)". Unfortunately, I can't compare the two above Temporal Formulas with <=>, as TLC shouts "cannot handle" at me when I try.. > > When Lamport mentioned that applying a state formula to a behaviour is the same as applying it to the first state of that behaviour, similarly for action formulas, I came up with the intuition that "[]" and "<>" could therefore probably be seen as quantifiers over every possible suffix of a behaviour. > > (I'm also assuming that what Lamport calls a behaviour is just a sequence of states. Please correct me if I'm wrong.) > > This now leads me to believe that the above equivalence holds, because of the following argument: > > Let P and Q be state formulas, and let B be a behaviour, then []P applied to B (as I understand it) means "(\A B_s \in suffixes(B) : P applied to B_s)". And since P applied to a behaviour is the same a P applied to the first state of that behaviour, then "[](P => <>Q)" means that for every state s in B where P is true, Q must hold true in some state t in the suffix of B, starting at s, which is equivalent to the definition of "~>". > > Can anyone confirm or refute my assumptions, such as the assumption that everything inside of "[]" operates on a suffix? Thank you very much for your time and sorry for the long post. > > Best regards > Pascal > > -- > 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+u...@xxxxxxxxxxxxxxxx. > To post to this group, send email to tla...@xxxxxxxxxxxxxxxx. > Visit this group at https://groups.google.com/group/tlaplus. > For more options, visit https://groups.google.com/d/optout.

**References**:**What do formulas inside "[]" operate on?***From:*pascal . s . . .

- Prev by Date:
**What do formulas inside "[]" operate on?** - Next by Date:
**Re: What do formulas inside "[]" operate on?** - Previous by thread:
**What do formulas inside "[]" operate on?** - Next by thread:
**Re: What do formulas inside "[]" operate on?** - Index(es):