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

Re: [tlaplus] Weak fairness until a majority

From: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>
Date: Thu, 8 Dec 2022 09:28:51 -0800
References: <b32e95fb-e3db-4425-84d7-c0392ead61bcn@googlegroups.com> <4878083E-8EB0-4BA6-9A9E-2B9E84FBC6A0@gmail.com> <CAJ-b8sxdpcYt-NWcU+ZJ6i2rsV_Jkv46wb9+9R8hf_FPUaVgBA@mail.gmail.com> <95f9d555-b351-4613-a549-46e2e2cd50c8n@googlegroups.com>

Yes, just recall  WF_v(A) <=> <>[](ENABLED <<A>>_v) => []<>(<<A>>_v)  .  Your condition or A in general rather may be any action-level formula.  For a concrete example, see https://github.com/lemmy/BlockingQueue/blob/14a1baed2dd80ce83f32687c67749b39320ea121/BlockingQueue.tla#L136-L143.

Markus

> On Dec 8, 2022, at 9:21 AM, Jack Vanlightly <jack.vanlightly@xxxxxxxxx> wrote:
> 
> So if I want to express weak fairness of an action with some conditions, I simply write WF_vars(conditions /\ MyAction)?

-- 
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/F232739E-B9C1-4066-AD1E-B4CE65582E93%40lemmster.de.

Follow-Ups:
- Re: [tlaplus] Weak fairness until a majority
  - From: Jack Vanlightly

References:
- [tlaplus] Weak fairness until a majority
  - From: Jack Vanlightly
- Re: [tlaplus] Weak fairness until a majority
  - From: Stephan Merz
- Re: [tlaplus] Weak fairness until a majority
  - From: Hillel Wayne
- Re: [tlaplus] Weak fairness until a majority
  - From: Jack Vanlightly

Prev by Date: Re: [tlaplus] Weak fairness until a majority
Next by Date: Re: [tlaplus] Weak fairness until a majority
Previous by thread: Re: [tlaplus] Weak fairness until a majority
Next by thread: Re: [tlaplus] Weak fairness until a majority
Index(es):
- Date
- Thread