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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Fri, 22 Feb 2019 11:46:04 +0100*References*: <f42beda0-ad14-41c4-8c5d-df85ad6890ea@googlegroups.com> <f105fe97-c975-4673-af64-4353228e8f8f@googlegroups.com>

Hello David,
I believe your objection is that the fairness conditions are not of the form SF_vars(...) but of the form SF_ch(...) where ch is the variable that represents the data channel [1], and that such fairness conditions cannot be written in PlusCal using fairness on processes or individual labels. So now we are back to the earlier thread [2] on expressing fair choice in PlusCal. I believe that the discussion in that thread argued quite convincingly that the translation of such a construct would not be straightforward, and would (at least) introduce additional labeling rules. (In your proposed "hack", you assume that each branch is labeled.) I agree with the arguments provided in the earlier thread to the effect that it is preferable to identify the intended fairness condition using TLA+ than PlusCal in these cases. Best regards, Stephan [1] Alternatively, one could write SF_vars(dtCh /\ sndC' = Append(sndC, sndOut)).
-- 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. |

**Attachment:
AlternatingBit.tla**

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

**Attachment:
Transmission.tla**

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

**References**:**[tlaplus] add fairness properties to a specification with PlusCal INSTANCEs***From:*david streader

**[tlaplus] Re: add fairness properties to a specification with PlusCal INSTANCEs***From:*david streader

- Prev by Date:
**[tlaplus] Re: add fairness properties to a specification with PlusCal INSTANCEs** - Next by Date:
**[tlaplus] Fingerprint collision probability?** - Previous by thread:
**[tlaplus] Re: add fairness properties to a specification with PlusCal INSTANCEs** - Next by thread:
**[tlaplus] Re: add fairness properties to a specification with PlusCal INSTANCEs** - Index(es):