[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Why does checking temporal properties appear to influence stuttering?

Run the hour clock example (see below) with liveness enabled in the .cfg file and there will be an error with the resulting .dot graphs (if produced) to match with stuttering arrows.

Comment out the liveness check and all the stuttering -and- error go away. 

Why? Sure, I understand why the error goes away if Liveness definition isn't checked; But isn't stuttering on by default because unless otherwise told fair it's unfair? Shouldn't the diagrams continue to show that here?


\* PROPERTY Liveness

------------------------------ MODULE stuttering2 ------------------------
Init == hour = 12
Next == IF hour = 23
THEN hour' = 0 \* hour' is "next value of hour"
ELSE hour' = hour + 1

\* Our system starts at Init
\* And evolves according to Next
Spec == Init /\ [][Next]_hour

Liveness == <>(hour = 15)

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 on the web visit https://groups.google.com/d/msgid/tlaplus/170b2b60-a3d1-44e3-965a-8bd21be6a6b3n%40googlegroups.com.