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

*From*: pascal.s...@xxxxxxxxx*Date*: Fri, 27 Jul 2018 05:47:22 -0700 (PDT)

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

**Follow-Ups**:**Re: What do formulas inside "[]" operate on?***From:*valentin . . . .

**Re: [tlaplus] What do formulas inside "[]" operate on?***From:*Stephan Merz

- Prev by Date:
**Need help in debugging/understanding concurrency concept** - Next by Date:
**Re: [tlaplus] What do formulas inside "[]" operate on?** - Previous by thread:
**Re: [tlaplus] Re: Need help in debugging/understanding concurrency concept** - Next by thread:
**Re: [tlaplus] What do formulas inside "[]" operate on?** - Index(es):