[tlaplus] About always and eventually.

[Jerry Clcanny <a837940593@xxxxxxxxx>]

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/03591ea0-86a2-42b9-9e76-f92df35209a2n%40googlegroups.com.