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

*From*: Jerry Clcanny <a837940593@xxxxxxxxx>*Date*: Sat, 15 Jul 2023 01:39:30 -0700 (PDT)

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.

**Follow-Ups**:**Re: [tlaplus] About always and eventually.***From:*Markus Kuppe

- Prev by Date:
**Re: [tlaplus] TLA+ and C++ templates** - Next by Date:
**Re: [tlaplus] About always and eventually.** - Previous by thread:
**Re: [tlaplus] About stuttering steps and deadlock in TLC** - Next by thread:
**Re: [tlaplus] About always and eventually.** - Index(es):