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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 14 Jun 2021 08:37:49 +0200*References*: <f735e5b2-8c89-450b-bfd7-293e16193d79n@googlegroups.com> <13814DBE-4382-4CAD-A523-19D6BA7DD8DC@gmail.com> <ca59de39-ed3d-45e3-86bc-ac7ce3296665n@googlegroups.com>

Is correctReceive ever enabled in the counter-example? The await condition in receiveData clearly ensures the condition inputQueue # {} but what about the second conjunct? Also, comparing tmpTakenInput for equality to a set of ten messages looks suspicious, perhaps you meant to write "tmpTakenInput \notin ..."? Getting fairness conditions right is difficult, and I suggest you start by considering simpler algorithms. Stephan
--
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0952E3C9-CB54-4A02-956E-B369069A5170%40gmail.com. |

**References**:**[tlaplus] ripetitive incorrect send***From:*p.to...@xxxxxxxxxxxxxxxxx

**Re: [tlaplus] ripetitive incorrect send***From:*Stephan Merz

**Re: [tlaplus] ripetitive incorrect send***From:*p.to...@xxxxxxxxxxxxxxxxx

- Prev by Date:
**Re: [tlaplus] ripetitive incorrect send** - Next by Date:
**[tlaplus] Translational Symmetry for Model Checking** - Previous by thread:
**Re: [tlaplus] ripetitive incorrect send** - Next by thread:
**[tlaplus] Translational Symmetry for Model Checking** - Index(es):