[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?