Re: [tlaplus] When TLC error trace send with stuttering

In ADT and process algebras CSP and CCS nothing stutters by default you have to add some thing to enable stuttering.

Note that stuttering is in fact very explicit in the next-state relations used in TLA+ specifications: [Next]_v is shorthand for "Next \/ v'=v", and this disjunct is responsible for stuttering. It allows any step to happen that leaves the _expression_ v unchanged, and a little thought will convince you that v'=v is bound to hold if all the variables that appear in v (and perhaps more) remain unchanged.

Jay writes:

(I think it's an error to restrict WF to a subset of variables, but someone more knowledgable can correct me.)

It is syntactically legal to write WF_e(A) for any _expression_ e (possibly different from the tuple of all variables) and any action A (even one that does not occur as a disjunct of the next-state relation), and sometimes it makes sense to write such fairness conditions. The problem with these is that they may result in specifications that are not "machine closed". Leslie recently pointed this out in his answer to another thread [1]. Unless you know exactly what you are doing, it is better to restrict yourself to fairness conditions WF_v(A) where v is the same subscript as the one used in [Next]_v, and A is a disjunct of Next.

Regards,

Stephan

[1] https://groups.google.com/forum/#!topic/tlaplus/1FvqnGFhxTE

On 1 Apr 2019, at 04:41, david streader <davidistreader@xxxxxxxxx> wrote:

Thanks Jay
My use of terminology alas is from the refinement of Abstract data types, ADT, and process algebra so I struggle with TLA terminology but I have read the texts in quite some detail.
So a step is disabled when its guard (or precondition) is false and although we don't say that it is the particular step that stutters it is when a guard evaluates to false that stuttering occurs.
With no fairness condition  Spec == Init /\ [][Inc \/ Reset]_x then the state machine we considered
Init == x=0
Inc == x<5 /\ x'=x+1
Reset == x=5 /\ x'=0
could stutter immediately and falsify any liveness condition. But the error trace displayed depends on the temporal condition, it may first completes several steps before stuttering even though it could stutter immediately and falsify the condition. I misinterpreted the error trace as implying that this was the first point that stuttering could occur where as I gather that this is the first point where stuttering is checked.

TLA+ allows fairness to be defined for very specific situations but because of my background in process algebra and abstract data types all I want is to have strong fairness every where. In ADT and process algebras CSP and CCS nothing stutters by default you have to add some thing to enable stuttering.

I gather  /\ WF_vars(Next) is will stop all stuttering but not sure what the effect of restricting the vars to a subset of the variables is. Is /\ SF_vars(Next) thought enforce strong fairness throughout the state machine?
Put another way: would  SF_vars(Next)  imply any other fairness condition?
It certainly is not having the effect I imagined but this may be caused by the translation from PlusCal to TLA+

regards david

--
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.

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