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

*From*: Martin <martin...@xxxxxxxxxxxxxx>*Date*: Wed, 11 Jan 2017 14:59:06 +0100*References*: <deb8973e-e74b-4dd2-b2f6-beea4e75e5d6@googlegroups.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.6.0

Hello, I hope I'm not giving a too narrow answer, but on p89 of Specifying Systems you see the two ways, box can be applied: * [] P where P is a state formula * [] [A]_v where A is an action and v is a state function The same holds for <> P and <> <A>_v. Now the formula []<> <A>_v \/ <B>_v is not covered these rules. If i understand it correctly, the reason for this requirement is that for actions, stuttering needs to be taken into account (the informal description is on p. 17 of the book). The syntactic convention ensures that the variables modulo which the box operator stutters are explicit. It also prevents cases such as []<> <A>_x \/ <B>_y, where the variables stuttered on are not the same. I hope this helps, cheers Martin On 01/11/2017 01:32 PM, George Singer 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? >

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

- Prev by Date:
**Why is this an invalid TLA formula?** - Next by Date:
**Re: [tlaplus] Why is this an invalid TLA formula?** - Previous by thread:
**Why is this an invalid TLA formula?** - Next by thread:
**Re: [tlaplus] Why is this an invalid TLA formula?** - Index(es):