Re: [tlaplus] Weak fairness until a majority

[Jack Vanlightly <jack.vanlightly@xxxxxxxxx>]

Great, I get it, thanks to you all!

On Thursday, December 8, 2022 at 6:29:08 PM UTC+1 Markus Alexander Kuppe wrote:

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.va...@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/aa95cb7a-deb3-4fe3-94ef-e758c8b90cfan%40googlegroups.com.