Why is this an invalid TLA formula?

[George Singer]

At the top of page 95 of *Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers*, Lamport states that

$$
\Box \Diamond ( \langle A \rangle_v \vee \langle B \rangle_v)
$$

is not a valid TLA formula, even though its equivalent formulation

$$
\Box \Diamond \langle A \vee B \rangle_v
$$

*is* a valid TLA formula.

**Question:** Why is the first formula invalid and the second formula valid?

[Martin]

Hello,

I hope I'm not giving a too narrow answer, but on p89 of Specifying
Systems you see the two ways, box can be applied:

* [] P where P is a state formula
* [] [A]_v where A is an action and v is a state function

The same holds for <> P and <> <A>_v. Now the formula []<> <A>_v \/
<B>_v is not covered these rules.

If i understand it correctly, the reason for this requirement is that
for actions, stuttering needs to be taken into account (the informal
description is on p. 17 of the book). The syntactic convention ensures
that the variables modulo which the box operator stutters are explicit.
It also prevents cases such as []<> <A>_x \/ <B>_y, where the variables
stuttered on are not the same.

I hope this helps,
cheers Martin

[Stephan Merz]

(Temporal) formulas are inductively defined as

- state predicates,
- [][A]_v and <> <<A>>_v for an action A and a state formula v,
- Boolean combinations of temporal formulas,
- []F and <>F for temporal formulas (and the derived forms F ~> G, WF_v(A), SF_v(A)),
- \E x : F, \A x : F, \EE v : F, \AA v : F,
- F -+-> G

It follows from the above that

[]<>( <<A>>_v \/ <<B>>_v )

is simply not a syntactically well-formed formula of TLA whereas

[]<> << A \/ B >>_v

is. If the first one were a formula, the two were semantically equivalent.

Hope this helps,
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+u...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.