Re: [tlaplus] Why is this an invalid TLA formula?

[Stephan Merz <stepha...@xxxxxxxxx>]

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