Re: [tlaplus] Digest for tlaplus@googlegroups.com - 2 updates in 1 topic

[Rostislav Nikitin]

Hello Stephan.

Thank for your answer.

Yep, you are absolutely right.

Yesterday I found this article: https://www.hillelwayne.com/post/fairness/

And after reading it I realized that I had a wrong undestanding how TLA+/TLC is working.

So yep, I need to add fair conditions like WF_vars(Next). And it is work for me.

Thank you again.

Bye.
Best regards, Rostislav Nikitin.

On Sun, Oct 26, 2025, 14:49 <tla...@googlegroups.com> wrote:

tla...@googlegroups.com

Google Groups

Topic digest
View all topics

• Temporal property unexpectedly fails - 2 Updates

Temporal property unexpectedly fails

Rostislav Nikitin <rostisla...@gmail.com>: Oct 25 05:54PM +0300 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 IntegersVARIABLES 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]_varsTemporalProperty == []<><<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.

Stephan Merz <stepha...@gmail.com>: Oct 25 05:16PM +0200 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.   Hope this helps, Stephan

Back to top

You received this digest because you're subscribed to updates for this group. You can change your settings on the group membership page. To unsubscribe from this group and stop receiving emails from it send an email to tlaplus+u...@googlegroups.com.