An eventually rule passes on a trace that ends before the event, and the engineer reads the pass as progress. Or an antecedent that never fires passes every check, and the team counts the rule as proven. Both are passes that prove nothing, but they are different nothings with different fixes. This lesson's one job is to separate three words reviewers constantly hear confused: weak, strong, and vacuous.
Weak and strong describe what an obligation that never completes is worth. A strong sequence holds only if a match actually occurs. A weak sequence holds unless some finite prefix of the trace already rules every match out; a sequence that simply never completes is allowed. So an unbounded wait for a grant, with the grant never coming, fails the strong form and passes the weak one. That holds on a finite run that ends first and, just the same, on an infinite trace that loops without ever granting: no finite prefix of the loop refutes the weak form, because the grant could still arrive one cycle later. A request that is eventually granted passes both.
Three consequences follow. A weak unbounded eventuality can never fail, on any trace, finite or infinite: it is a rule that cannot be broken, which is why liveness is written with s_eventually or strong(...) and never with a bare unbounded delay. A strong one fails whenever the obligation is left open, on a run that ended too soon (which says something about the run, not the design) and on a lasso, a prefix followed by a loop that repeats for ever, which is the only counterexample to real liveness. And a bounded formal run sees only finite prefixes, so it cannot refute even the strong form as a statement about all futures: it can only report that nothing failed within its depth.
Strength is a property of the obligation, never of its trigger: putting strength on the antecedent is a category error that keeps reappearing in answer banks. Vacuity is a separate matter. A rule whose antecedent never fires passes whether it is weak or strong, in simulation and in proof, because there is no attempt to judge. The fix is not a different strength but a cover: reach the antecedent and show the rule was ever tried.
The script below evaluates the rule every request is followed, strictly later, by a grant. A trace is a prefix and, for an infinite trace, a loop that repeats for ever; a finite run has no loop. It checks the full table: four traces, each judged weak and strong, and asserts that the two differ in exactly the two rows where a request is left open, the finite run and the lasso. It also asserts that a rule whose trigger never fires passes both ways, that its antecedent cover is empty, and that a mutated interpreter with the two meanings swapped is caught:
# Rule under test: every request is followed, strictly later, by a grant.
# A trace is (prefix, loop). loop = None means a FINITE run that simply ends; otherwise the
# trace is prefix then loop repeated for ever (an infinite trace, the form a proof engine reasons about).
def later_grant(trace, t):
prefix, loop = trace
if any(g for _, g in prefix[t + 1:]):
return True
return bool(loop) and any(g for _, g in loop)
def open_obligation(trace):
"""True when some request never gets its grant on this trace."""
prefix, loop = trace
if any(req and not later_grant(trace, t) for t, (req, _) in enumerate(prefix)):
return True
return bool(loop) and any(r for r, _ in loop) and not any(g for _, g in loop)
def verdict(trace, strength):
# weak(R) is the safety closure of strong(R): it fails only if a FINITE prefix already rules every
# extension out. An open eventuality never does, whether the trace stops or loops for ever.
if not open_obligation(trace):
return "pass"
return "pass" if strength == "weak" else "fail"
R, G, I = (1, 0), (0, 1), (0, 0)
cases = {
"finite, no grant": ([R, I, I], None),
"finite, grant": ([R, I, G], None),
"lasso, no grant": ([R, I], [I, I]),
"lasso, grant": ([R, I], [I, G]),
}
want = {"finite, no grant": ("pass", "fail"), "finite, grant": ("pass", "pass"),
"lasso, no grant": ("pass", "fail"), "lasso, grant": ("pass", "pass")}
for name, tr in cases.items():
assert (verdict(tr, "weak"), verdict(tr, "strong")) == want[name], name
differ = [n for n, tr in cases.items() if verdict(tr, "weak") != verdict(tr, "strong")]
assert differ == ["finite, no grant", "lasso, no grant"] # an open eventuality is the only place they part
def covered(trace):
prefix, loop = trace
return any(r for r, _ in prefix + (loop or []))
vacuous = ([I, I], [I, G])
assert verdict(vacuous, "weak") == verdict(vacuous, "strong") == "pass" and not covered(vacuous)
assert all(covered(tr) for tr in cases.values())
def swapped(trace, strength):
return verdict(trace, "strong" if strength == "weak" else "weak")
assert any(swapped(tr, "weak") != verdict(tr, "weak") for tr in cases.values())
print("PASS: weak and strong part on every open obligation, finite or looping; vacuity needs a cover")The textbook forms stay as concept listings throughout this course, because an unbounded eventuality needs a liveness engine the open flow does not provide, and a runnable Boolean form cannot express liveness at all: a Boolean check on past values can only refuse a finite prefix, which is safety. The comments say which cycle each form refers to and what refutes it; the wrong forms after them are the ones answer banks keep printing:
// not-run: unbounded eventualities need a liveness engine
// strong, the grant arrives in the same cycle as the request or later:
// assert property (req |-> s_eventually gnt);
// strong, the grant arrives strictly later (the next cycle or after):
// assert property (req |-> strong(##[1:$] gnt));
// weak (the default for a sequence inside a property): same cycles as the strong form above, but
// a sequence that never completes is allowed, so no finite prefix refutes it
// assert property (req |-> ##[1:$] gnt);
// a trace with an open request, finite or a lasso that never grants: the two strong forms fail it,
// the weak form passes it. The weak unbounded form cannot fail on any trace.// bad-example: both of these look right and say the wrong thing
// assert property (s_eventually (req |-> gnt));
// satisfied as soon as ANY cycle has req low, so it says nothing about requests
// assert property (strong(req ##[1:$] gnt));
// a stand-alone strong sequence must match from every start: it fails whenever req is low
// the bounded substitute names the bound: req |-> ##[1:N] gnt, which is safety (next lesson)Strength sits on the liveness obligation, never on the antecedent: a strong wrapped around a trigger is rewritten or rejected.
Every unbounded eventually either names its engine or is replaced by a bounded window with a justified bound; a bare eventually with a bounded proof is a review failure.
Vacuity has its own evidence: an antecedent cover per implication-style rule, reached, not just written.
When an eventually rule passes suspiciously fast, ask which form it is. A weak unbounded form passes every trace, so its pass is empty by construction: rewrite it as a strong form, or as a bounded window. For the strong form ask what fails it: a lasso with an open request is the real counterexample, a finite run that ends early is an artefact of the run. Then ask whether the antecedent cover reaches: a rule whose trigger never fires is vacuous, whatever its strength. A rule that a finite prefix fails was safety all along and should say its bound.
Almost nothing: any finite prefix could extend with the event, and so could any loop, so the weak form cannot fail on that trace or on a lasso without the event. Only the strong form on a lasso, or a bound checked as safety, says something about progress.