Re: [tlaplus] What do formulas inside "[]" operate on?

[Stephan Merz <stepha...@xxxxxxxxx>]

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.