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

*From*: ns <nedsri1988@xxxxxxxxx>*Date*: Tue, 27 Apr 2021 21:16:18 -0700 (PDT)*Ironport-hdrordr*: A9a23:RsydL6F0TQ26pWDvpLqFR5HXdLJzesId70hD6mlaTxtJfsuE0/2/hfhz726JtB89elEF3eqBNq6JXG/G+fdOi+QsFJqrQQWOghrNEKhM9o3nqgeQfBHW1ukY7qt4drg7NduYNykDse/e4BOkV/46ytiG76zAv5ap815JTRt2L4Bt6h4RMHftLmRSRBNaQboVfaDslfZvgjq7ZDAvaN6nb0N1K9Trgt3QidbbZgQbDAQs8wmEgVqTmffHOjy5+jtbbD9V27cl9gH+4nHEz4Gqs/S6zRGZ0m/I8v1t6avc4/9OHtaFhMRQCjiEsHfQWK1ZQLGJsD04p+uigWxa4eXkmBsrM8Rt5365RAjcymqO5yDa3Dkj8HPkw1OD6EGT2vDRfz4iDtoEuIQxSGqm12MbsNZw3Lkj5Q2knqBKBhDNljmV3amzazhWkCOP0BwfuN9WpHBSVrYeZKRcxLZvn399IdMvGGbf5Jo8GOdjSPvA7OtbGGn1U1np+kdoxtKoUjAfPDejBnIDtMucziRMkBlCo3cw9YgwmHEP8Z54ZYJD+/2BEqkArsA6cuYmKYx6AukFTY+MDnHVBSjLLHmZLT3cdZ0vCjbqsJ744LI84aWRdJsEwIBaouW/bHpo8VU/cU7vFsGCtacqg3XwaVT4Zy3kzoV15pRyuLHwAJrtdQOZTkw2+vHQ0ckiPg==*References*: <9448bd47-eee3-452d-bcfd-74d4a5a80595n@googlegroups.com> <861a35d0-dc74-43a2-bbb1-c1015063bb0an@googlegroups.com>

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.

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

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+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/526d9972-25ac-4717-9510-7779b15bd722n%40googlegroups.com.

**Follow-Ups**:**[tlaplus] Re: Why is TLA_ complaining about this? (***From:*Leslie Lamport

**References**:**[tlaplus] Why is TLA_ complaining about this? (***From:*ns

**[tlaplus] Re: Why is TLA_ complaining about this? (***From:*Andrew Helwer

- Prev by Date:
**Re: [tlaplus] Different trace for a temporal property violation (stuttering) using same seed and fp** - Next by Date:
**[tlaplus] Re: Why is TLA_ complaining about this? (** - Previous by thread:
**[tlaplus] Re: Why is TLA_ complaining about this? (** - Next by thread:
**[tlaplus] Re: Why is TLA_ complaining about this? (** - Index(es):