tla+

TLC passes property but the state is not existed

I'm a new user of TLA+. The following code might be silly. It's a narrowed-down version of my private code.
There are no lines assigning END to s on the following code but the Prop passes without error on TLC model check.

----------------------------- MODULE notExisted -----------------------------
EXTENDS Sequences
VARIABLES s, q

Init == /\ s = "S0"
        /\ q = <<>>

sub_nxt == /\ q' = Append(q, "wow")
           /\ UNCHANGED<<s>>

Next == \/ /\ s = "S0"
           /\ s' = "S1"
           /\ UNCHANGED<<q>>

Spec == /\ Init
        /\ [][Next]_<<s,q>>
        /\ SF_<<s,q>>(sub_nxt)

Prop == []<>(s = "END")

=============================================================================

I can't figure out why it passes. There might be bad pattern on my code.
Can anyone explain? The TLA+ version is 1.7.1. The OS is Ubuntu 20.04. Thanks.

Solution

  • It is a self-answer. I checked Specifying Systems "14.3.5 Limitations of Liveness Checking" and finally figured out what was wrong. I think...
    The SF is False since the Spec is finite and sub_nxt always true.
    In that case, the SF_<<s,q>>(sub_nxt) => []<>(s = "END") is true.
    The A => B is true when A is false.

    I've also tried following and it also passes.

    --------------------------- MODULE LimOfLivCheck ---------------------------
EXTENDS Integers
VARIABLE x

Spec == (x=0) /\ [][x' = x + 2 /\ x < 10]_x /\ WF_x(x' = x + 2)

Prop == []<>(x=1)

=============================================================================