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

[tlaplus] About always and eventually.

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:

--------------------------- MODULE MC --------------------------------------
\* MC.tla
EXTENDS Integers

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)

\* MC.cfg


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.