Dear group:
Around the 16:21-16:48 marks in the video 9a
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.