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

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

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.