Using (U)ntil operator in SPIN ltl formula

I am trying to understand how to correctly use the Until operator in an ltl formula. I found this definition (below) to be clear:

Until

AUB: true if there exists i such that:

B is true in [s_i, s_i+1, s_i+2, … ]

for all j such that 0 ≤ j < i, formula A is true in [s_j, s_j+1, s_j+2, … ]

meaning:

B is true at time i

for times between 0 and i-1, formula A is true

still using the formalization of "true at time i"

Sample code with example ltl formula:

mtype = {Regular, Reverse, Quit}

mtype state = Regular;

init {
do ::
   if
   ::state == Regular -> state = Reverse
   ::state == Reverse -> state = Quit
   ::state == Quit -> break
   fi
od
}

ltl p0 { [] ((state == Reverse) U (state != Reverse))}

Based on the definition of the until operator that I gave, I don't understand how the above ltl formula is not producing any errors. Wouldn't state == Reverse need to be true for all time up until state != Reverse? Initially state == Regular.

Below is the SPIN output after running the test:

(Spin Version 6.4.6 -- 2 December 2016)
    + Partial Order Reduction

Full statespace search for:
    never claim             + (p0)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     + (fairness disabled)
    invalid end states  - (disabled by never claim)

State-vector 28 byte, depth reached 13, errors: 0
        9 states, stored (11 visited)
        2 states, matched
       13 transitions (= visited+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.000   equivalent memory usage for states (stored*(State-vector + overhead))
    0.288   actual memory usage for states
  128.000   memory used for hash table (-w24)
    0.534   memory used for DFS stack (-m10000)
  128.730   total actual memory usage


unreached in init
    (0 of 12 states)
unreached in claim p0
    _spin_nvr.tmp:14, state 20, "-end-"
    (1 of 20 states)

pan: elapsed time 0 seconds

STRONG UNTIL

Its formal definition is:

M, s_k ⊨ ϕ U ψ

<->

∃ j ∈ N .

(j ≥ k) ∧

∀ i ∈ N . ((k ≤ i < j) ⇒ (<s_i, s_i+1> ∈ R_t)) ∧

(M, s_j ⊨ ψ) ∧

∀ i ∈ N . ((k ≤ i < j) ⇒ (M, s_i ⊨ ϕ))

where

M is the Kripke Structure

R_t is the transition relation

Explanation:

Conditions (1)-(2) enforce the sequence of states (s_k, s_k+1, ..., s_j, ...) to be a valid execution path of the transition system over which the ltl formula can be evaluated.
Condition (3) forces ψ to hold in s_j.
Condition (4) forces ϕ to hold in any state s_i that lies along the path from s_k (included) up to s_j (excluded).

Since an implication with a false premise is always true, the logical implication inside condition (4) is trivially satisfied for any i that lies outside of the range [k, j). Whenever j is picked to be equal to k, as in your question, the range [k, j) = [k, k) is empty and any choice of i lies outside said interval. In this case, regardless of the fact M, s ⊨ ϕ holds (or not) for some s, condition (4) is trivially satisfied for any choice of i and it no longer imposes any constraint over the execution path (s_k, s_k+1, ..., s_j, ...). In other words, when j = k condition (4) no longer provides any meaningful contribution to the verification of property ϕ U ψ over the state s_k.

WEAK UNTIL

The difference among weak until, hereby denoted with ϕ W ψ, and strong until is that weak until is also satisfied by any execution path s.t. G (ϕ ∧ ¬ψ), whereas strong until compels F ψ.

EXAMPLE ANALYSIS

The property p0

[] ((state == Reverse) U (state != Reverse))

requires p1

((state == Reverse) U (state != Reverse))

to hold in each and every state of your system. I will break down p1 in two components for clarity, and define ϕ to be equal state == Reverse and ψ to be equal state != Reverse (note: ϕ <-> !ψ).

Let's assume, to simplify things, that your system is comprised by the following three states:

s_0: a regular state, which also happens to be the initial state
s_1: a reverse state
s_2: the final state

In order for p0 to hold, p1 must hold for each of these states.

in state s_0 the property ψ holds, therefore p1 holds too for j equal 0.
in state s_1 the property ψ is false. However, we have that ϕ holds in s_1 and ψ holds in s_2 which is its immediate, and only, successor. So property p1 holds in s_1.
in state s_2 the property ψ is true, so p1 is again trivially satisfied.