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

Why is this an invalid TLA formula?



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?