Re: [tlaplus] About always and eventually.

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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.