Re: [tlaplus] Temporal property unexpectedly fails

A TLA+ specification Init /\ [][Next]_vars allows for behaviors that end in infinite stuttering after finitely many transitions, and this is exactly what the counter-example shows. In fact, a minimal counter-example would be to not perform any transitions at all but stutter at the initial state. However, TLC does not guarantee minimal counter-examples for liveness properties.

In order to avoid stuttering when some steps are possible, you will have to add a fairness condition to your specification. The most basic fairness condition is WF_vars(Next), which ensures progress: some transition will eventually happen as long as the system is not deadlocked. For your simple specification, this should ensure that the property holds.

Stephan

On 25 Oct 2025, at 16:54, Rostislav Nikitin <rostislav.nikitin@xxxxxxxxx> wrote:

Hello everyone.
What do you think, is a violation of the temporal property a normal behavior or not?
Because from my point of view, it shouldn't be any violation.

So this is a very simple example:

EXTENDS Integers
VARIABLES step, state

vars == <<step, state>>

TypeOK ==
state \in {"created", "inProgress", "completed"}

Init ==
/\ step = 1
/\ state = "created"

InProgress ==
/\ state = "created"
/\ step' = step + 1
/\ state' = "inProgress"

Completed ==
/\ state = "inProgress"
/\ step' = step + 1
/\ state' = "completed"

Next ==
\/ InProgress
\/ Completed

Spec == Init /\ [][Next]_vars

TemporalProperty ==
[]<><<state = "completed">>_vars

I am trying to check the temporal property "TemporalProperty" and it fails on the last step:
/\ state = "completed"
/\ step = 3
Stuttering State(num = 4)

If we look at the temporal property _expression_:
[]<><<state = "completed">>_vars
It says: "should always eventually happen, state = "completed" or vars should be changed".
So on the last step (and all the next steps) state = "completed" and this satisfies the temporal property.

Why does the stuttering error appear?

Thanks for your attention.
--
Bye.
Best regards, Rostislav Nikitin.

--
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 visit https://groups.google.com/d/msgid/tlaplus/CAM5RVs8Lqg5XUc06Q3fJo0gBCyHBZ7-ZYnTvEVAkyjbzkg0FbQ%40mail.gmail.com.