Temporal property unexpectedly fails

[Rostislav Nikitin]

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.

[Stephan Merz]

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

--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAM5RVs8Lqg5XUc06Q3fJo0gBCyHBZ7-ZYnTvEVAkyjbzkg0FbQ%40mail.gmail.com.