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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Wed, 11 Jan 2017 15:58:46 +0100*References*: <deb8973e-e74b-4dd2-b2f6-beea4e75e5d6@googlegroups.com>

(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 > 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.

**References**:**Why is this an invalid TLA formula?***From:*George Singer

- Prev by Date:
**Re: [tlaplus] Why is this an invalid TLA formula?** - Next by Date:
**Is TLA+ still useful if your implementation language is a purely functional one, like Haskell?** - Previous by thread:
**Re: [tlaplus] Why is this an invalid TLA formula?** - Next by thread:
**Is TLA+ still useful if your implementation language is a purely functional one, like Haskell?** - Index(es):