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

*From*: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>*Date*: Sun, 16 Jul 2023 12:53:18 +0200*References*: <03591ea0-86a2-42b9-9e76-f92df35209a2n@googlegroups.com>

Hi Jerry, C2 states that `[]<>Q` if-and-only-if `P` holds for the *initial* state. In simpler terms, C2 is vacuously true. For comparison, you can try `[]C2`. Markus > On Jul 15, 2023, at 10:39 AM, Jerry Clcanny <a837940593@xxxxxxxxx> wrote: > > I am trying to understand `[]<>p`. > > I understand `<>` like this: The "eventually" operator in TLA+ (and similarly in LTL), denoted by `<>`, doesn't strictly mean "in the future" as it might in everyday language. Instead, it means "at some point" in a behavior, whether that point is in the past, present, or future. When we say that a property `P` is "eventually true", we mean that there exists a state in the behavior where `P` is true. This could be a state that has already occurred, the current state, or a state that will occur in the future. This is also why it's often more accurate to describe the `<>` operator as the "sometime" operator, rather than the "eventually" operator. > > I understand `[]<>p` like this: When we examine `[](<>(i = 0))`, it holds true for a behavior sequence (`s1 -> s2 -> s3 -> s4 -> ...`) if and only if `p` holds true for all **subsequences** starting from **each** state and continuing through its subsequent states (for example, `s1 -> s2 -> s3 -> ...`, `s2 -> s3 -> ...`, `s3 -> ...`, and so on). To summarize, the meaning of `[](<>p)` is that the property `p` is true **at some point** in each subsequence of the behavior. This point could be in the present or at some future time, but **not in the past**. > > So I think the following tla+ program should be error: > > ```tla > --------------------------- MODULE MC -------------------------------------- > \* MC.tla > EXTENDS Integers > VARIABLES i > > Init == i = 0 > > Next == > /\ i < 10 > /\ i' = i + 1 > > Spec == > /\ Init > /\ [][Next]_i > /\ WF_i(Next) > > P == > \/ i = 1 > \/ i = 8 > > Q == i = 2 > > C1 == P => (<>Q) > C2 == P => ([]<>Q) > ============================================================================ > ``` > > ```cfg > \* MC.cfg > SPECIFICATION > Spec > > PROPERTY > C2 > ``` > > But tlc says there is no error. -- 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/D33F13A1-C11B-4DBD-80BF-4BA5CBA15550%40lemmster.de.

**References**:**[tlaplus] About always and eventually.***From:*Jerry Clcanny

- Prev by Date:
**[tlaplus] About always and eventually.** - Next by Date:
**Re: [tlaplus] JavaNullPointerException on Prove Step or Module - problem persisted but has now vanished** - Previous by thread:
**[tlaplus] About always and eventually.** - Next by thread:
**[tlaplus] Directed Graph from Specifying Systems** - Index(es):