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

[recepient recepient <netsmaza@xxxxxxxxx>]

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?

Thanks,







SPECIFICATION Spec
\* PROPERTY Liveness

------------------------------ MODULE stuttering2 ------------------------
EXTENDS TLC, Integers
VARIABLES hour 
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.