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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 23 Nov 2022 21:00:15 +0100*References*: <CAE7Z=+5ZP00oiNr26TKr0+=uxsaGsGMUWRm10+mASAUHF3wSRQ@mail.gmail.com>

Hello, this is the definition of weak fairness. An equivalent definition is [](([]ENABLED <<A>>_v) => <> <<A>>_v) and you may check your understanding of temporal logic by proving that the two formulas are equivalent. In system specifications, fairness conditions are assumptions on the behavior of (the platform that runs) the system. They need to be validated in order to make sure that they correspond to the understanding that you have of the system, but they are not (and cannot be) proved because they are not universally true. Regards, Stephan On 23 Nov 2022, at 20:03, Huailin <huailin@xxxxxxxxx> wrote: -- 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/BEAFBF1F-DF15-4016-BAFE-A3505E719D93%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] About WF***From:*Huailin

**References**:**[tlaplus] About WF***From:*Huailin

- Prev by Date:
**[tlaplus] About WF** - Next by Date:
**Re: [tlaplus] About WF** - Previous by thread:
**[tlaplus] About WF** - Next by thread:
**Re: [tlaplus] About WF** - Index(es):