[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Why is this an invalid TLA formula?
(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,
> On 11 Jan 2017, at 13:32, George Singer <george....@xxxxxxxxx> wrote:
> 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?
> 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.