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

[tlaplus] Re: Seeking clarification of "continuously enabled" in weak fairness (video 9a)



WF_vars(A) is false for a behaviour that has an infinite tail where A is enabled but never taken (more precisely <A>_vars is never true); WF_vars(A) is true otherwise. Intuitively, WF_vars(A) means that A can not be enabled forever yet never happen. So yes, if A is not enabled forever (continuously), then WF_vars(A) can be true even if A never occurs.

-- Ron

On Monday, February 15, 2021 at 2:30:25 AM UTC bc.be...@xxxxxxxxx wrote:
going further ...

around 17:30, LL points out that WF_vars(A) can be made true by a state in which A is not enabled.

By that, I deduce (perhaps incorrectly), that a behavior with even an infinite number of finite, contiguous sub-sequences of A-enabled states will satisfy WF_vars(A) even if no A-step ever occurs.

Did I get that right?

On Sunday, February 14, 2021 at 6:20:32 PM UTC-8 Brian Beckman wrote:
Dear group:

Around the 16:21-16:48 marks in the video 9a

http://lamport.azurewebsites.net/video/video9a.html

LL gives the example of (what I see as) a contiguous [sic; as opposed to "continuous"] sequence of states s45 -> s46 -> ... -> s50, all enabled (green) for action A. quoting loosely, now, ~"Weak Fairness asserts that an A step must occur somewhere in that finite, contiguous sub-sequence of A-enabled states, after which, A need not be enabled"~ that is s51->s52->etc. could revert to red.

I take this to mean that any finite, contiguous sub-sequence of states containing at least two A-enabled states, say sA_{4242} -> sA_{4243}, is a candidate for weak fairness. WF will be true if sA_{4242}->sA_{4243} is an A-step. The sub-sequence of A-enabled states could be longer, even going on forever, but it could stop after even one A-step.

I've been skimming "Specifying Systems" and Hillel's book, "Practical TLA+" for examples of finite, contiguous sub-sequences of X-enabled states, for some particular action X -- the same X in all the X-enabled states. In all the examples I've seen, the sequences of X-enabled states start at one spot and go on forever.

So my question is: does (quoting verbatim now from the video) "if A ever remains continuously [sic; as opposed to "contiguously but possibly finitely often"] enabled then an A step must eventually occur"

does "continuously" mean that A, once enabled, must remain enabled forever for WF to pertain? (as in all the examples I've seen)

or does "continuously" also admit finite, contiguous sub-sequences as pertinent to WF? (as implied by the brief comment that "after which, A need not be enabled")

If "continuously" means the latter, then WF could pertain multiple times in a behavior, once on each finite, contiguous sub-sequence of A-enabled states. There could even be an infinite number of "WF-pertinent zones" (to coin a clumsy term) in a behavior.


--
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/e75bd60a-ccec-4bb2-8e8f-bcf5f9efc73en%40googlegroups.com.