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

[tlaplus] Re: problems debugging liveness errors.

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.