[tlaplus] Re: Why is TLA_ complaining about this? (

On Wednesday, May 5, 2021 at 8:14:33 PM UTC-7 Leslie Lamport wrote:

By

   The invariant Prop is not a state predicate (one with no primes or temporal operators)".

TLC meant

The formula Prop that you claim to be an invariant is not an invariant because it is not a state
predicate (one with no primes or temporal operators).

If you still don't understand it, look up "state predicate" in "Specifying Systems".

On Wednesday, May 5, 2021 at 7:26:50 PM UTC-7 ns wrote:
hi Leslie, thanks for that explanation. It makes sense, but I'm still confused by what formulas TLC will accept. For example, the following as an invariant in the model
Prop == (x<y => [](x < y+1))
does not involve any actions. From what I can tell this ought to be a nice formula according to the rules in the book:
"A temporal state formula is one obtained from state predicates by applying simple Boolean operators and the temporal operators [], <>, and ~>"
This formula is constructed according to that rule. Yet TLC complains about it saying "The invariant Prop is not a state predicate (one with no primes or temporal operators)".

Thanks

On Tuesday, April 27, 2021 at 10:15:06 PM UTC-7 Leslie Lamport wrote:
TLA+ has syntactic rules to make it impossible to write a formula that is not insensitive to stuttering--formulas like [](x'=x+1). Whether an arbitrary formula made with [] and ' is insensitive to stuttering is undecidable. To keep the language simple, TLA+ uses rules that are stronger than necessary, but handle all the formulas that people should write. (For reasons I won't go into, writing complicated temporal logic formulas is a bad idea.) So you should understand the formulas that TLA+ does allow you to write, and don't try writing ones that TLA+ doesn't allow. You will find that TLC doesn't handle many properties that are legal TLA+ formulas that one would sometimes like to write. This is because those other properties don't arise very often, so enhancing TLC to handle them has low priority.

Leslie

On Tuesday, April 27, 2021 at 9:16:18 PM UTC-7 ns wrote:
I don't have any objection to what you just stated but I'm not seeing how it addresses my question. Consider the following
  [](p => []q)   (1)
This is saying that for every state, if p holds then henceforth in every state q must hold. By the same reasoning, I don't see why you can't have an "action oriented" version of this
[] [A => [][B]_vars]_vars (2)
which would read "for every step, if A holds of that step then henceforth B in every step or UNCHANGED vars must hold, or UNCHANGED vars". I hope that conveys my question a little better.

thanks

On Friday, April 23, 2021 at 6:20:26 PM UTC-7 andrew...@xxxxxxxxx wrote:
The logical formula in your action property must be true or false of a pair of states. The []F temporal operator is true or false of an infinite series of states.

Andrew

On Friday, April 23, 2021 at 3:38:28 PM UTC-4 ns wrote:
If I have a property of the form
[][A => (p /\  [] (q => r))]_vars   (1)
where A is an action and p,q,r are state predicates, I get two complaints:

Level error in applying operator $SquareAct:
The level of argument 1 exceeds the maximum level allowed by the operator.
and
=> has both temporal formula and action as arguments.

If I remove the nested [] then both complaints go away (and TLC is fine with too)
[][A => (p /\  (q => r))]_vars (2)
However, even if I replace the A with another state predicate the second complaint still remains.
Could someone tell me where I'm going wrong. I don't recall seeing any restriction on nesting of temporal operators in the Specifying Systems book but I could have quite easily missed it. Regarding why TLC accepts the second formula (2), I assume its "nice" because its considered a Box-Action formula?

thanks