[tlaplus] Re: When TLC error trace send with stuttering - what does this mean?

[Jay Parlar <parlar@xxxxxxxxx>]

> Does the addition of liveness conditions change the State Graph to indicate where infinite stuttering might occur?

Can you clarify what you mean here? If by “liveness conditions”, you mean adding temporal property checks, then nothing should change in the state space simply by adding those checks. 

Stuttering is only checked for if you add a liveness property, because stuttering can only affect the “correct behaviour” of a system if a temporal property is part of the correct behaviour. 

-- 
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.