Every later lesson in this section leans on translations: an overlapped rule becomes a same-cycle comparison, a non-overlapped rule becomes a history comparison one cycle later. A translation with the offset wrong by one compiles, runs, and proves the wrong rule, often vacuously. This lesson's one job is the table the rest of the course relies on, plus a mechanical check that the table is right.
Translation is index arithmetic. A textbook attempt starts in cycle t; the Boolean check that means the same thing runs in cycle t plus the delay of the operator, and names the antecedent through history of exactly that depth. Get the depth right and the two forms flag the same cycles on every trace; get it wrong by one and they disagree on traces any solver will find.
Textbook form | Boolean history form | Cycle it checks |
|---|---|---|
a |-> b | fail when a && !b | Same cycle as the antecedent. |
a |=> b | fail when a_d1 && !b | One cycle after the antecedent. |
a ##1 b (chain) | match when a_d1 && b | Completion cycle of the chain. |
a ##2 b (chain) | match when a_d2 && b | Completion cycle of the chain. |
a[*2] ##1 b | match when the run counter, saturating at 2, was 2 last cycle, and b | Cycle b arrives, after at least two consecutive a. |
a ##[1:3] b (chain) | match when b && (a_d1 || a_d2 || a_d3) | Each cycle the window can complete. |
a |-> ##[1:3] b | fail when a_d3 && !(b_d2 || b_d1 || b) | Cycle t + 3, when the window closes. |
a throughout (b ##2 c) | match when a && a_d1 && a_d2 && b_d2 && c | Completion cycle, with a held across all three cycles. |
$rose(a) | a && !a_d1 | The edge cycle itself. |
$fell(a) | !a && a_d1 | The edge cycle itself. |
a until b | none in the open flow | Concept only: it needs an unbounded wait. |
A chain or sequence has no verdict of its own, so its Boolean form is a match: the cycle where the sequence completes. A rule built on an implication is a failure: the cycle where an attempt is judged and found wanting. Three things have no Boolean equivalent in the open flow and stay as concept listings throughout the course: an unbounded eventuality, a strong sequence over an infinite trace, and until. A throughout with a fixed window is expressible, as the row shows; without a window it belongs with the unbounded three. One convention applies to every history register here: before the first cycle every sample is 0, which is what a register cleared by reset holds. Edges at cycle 0 are measured against that value.
The script below is the check of the table. It contains two independent pieces. The textbook interpreter works from the trace itself: for each start cycle t it applies the textbook meaning of the operator and records the completion cycles. The Boolean machine never looks at the trace: it holds shift registers and a run counter, advances them one cycle at a time and evaluates the Boolean form of the row. The script compares the two on every trace of length 6 (length 5 for the three-signal row), then repeats the run with an off-by-one injected into each Boolean row and asserts that every injection is caught.
from itertools import product
def tb(row, s, n):
"""Textbook meaning: one attempt per start cycle t; returns the cycles where a rule is violated
(properties) or a sequence matches. Attempts whose window runs past the trace end are not judged."""
a, b, c = s["a"], s["b"], s["c"]
out = set()
for t in range(n):
if row == "a |-> b" and a[t] and not b[t]: out.add(t)
if row == "a |=> b" and t + 1 < n and a[t] and not b[t + 1]: out.add(t + 1)
if row == "a ##1 b" and t + 1 < n and a[t] and b[t + 1]: out.add(t + 1)
if row == "a ##2 b" and t + 2 < n and a[t] and b[t + 2]: out.add(t + 2)
if row == "a[*2] ##1 b" and t + 2 < n and a[t] and a[t + 1] and b[t + 2]: out.add(t + 2)
if row == "a ##[1:3] b":
out |= {t + k for k in (1, 2, 3) if t + k < n and a[t] and b[t + k]}
if row == "a |-> ##[1:3] b" and t + 3 < n and a[t] and not any(b[t + k] for k in (1, 2, 3)): out.add(t + 3)
if row == "a throughout (b ##2 c)" and t + 2 < n and a[t] and a[t + 1] and a[t + 2] and b[t] and c[t + 2]: out.add(t + 2)
if row == "$rose(a)" and a[t] and not (a[t - 1] if t else 0): out.add(t)
if row == "$fell(a)" and not a[t] and (a[t - 1] if t else 0): out.add(t)
return out
BOOL = { # x(sig, k): value of sig k cycles ago, read from a shift register; m = 1 injects an off-by-one
"a |-> b": lambda x, m: x("a", m) and not x("b", 0),
"a |=> b": lambda x, m: x("a", 1 + m) and not x("b", 0),
"a ##1 b": lambda x, m: x("a", 1 + m) and x("b", 0),
"a ##2 b": lambda x, m: x("a", 2 + m) and x("b", 0),
"a[*2] ##1 b": lambda x, m: x("run", 1 + m) >= 2 and x("b", 0),
"a ##[1:3] b": lambda x, m: x("b", 0) and (x("a", 1 + m) or x("a", 2 + m) or x("a", 3 + m)),
"a |-> ##[1:3] b": lambda x, m: x("a", 3 + m) and not (x("b", 2) or x("b", 1) or x("b", 0)),
"a throughout (b ##2 c)": lambda x, m: x("a", 0) and x("a", 1) and x("a", 2) and x("b", 2 + m) and x("c", 0),
"$rose(a)": lambda x, m: x("a", 0) and not x("a", 1 + m),
"$fell(a)": lambda x, m: not x("a", 0) and x("a", 1 + m),
}
def machine(row, s, n, m=0):
"""Boolean history form: registers only (shift registers plus a saturating run counter)."""
reg = {k: [0] * 6 for k in "abc"}
reg["run"] = [0] * 6
out = set()
for t in range(n):
for k in "abc":
reg[k] = [s[k][t]] + reg[k][:-1]
run_now = min(2, reg["run"][0] + 1) if s["a"][t] else 0
reg["run"] = [run_now] + reg["run"][:-1]
if BOOL[row](lambda sig, d: reg[sig][d], m): out.add(t)
return out
def all_traces(n, used):
zero = (0,) * n
pool = [list(product((0, 1), repeat=n)) if k in used else [zero] for k in "abc"]
for a, b, c in product(*pool):
yield {"a": a, "b": b, "c": c}
checked = 0
for row in BOOL:
n = 5 if "throughout" in row else 6
used = "a" if "(a)" in row else "abc" if "throughout" in row else "ab"
caught = 0
for s in all_traces(n, used):
want = tb(row, s, n)
assert machine(row, s, n) == want, row
caught += machine(row, s, n, m=1) != want
checked += 1
assert caught > 0, "the off-by-one went unnoticed: " + row
print("PASS: %d rows agree with the textbook meaning on %d traces; every off-by-one variant is caught" % (len(BOOL), checked))Every property comment says which cycle it checks: same cycle, next cycle, or completion cycle of a named window.
History depth equals the operator delay exactly: one for non-overlapped, two for a two-delay, an OR of three for a one-to-three window.
Anything unbounded is marked as concept with its runnable bounded partner beside it, never translated silently into a bounded form.
Rerun the checker whenever the table grows: add the new row as a pair of functions, extend the loop, and add its off-by-one as a variant the loop must catch. A translation the checker cannot catch a wrong variant of is a translation the proof cannot distinguish either, which means the two forms are the same rule and the row adds nothing. Remember what the checker does not cover: it compares forms of one rule, so it cannot tell you the rule itself is the one the specification asks for.
If both used the same indexing they could share a mistake and still agree. The interpreter encodes the textbook meaning (attempts and windows over the trace); the machine encodes what hardware can do (a few registers). Agreement between them on every trace is the evidence, and the injected off-by-one shows the comparison can disagree.