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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 28 Jun 2022 18:37:40 +0200*References*: <9e859fd3-6d18-43f6-81b0-ed329f780047n@googlegroups.com> <2C070E7E-A900-4476-B102-808738D0A34A@gmail.com> <6d08a54c-e7eb-47ed-a8d2-5e551c4cac09n@googlegroups.com> <556DE16C-105F-46E9-B580-5BC5DD4C274D@gmail.com> <09eb6219-9a8b-4f35-ad5a-e522cf160e05n@googlegroups.com>

It seems to me that you can express this condition by writing SF_vars(TMRcvAborted /\ tmConfirmed' = RM) But I don't understand your specification well enough to know if this is a reasonable fairness condition, and why you really need this variant rather than WF/SF_vars(TMRcvAborted) which requires TMRcvAborted to occur eventually when it is enabled, eventually ensuring that tmConfirmed = RM. Given that no action appears to be in conflict with TMRcvAborted, there should be no difference between weak and strong fairness for this action. 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/05BAD015-F2FC-4FAD-939C-F470AF363410%40gmail.com. |

**Follow-Ups**:

**References**:**[tlaplus] Question about "Temporal formula is a tautology" in fairness***From:*钱晨

**Re: [tlaplus] Question about "Temporal formula is a tautology" in fairness***From:*Stephan Merz

**Re: [tlaplus] Question about "Temporal formula is a tautology" in fairness***From:*Stephan Merz

**Re: [tlaplus] Question about "Temporal formula is a tautology" in fairness***From:*钱晨

- Prev by Date:
**Re: [tlaplus] Question about "Temporal formula is a tautology" in fairness** - Next by Date:
**Re: [tlaplus] Question about "Temporal formula is a tautology" in fairness** - Previous by thread:
**Re: [tlaplus] Question about "Temporal formula is a tautology" in fairness** - Next by thread:
**Re: [tlaplus] Question about "Temporal formula is a tautology" in fairness** - Index(es):