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

[tlaplus] Re: problems debugging liveness errors.

Many thanks
       Initially I thought that, in order to establish strong fairness  you only  needed to restrict a step when there was a choice between two transitions of the same step.  That is when a step itself was nondeterministic. But I can see that even with deterministic steps  all you need is the exiting step to be some where in the loop then you need  to restrict the step.

       Strong Fairness in TLA+  is quite different from that in process algebras such as Fair Failure semantics. It is interesting that liveness conditions are so hard to verify in TLA+ whereas in process algebras they are, by default, what are normally specified and verified.

Finally I am getting the differences between process algebra and TLA+  

regards david

On Friday, 3 May 2019 06:03:42 UTC+12, Jay Parlar wrote:
One final comment: I'd be wary of the number of strongly fair labels you've placed in your spec. My understanding is that strong fairness is rarely used, as it's difficult to implement actual systems that satisfy it. It definitely has its place, but it's not common. Placing it on every process and label in your spec is most likely not the correct course of action.

I understand doing it given your initial assumption that "looping forever was prohibited by these strong fairness clauses", but as we've shown, your assumption was incorrect.

I just don't want you or your students to think that the right way to approach these specs is by marking everything as strongly fair.

Jay P.

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.