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

[Martin <martin...@xxxxxxxxxxxxxx>]

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