vj-sim 0.3.0

//! T11 (`docs/superpowers/plans/2026-10-03-sva.md`): a reference interpreter
//! for a built [`Automaton`] over a CONCRETE trace -- the oracle the sequence
//! operator tests check against wherever a pure word language cannot express
//! the semantics (`first_match`, which selects matches by END TICK across a
//! whole evaluation attempt), and the one place the
//! [`Transition::FirstMatchBegin`]/[`Transition::FirstMatchEnd`] contract is
//! executable. The runtime engine (`vj-runtime::sva_engine`, a later task)
//! is a separate, incremental implementation of the same contract; this one is
//! a plain tick-ordered search that favors being obviously right over being
//! fast, and is never on a simulation path.
//!
//! One call is one EVALUATION ATTEMPT (16.12, 16.9.3): the sequence starts at
//! tick `start`, `leaf(id, tick)` says whether Boolean leaf `id` holds on
//! `tick`, and the result is every tick a match ends on. Ticks run `0..len`;
//! a path that would leave that window is dropped (a sequence cannot match on
//! a tick the trace never reached).
use std::collections::{BTreeMap, BTreeSet, HashMap};
use std::fmt;

use super::ir::{
    Automaton, CallArg, CallId, ClockId, EndMethod, EndPoint, FirstMatchId, LeafId, LocalVarId,
    ThreadStateId, Transition,
};
use super::wide;

/// What one attempt of an automaton over a trace produced.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Attempt {
    /// The automaton's EMPTY match (16.9.2.1), copied through: it spans no
    /// tick, so it has no end tick to put in `ends`.
    pub admits_empty: bool,
    /// Every tick a NONEMPTY match of the sequence ends on.
    pub ends: BTreeSet<u32>,
}

/// One thread's local-variable frame (T13): slot `i` is the value of
/// [`LocalVarId`]`(i)`, `None` while the variable is unassigned (16.10).
pub type Frame = Vec<Option<i64>>;

/// The matches of one sequence evaluation, `(end tick, frame)`. Almost every
/// evaluation of a bounded or single-letter antecedent has at most one, so the
/// first lives inline: no heap allocation per attempt tick.
pub type Matches = smallvec::SmallVec<[(u32, Frame); 1]>;

/// What one attempt of an automaton produced when its local-variable frames
/// are tracked (see [`attempt_with_locals`]).
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct LocalAttempt {
    /// The automaton's empty match, copied through as in [`Attempt`].
    pub admits_empty: bool,
    /// Every nonempty match as `(end tick, the matching thread's frame)`: one
    /// entry per distinct pair, since several threads may match on the same
    /// tick with different valuations (16.10 rule (c)).
    pub matches: BTreeSet<(u32, Frame)>,
}

impl LocalAttempt {
    /// The end ticks alone, the shape [`Attempt::ends`] has.
    pub fn ends(&self) -> BTreeSet<u32> {
        self.matches.iter().map(|(t, _)| *t).collect()
    }
}

/// One subroutine call a thread scheduled at a match item (16.11, T14): the
/// tick of the end point it fired on, which call site, and each actual
/// argument's value (`None` for a by-reference argument, which has no value of
/// its own: it names the actual).
#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
pub struct CallEvent {
    pub tick: u32,
    pub call: CallId,
    pub args: Vec<Option<i64>>,
}

/// What one attempt produced when both local-variable frames and subroutine
/// calls are tracked (see [`attempt_with_calls`]).
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct CallAttempt {
    /// The matches, as in [`LocalAttempt`].
    pub attempt: LocalAttempt,
    /// Every distinct call a thread scheduled, whether or not that thread
    /// later matched: a match item fires at every end point of the sequence it
    /// is attached to (16.11), even when a longer sequence it is part of then
    /// fails.
    pub calls: BTreeSet<CallEvent>,
}

/// An automaton shape this interpreter refuses to run, never a guess.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum TraceError {
    /// An edge kind with no meaning outside the full engine (abort edges
    /// belong to T20 and later; the local-variable edges are only interpreted
    /// by [`attempt_with_locals`], which has a frame to run them on).
    UnsupportedEdge(&'static str),
    /// A leaf read local variable `var` while it was unassigned (16.10): the
    /// builder rejects every read it can prove unassigned, so this is a
    /// malformed automaton or an evaluator reading a slot it was not given.
    UnassignedRead(LocalVarId),
    /// A [`Transition::FirstMatchEnd`] reached by a thread that never took the
    /// group's [`Transition::FirstMatchBegin`]: a malformed automaton.
    EndWithoutBegin(FirstMatchId),
    /// A [`Transition::FirstMatchBegin`] reached while the group is already
    /// open on the same thread: a malformed automaton (a region cannot
    /// contain itself).
    BeginWhileOpen(FirstMatchId),
    /// A `.matched` end point run without a clock model: its status depends on
    /// the two clocks' tick times, which only [`attempt_with_clocks`] has.
    MatchedWithoutClocks,
    /// A `.matched` end point inside an instance that is itself being run in
    /// another clock's tick space: the model has one destination and one source
    /// clock, so a third is refused rather than guessed.
    NestedMatched,
    /// The clock model's tick times are not strictly increasing.
    BadClocks,
    /// A [`Timeline`]'s tick list is not strictly increasing, or names a step at
    /// or past the trace's real length.
    BadTimeline,
    /// [`crate::sva::property::Evaluator::root_sequence_matches`] on a property
    /// whose root is not a bare sequence (a `cover sequence` always has one).
    NotASequence,
}

impl fmt::Display for TraceError {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            TraceError::NotASequence => write!(
                f,
                "sva trace interpreter: the matches of a property whose root is not a sequence \
                 were asked for"
            ),
            TraceError::BadTimeline => write!(
                f,
                "sva trace interpreter: a timeline's tick lists must be strictly increasing and \
                 inside the trace"
            ),
            TraceError::MatchedWithoutClocks => write!(
                f,
                "sva trace interpreter: a `.matched` end point needs a clock model \
                 (attempt_with_clocks)"
            ),
            TraceError::NestedMatched => write!(
                f,
                "sva trace interpreter: a `.matched` inside an instance run on another clock is \
                 not modelled"
            ),
            TraceError::BadClocks => write!(
                f,
                "sva trace interpreter: the clock model's tick times must be strictly increasing"
            ),
            TraceError::UnsupportedEdge(kind) => {
                write!(f, "sva trace interpreter: {kind} edges are not interpreted")
            }
            TraceError::EndWithoutBegin(g) => write!(
                f,
                "sva trace interpreter: FirstMatchEnd({}) reached without its FirstMatchBegin",
                g.0
            ),
            TraceError::BeginWhileOpen(g) => write!(
                f,
                "sva trace interpreter: FirstMatchBegin({}) reached while the group is open",
                g.0
            ),
            TraceError::UnassignedRead(v) => write!(
                f,
                "sva trace interpreter: read of unassigned local variable {}",
                v.0
            ),
        }
    }
}

impl std::error::Error for TraceError {}

/// The value of local variable `var` in `frame`, or
/// [`TraceError::UnassignedRead`] while it is unassigned. The accessor a
/// locals-aware leaf evaluator reads a variable through.
pub fn read_local(frame: &[Option<i64>], var: LocalVarId) -> Result<i64, TraceError> {
    frame
        .get(var.0 as usize)
        .copied()
        .flatten()
        .ok_or(TraceError::UnassignedRead(var))
}

/// One thread: `(tick, state, open first_match regions as (group, begin
/// tick), sorted by group, local-variable frame)`. Tick first so the work set
/// pops in tick order.
///
/// `ClockId` is the thread's CURRENT clock (multiclock sequences, 16.13): it moves
/// only along a [`Transition::ClockSync`], and a [`Transition::Delay`] counts
/// ticks of it.
type Config = (u32, u32, ClockId, Vec<(FirstMatchId, u32)>, Frame);

/// The evaluator both entry points feed [`run`]: a leaf's value at a tick
/// given the thread's frame.
type Eval<'a> = &'a dyn Fn(LeafId, u32, &[Option<i64>]) -> Result<i64, TraceError>;

/// Runs one attempt: see the module doc comment. A leaf here is a pure
/// Boolean, so an automaton with local-variable edges is refused (see
/// [`attempt_with_locals`]).
///
/// Configurations are processed strictly in tick order (a `BTreeSet` popped
/// from the front), so every `FirstMatchEnd` at tick `t` is seen before any at
/// a later tick -- exactly the order the engine's lock-step stepping gives it,
/// and the property the first-match table's "record the first end tick seen"
/// rule rests on.
pub fn attempt(
    au: &Automaton,
    start: u32,
    len: u32,
    leaf: &dyn Fn(LeafId, u32) -> bool,
) -> Result<Attempt, TraceError> {
    let matches = run(
        au,
        start,
        len,
        &|id, tick, _| Ok(i64::from(leaf(id, tick))),
        false,
    )?;
    Ok(Attempt {
        admits_empty: au.admits_empty,
        ends: matches.0.into_iter().map(|(t, _)| t).collect(),
    })
}

/// [`attempt`] with the local-variable frame (T13): every thread carries a
/// [`Frame`] that starts all-unassigned, a [`Transition::LocalVarWrite`]
/// stores the cast value of its `value` leaf, a [`Transition::LocalVarCopy`]
/// copies (casting, or propagating "unassigned"), and a fork copies the frame.
///
/// `eval(leaf, tick, frame)` is the VALUE of a leaf at a tick given the
/// thread's frame: a guard holds when it is nonzero and a write stores it. An
/// evaluator reads a local variable through [`read_local`], so a read of an
/// unassigned variable fails the whole attempt with
/// [`TraceError::UnassignedRead`] instead of guessing a value.
pub fn attempt_with_locals(
    au: &Automaton,
    start: u32,
    len: u32,
    eval: Eval<'_>,
) -> Result<LocalAttempt, TraceError> {
    Ok(LocalAttempt {
        admits_empty: au.admits_empty,
        matches: run(au, start, len, eval, true)?.0,
    })
}

/// [`attempt_with_locals`] that also reports the subroutine calls (16.11) the
/// attempt scheduled. A [`Transition::SubroutineCall`] is a same-tick,
/// unguarded pass-through whose only effect is its [`CallEvent`], recorded the
/// moment a thread takes the edge: a call is not conditional on the sequence
/// ultimately matching.
pub fn attempt_with_calls(
    au: &Automaton,
    start: u32,
    len: u32,
    eval: Eval<'_>,
) -> Result<CallAttempt, TraceError> {
    let (matches, calls) = run(au, start, len, eval, true)?;
    Ok(CallAttempt {
        attempt: LocalAttempt {
            admits_empty: au.admits_empty,
            matches,
        },
        calls,
    })
}

/// [`attempt_with_calls`] over two clock domains (16.13.5, 16.13.6): the trace is
/// `clocks.dest.len()` ticks of the clock the automaton runs on, and a
/// `.matched` end point inside it is evaluated against ticks of the clock of
/// the instance it is applied to (`clocks.source`). `eval(leaf, tick, frame)` is
/// called with a tick of the leaf's OWN clock -- source ticks for the leaves
/// of an instance a `.matched` is applied to, destination ticks for the rest --
/// and it is the evaluator that knows which leaves are which.
///
/// Only the calls of instances whose end point some thread actually tested are
/// reported.
pub fn attempt_with_clocks(
    au: &Automaton,
    start: u32,
    clocks: &TraceClocks,
    eval: Eval<'_>,
) -> Result<CallAttempt, TraceError> {
    let strictly_increasing = |v: &[u64]| v.windows(2).all(|w| w[0] < w[1]);
    if !strictly_increasing(&clocks.dest) || !strictly_increasing(&clocks.source) {
        return Err(TraceError::BadClocks);
    }
    let mut runner = Runner {
        eval,
        locals: true,
        len: clocks.dest.len() as u32,
        clocks: Some(clocks),
        timeline: None,
        status: HashMap::new(),
        calls: BTreeSet::new(),
        word: None,
    };
    let matches = runner.attempt(au, start, Space::Dest)?;
    Ok(CallAttempt {
        attempt: LocalAttempt {
            admits_empty: au.admits_empty,
            matches,
        },
        calls: runner.calls,
    })
}

/// A finite trace completed with a constant tail, the infinite words Annex F's
/// satisfaction relations are defined over (F.5.3.2): `w` followed by `⊤^ω` is
/// the WEAK verdict word (nothing has failed yet), `w` followed by `⊥^ω` the
/// STRONG one (everything still owed has failed). A letter `⊤` satisfies every
/// Boolean expression, a letter `⊥` none -- not even `1'b1` (F.5.3).
///
/// Ticks `0..real` are the trace's real samples (a leaf is evaluated there);
/// then come the explicit `mid` letters (`true` is `⊤`), then `tail_top`
/// forever. `mid` exists because a `⊥`-tailed word cut at a later tick and
/// completed with `⊤` (`w^{0,i-1}⊤^ω`, accept_on/weak) has a run of `⊥`
/// letters before its `⊤` tail.
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct TailWord {
    pub real: u32,
    pub mid: Vec<bool>,
    pub tail_top: bool,
}

impl TailWord {
    /// `w⊤^ω` over `real` real samples: the weak verdict word.
    pub fn weak(real: u32) -> Self {
        TailWord {
            real,
            mid: Vec::new(),
            tail_top: true,
        }
    }

    /// `w⊥^ω` over `real` real samples: the strong verdict word.
    pub fn strong(real: u32) -> Self {
        TailWord {
            real,
            mid: Vec::new(),
            tail_top: false,
        }
    }

    /// The first tick whose letter is the constant tail: every later tick looks
    /// the same, so a property cannot tell tick `extent()` from any tick after.
    pub fn extent(&self) -> u32 {
        self.real + self.mid.len() as u32
    }

    /// `Some(true)` for a `⊤` letter, `Some(false)` for `⊥`, `None` for a real
    /// sample at `tick`.
    pub fn letter(&self, tick: u32) -> Option<bool> {
        if tick < self.real {
            None
        } else {
            Some(
                self.mid
                    .get((tick - self.real) as usize)
                    .copied()
                    .unwrap_or(self.tail_top),
            )
        }
    }

    /// The dual word `w̄` (F.5.3.1: `w ⊨ not P` iff `w̄ ⊭ P`): every `⊤` letter
    /// becomes `⊥` and vice versa. The real samples are untouched.
    pub fn flip(&self) -> Self {
        TailWord {
            real: self.real,
            mid: self.mid.iter().map(|t| !t).collect(),
            tail_top: !self.tail_top,
        }
    }

    /// `w^{0,n-1}⊤^ω`: the first `n` letters, then `⊤` forever (the word
    /// `weak(R)` and `accept_on` complete a prefix with, F.5.3.1).
    pub fn cut_then_top(&self, n: u32) -> Self {
        if n <= self.real {
            return TailWord::weak(n);
        }
        let keep = (n - self.real) as usize;
        let mid = (0..keep)
            .map(|i| self.mid.get(i).copied().unwrap_or(self.tail_top))
            .collect();
        let mut w = TailWord {
            real: self.real,
            mid,
            tail_top: true,
        };
        // Trailing `⊤` letters are the tail already: one canonical spelling.
        while w.mid.last() == Some(&true) {
            w.mid.pop();
        }
        w
    }
}

/// The instants each clock of a multiclock assertion ticks at (16.13), over ONE
/// shared axis of positions (the simulation's time steps, or the trace's rows).
/// Position `p` is a tick of clock `c` when `p` is in `c`'s list.
///
/// Positions `0..real` are the trace's real steps. From `real` on, a word is the
/// constant `⊤`/`⊥` tail of [`TailWord`], which is a letter at EVERY position, so
/// every position past `real` is a tick of every clock: the tail neither adds nor
/// removes obligations clock by clock, it simply continues the verdict word. A
/// clock with no list at all ticks at every position (the single-clock case, where
/// a timeline is not needed).
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Timeline {
    real: u32,
    ticks: Vec<Vec<u32>>,
}

impl Timeline {
    /// `ticks[c]` is the sorted tick list of `ClockId(c)`; every entry must be
    /// below `real`.
    pub fn new(real: u32, ticks: Vec<Vec<u32>>) -> Result<Self, TraceError> {
        let ok = ticks
            .iter()
            .all(|l| l.windows(2).all(|w| w[0] < w[1]) && l.iter().all(|&t| t < real));
        if ok {
            Ok(Timeline { real, ticks })
        } else {
            Err(TraceError::BadTimeline)
        }
    }

    /// One tick list per row of `rows`: step `t` is a tick of clock `c` when
    /// `rows[c][t]`. The timeline is as long as the longest row.
    pub fn from_rows(rows: &[&[bool]]) -> Self {
        let real = rows.iter().map(|r| r.len() as u32).max().unwrap_or(0);
        let ticks = rows
            .iter()
            .map(|r| {
                r.iter()
                    .enumerate()
                    .filter(|&(_, &b)| b)
                    .map(|(t, _)| t as u32)
                    .collect()
            })
            .collect();
        Timeline { real, ticks }
    }

    /// The number of real steps.
    pub fn real(&self) -> u32 {
        self.real
    }

    /// The first `n` real steps: the timeline of a word cut to `n` letters, whose
    /// later positions are the constant tail (a tick of every clock). A cut
    /// longer than the trace is the trace.
    pub fn truncated(&self, n: u32) -> Timeline {
        let real = n.min(self.real);
        Timeline {
            real,
            ticks: self
                .ticks
                .iter()
                .map(|l| l.iter().copied().take_while(|&t| t < real).collect())
                .collect(),
        }
    }

    fn list(&self, c: ClockId) -> Option<&[u32]> {
        self.ticks.get(c.0 as usize).map(Vec::as_slice)
    }

    /// Is `p` a tick of `c`?
    pub fn is_tick(&self, c: ClockId, p: u32) -> bool {
        match self.list(c) {
            _ if p >= self.real => true,
            None => true,
            Some(l) => l.binary_search(&p).is_ok(),
        }
    }

    /// The first tick of `c` at or after `p` (`p` itself when it is one).
    pub fn next_tick(&self, c: ClockId, p: u32) -> u32 {
        match self.list(c) {
            _ if p >= self.real => p,
            None => p,
            Some(l) => l
                .get(l.partition_point(|&t| t < p))
                .copied()
                .unwrap_or(self.real),
        }
    }

    /// The `k`-th tick of `c` strictly after `p` (`k == 0` is `p` itself: the
    /// caller is already standing on a tick). `##1` is `k == 1`: "the nearest
    /// strictly subsequent tick" (16.13.1).
    pub fn kth_after(&self, c: ClockId, p: u32, k: u32) -> u32 {
        if k == 0 {
            return p;
        }
        match self.list(c) {
            _ if p >= self.real => p + k,
            None => p + k,
            Some(l) => {
                let at_or_before = l.partition_point(|&t| t <= p);
                let j = at_or_before + k as usize - 1;
                match l.get(j) {
                    Some(&t) => t,
                    None => self.real + (j - l.len()) as u32,
                }
            }
        }
    }
}

/// One evaluation attempt of `au` from `entry` with initial frame `frame0`,
/// started at tick `start`, over the tail-completed `word` (see [`TailWord`]).
/// Ticks `0..horizon` are searched; `horizon` must reach as far as any match can
/// matter (a property evaluator derives it from the automaton, see
/// `property::horizon`). A leaf on a `⊤`/`⊥` letter is that letter: guards hold
/// on `⊤` only, a value read there is `0`, and no subroutine call is scheduled.
///
/// Every match is `(end tick, frame)`, as in [`LocalAttempt`]; the empty match
/// is the caller's to track (it is a flag of the automaton, not of a path).
pub fn attempt_word(
    au: &Automaton,
    entry: ThreadStateId,
    frame0: &[Option<i64>],
    start: u32,
    word: &TailWord,
    horizon: u32,
    eval: Eval<'_>,
) -> Result<BTreeSet<(u32, Frame)>, TraceError> {
    attempt_word_in(
        au,
        entry,
        frame0,
        start,
        word,
        horizon,
        eval,
        None,
        au.entry_clock,
    )
}

/// [`attempt_word`] over a multiclock [`Timeline`] (`None`: every position is a
/// tick of every clock). The thread starts in clock `dom` and `start` is moved to
/// the first tick of `dom` at or after it. A `.matched` end point is refused
/// here exactly as in [`attempt_word`]: its two-space clock model is
/// [`attempt_with_clocks`]'s.
#[allow(clippy::too_many_arguments)]
pub fn attempt_word_in(
    au: &Automaton,
    entry: ThreadStateId,
    frame0: &[Option<i64>],
    start: u32,
    word: &TailWord,
    horizon: u32,
    eval: Eval<'_>,
    timeline: Option<&Timeline>,
    dom: ClockId,
) -> Result<BTreeSet<(u32, Frame)>, TraceError> {
    attempt_word_calls(au, entry, frame0, start, word, horizon, eval, timeline, dom)
        .map(|(matches, _)| matches)
}

/// [`attempt_word_in`] that also returns every subroutine call a thread
/// scheduled (16.11) on a REAL tick of `word`: a call reached on a `⊤`/`⊥`
/// letter is not a call of the simulation, as no sample was taken there. A call
/// is listed whether or not the thread that scheduled it later matched.
#[allow(clippy::too_many_arguments)]
pub fn attempt_word_calls(
    au: &Automaton,
    entry: ThreadStateId,
    frame0: &[Option<i64>],
    start: u32,
    word: &TailWord,
    horizon: u32,
    eval: Eval<'_>,
    timeline: Option<&Timeline>,
    dom: ClockId,
) -> Result<RunResult, TraceError> {
    let mut runner = Runner {
        eval,
        locals: true,
        len: horizon,
        clocks: None,
        timeline,
        status: HashMap::new(),
        calls: BTreeSet::new(),
        word: Some(word),
    };
    let matches = runner.attempt_from(au, entry, frame0.to_vec(), start, dom, Space::Dest)?;
    Ok((matches, runner.calls))
}

/// What [`run`] finds: every `(end tick, frame)` a match ends with, and every
/// distinct call a thread scheduled.
pub type RunResult = (BTreeSet<(u32, Frame)>, BTreeSet<CallEvent>);

/// The shared search behind [`attempt`], [`attempt_with_locals`] and
/// [`attempt_with_calls`]. `locals` says whether the local-variable,
/// subroutine-call and end-point edges are interpreted or refused.
fn run(
    au: &Automaton,
    start: u32,
    len: u32,
    eval: Eval<'_>,
    locals: bool,
) -> Result<RunResult, TraceError> {
    let mut runner = Runner {
        eval,
        locals,
        len,
        clocks: None,
        timeline: None,
        status: HashMap::new(),
        calls: BTreeSet::new(),
        word: None,
    };
    let matches = runner.attempt(au, start, Space::Dest)?;
    Ok((matches, runner.calls))
}

/// The tick-time model [`attempt_with_clocks`] runs a `.matched` end point
/// (16.13.5) under: the simulation time of every tick of the clock of the
/// automaton being run (`dest`, the clock of the context that tests the method)
/// and of the clock of the instance the method is applied to (`source`).
/// Both are strictly increasing.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct TraceClocks {
    pub dest: Vec<u64>,
    pub source: Vec<u64>,
}

/// Which clock's ticks a run counts in: the tested automaton's own (`Dest`), or
/// the clock of the instance a `.matched` is applied to (`Source`).
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
enum Space {
    Dest,
    Source,
}

/// What an end point's instance produced, by end tick: the distinct frames its
/// attempts matched with there.
type EndStatus = BTreeMap<u32, BTreeSet<Frame>>;

/// One interpretation: the leaf evaluator, the clock model if any, and the two
/// pieces of state that outlive a single attempt -- the memoized free-running
/// status of every end-point instance, and the calls scheduled so far.
struct Runner<'a> {
    eval: Eval<'a>,
    locals: bool,
    /// Length of the [`Space::Dest`] trace.
    len: u32,
    clocks: Option<&'a TraceClocks>,
    /// The per-clock tick lists of a multiclock run (16.13), or `None` when every
    /// position is a tick of every clock. Only [`Space::Dest`] runs consult it.
    timeline: Option<&'a Timeline>,
    /// Keyed by the end point's identity (its address inside the automaton being
    /// run, stable for the whole run) and the space it was evaluated in.
    status: HashMap<(usize, Space), EndStatus>,
    calls: BTreeSet<CallEvent>,
    /// The tail-completed word the run is over (see [`TailWord`]), or `None` for
    /// a plain trace: ticks from `word.real` on are ⊤/⊥ letters, not samples.
    word: Option<&'a TailWord>,
}

impl Runner<'_> {
    fn len_of(&self, space: Space) -> u32 {
        match space {
            Space::Dest => self.len,
            Space::Source => self.clocks.map_or(0, |c| c.source.len() as u32),
        }
    }

    /// Every attempt of `au` started at every tick of `space`: what a
    /// free-running sequence instance does (16.9.11, "does not depend upon the
    /// starting point").
    fn free_run(&mut self, au: &Automaton, space: Space) -> Result<EndStatus, TraceError> {
        let mut out = EndStatus::new();
        for start in 0..self.len_of(space) {
            // An attempt starts at a tick of the instance's own clock only.
            if space == Space::Dest
                && self
                    .timeline
                    .is_some_and(|t| !t.is_tick(au.entry_clock, start))
            {
                continue;
            }
            for (end, frame) in self.attempt(au, start, space)? {
                out.entry(end).or_default().insert(frame);
            }
        }
        Ok(out)
    }

    /// The status of `ep`'s instance for a run in `space`, computed once.
    fn end_status(&mut self, ep: &EndPoint, space: Space) -> Result<&EndStatus, TraceError> {
        let key = (std::ptr::from_ref(ep) as usize, space);
        if !self.status.contains_key(&key) {
            let computed = self.compute_status(ep, space)?;
            self.status.insert(key, computed);
        }
        Ok(&self.status[&key])
    }

    fn compute_status(&mut self, ep: &EndPoint, space: Space) -> Result<EndStatus, TraceError> {
        match (ep.method, space) {
            // Same clock: the instance's end ticks are this run's ticks.
            (EndMethod::Triggered, _) => self.free_run(&ep.automaton, space),
            (EndMethod::Matched, Space::Source) => Err(TraceError::NestedMatched),
            (EndMethod::Matched, Space::Dest) => {
                let Some(clocks) = self.clocks else {
                    // Over a shared timeline: the instance's raw end points, at
                    // ticks of its own clock; the reading edge gathers the ones
                    // since its own clock's previous tick (the handoff below).
                    return self.free_run(&ep.automaton, Space::Dest);
                };
                let source = self.free_run(&ep.automaton, Space::Source)?;
                let mut out = EndStatus::new();
                for (d, &hi) in clocks.dest.iter().enumerate() {
                    // The one-slot handoff: a testing tick sees every match
                    // since the previous testing tick, including one at its own
                    // time (see `EndMethod::Matched`).
                    let lo = d.checked_sub(1).map(|p| clocks.dest[p]);
                    let mut frames = BTreeSet::new();
                    for (&end, fs) in &source {
                        let t = clocks.source[end as usize];
                        if t <= hi && lo.is_none_or(|l| t > l) {
                            frames.extend(fs.iter().cloned());
                        }
                    }
                    if !frames.is_empty() {
                        out.insert(d as u32, frames);
                    }
                }
                Ok(out)
            }
        }
    }

    /// One evaluation attempt of `au` started at tick `start` of `space`.
    fn attempt(
        &mut self,
        au: &Automaton,
        start: u32,
        space: Space,
    ) -> Result<BTreeSet<(u32, Frame)>, TraceError> {
        // A fresh attempt gets a fresh frame: no variable has a value carried
        // over from a previous attempt (16.10).
        let frame = vec![None; au.local_vars.len()];
        self.attempt_from(au, au.start, frame, start, au.entry_clock, space)
    }

    /// [`Runner::attempt`] from an arbitrary entry state and initial frame: the
    /// shape a property evaluator needs, where one automaton holds many
    /// sequences' entries and a consequent's sequence starts with the frame the
    /// antecedent left behind.
    fn attempt_from(
        &mut self,
        au: &Automaton,
        entry: ThreadStateId,
        frame0: Frame,
        start: u32,
        dom0: ClockId,
        space: Space,
    ) -> Result<BTreeSet<(u32, Frame)>, TraceError> {
        let (raw_eval, locals, len, word) = (self.eval, self.locals, self.len_of(space), self.word);
        // Only the run in the automaton's own space has a timeline.
        let timeline = if space == Space::Dest {
            self.timeline
        } else {
            None
        };
        // The position of the `k`-th tick of `dom` after `from` (`k == 0`: `from`).
        let step = |dom: ClockId, from: u32, k: u32| -> u32 {
            timeline.map_or(from + k, |t| t.kth_after(dom, from, k))
        };
        let start = timeline.map_or(start, |t| t.next_tick(dom0, start));
        // Past the real samples a leaf is a ⊤/⊥ letter, not a value: a guard
        // holds on ⊤ and never on ⊥ (F.5.3), and a value read there is an
        // arbitrary constant (F.5.5: "any constant values of the type"), 0.
        let letter = |tick: u32| -> Option<bool> {
            if space == Space::Dest {
                word.and_then(|w| w.letter(tick))
            } else {
                None
            }
        };
        let eval = |leaf: LeafId, tick: u32, frame: &[Option<i64>]| -> Result<i64, TraceError> {
            match letter(tick) {
                Some(_) => Ok(0),
                None => raw_eval(leaf, tick, frame),
            }
        };
        let mut matches = BTreeSet::new();
        // (group, begin tick) -> the earliest end tick recorded for it.
        let mut table: BTreeMap<(FirstMatchId, u32), u32> = BTreeMap::new();
        let mut seen: BTreeSet<Config> = BTreeSet::new();
        let mut work: BTreeSet<Config> = BTreeSet::new();
        if start < len {
            work.insert((start, entry.0, dom0, Vec::new(), frame0));
        }
        while let Some((tick, state, dom, tags, frame)) = work.pop_first() {
            if !seen.insert((tick, state, dom, tags.clone(), frame.clone())) {
                continue;
            }
            let st = au.state(ThreadStateId(state));
            for edge in &st.edges {
                if let Some(g) = edge.guard {
                    let holds = match letter(tick) {
                        Some(top) => top,
                        None => raw_eval(g, tick, &frame)? != 0,
                    };
                    if !holds {
                        continue;
                    }
                }
                let target = edge.target.0;
                match &edge.label {
                    Transition::Epsilon => {
                        work.insert((tick, target, dom, tags.clone(), frame.clone()));
                    }
                    Transition::Delay { min, max } if timeline.is_none() => {
                        let room = len - 1 - tick;
                        let hi = max.map_or(room, |m| m.min(room));
                        for k in *min..=hi {
                            work.insert((tick + k, target, dom, tags.clone(), frame.clone()));
                        }
                    }
                    // `##[min:max]` counts ticks of the thread's current clock
                    // (16.13.1); the first position past the trace ends the window.
                    Transition::Delay { min, max } => {
                        let mut k = *min;
                        while max.is_none_or(|m| k <= m) {
                            let to = step(dom, tick, k);
                            if to >= len {
                                break;
                            }
                            work.insert((to, target, dom, tags.clone(), frame.clone()));
                            k += 1;
                        }
                    }
                    Transition::ClockSync { to, strict } => {
                        let at = if *strict {
                            step(*to, tick, 1)
                        } else {
                            timeline.map_or(tick, |t| t.next_tick(*to, tick))
                        };
                        if at < len {
                            work.insert((at, target, *to, tags.clone(), frame.clone()));
                        }
                    }
                    Transition::Match { .. } => {
                        matches.insert((tick, frame.clone()));
                    }
                    Transition::FirstMatchBegin { group } => {
                        if tags.iter().any(|(g, _)| g == group) {
                            return Err(TraceError::BeginWhileOpen(*group));
                        }
                        let mut t2 = tags.clone();
                        t2.push((*group, tick));
                        t2.sort();
                        work.insert((tick, target, dom, t2, frame.clone()));
                    }
                    Transition::FirstMatchEnd { group } => {
                        let Some(pos) = tags.iter().position(|(g, _)| g == group) else {
                            return Err(TraceError::EndWithoutBegin(*group));
                        };
                        let begin = tags[pos].1;
                        let earliest = *table.entry((*group, begin)).or_insert(tick);
                        if earliest == tick {
                            let mut t2 = tags.clone();
                            t2.remove(pos);
                            work.insert((tick, target, dom, t2, frame.clone()));
                        }
                    }
                    Transition::Abort { .. } => return Err(TraceError::UnsupportedEdge("Abort")),
                    Transition::LocalVarWrite { var, value } => {
                        if !locals {
                            return Err(TraceError::UnsupportedEdge("LocalVarWrite"));
                        }
                        let v = au.local_var(*var).cast(eval(*value, tick, &frame)?);
                        let mut f2 = frame.clone();
                        f2[var.0 as usize] = Some(v);
                        work.insert((tick, target, dom, tags.clone(), f2));
                    }
                    Transition::LocalVarCopy { dst, src } => {
                        if !locals {
                            return Err(TraceError::UnsupportedEdge("LocalVarCopy"));
                        }
                        let mut f2 = frame.clone();
                        wide::copy_local(
                            &mut f2,
                            *dst,
                            au.local_var(*dst),
                            &frame,
                            *src,
                            au.local_var(*src),
                        );
                        work.insert((tick, target, dom, tags.clone(), f2));
                    }
                    Transition::LocalVarStep { var, delta } => {
                        if !locals {
                            return Err(TraceError::UnsupportedEdge("LocalVarStep"));
                        }
                        let decl = au.local_var(*var);
                        let mut f2 = frame.clone();
                        if decl.is_wide() {
                            wide::step_local(&mut f2, *var, decl, *delta)
                                .ok_or(TraceError::UnassignedRead(*var))?;
                        } else {
                            let cur = read_local(&frame, *var)?;
                            f2[var.0 as usize] = Some(decl.cast(cur.wrapping_add(*delta)));
                        }
                        work.insert((tick, target, dom, tags.clone(), f2));
                    }
                    Transition::SubroutineCall { call, args } => {
                        if !locals {
                            return Err(TraceError::UnsupportedEdge("SubroutineCall"));
                        }
                        let mut vals = Vec::with_capacity(args.len());
                        for a in args {
                            vals.push(match a {
                                CallArg::Value(leaf) => Some(eval(*leaf, tick, &frame)?),
                                CallArg::Ref | CallArg::Const => None,
                            });
                        }
                        // A call scheduled on a ⊤/⊥ letter is not a real call.
                        if letter(tick).is_none() {
                            self.calls.insert(CallEvent {
                                tick,
                                call: *call,
                                args: vals,
                            });
                        }
                        work.insert((tick, target, dom, tags.clone(), frame.clone()));
                    }
                    Transition::EndPoint { point, flag } => {
                        if !locals {
                            return Err(TraceError::UnsupportedEdge("EndPoint"));
                        }
                        if let Some(top) = letter(tick) {
                            // `s.triggered` on a ⊤ letter holds like any Boolean
                            // does there, and never on ⊥ (F.5.3).
                            if let Some(slot) = flag {
                                let mut f2 = frame.clone();
                                f2[slot.0 as usize] = Some(i64::from(top));
                                work.insert((tick, target, dom, tags.clone(), f2));
                            } else if top {
                                work.insert((tick, target, dom, tags.clone(), frame.clone()));
                            }
                            continue;
                        }
                        let ep = au.end_point(*point);
                        // `.matched` over a shared timeline (16.13.5): the one-slot
                        // handoff sees every end point since the previous tick of
                        // the testing thread's clock, up to and including this one.
                        let handoff = (ep.method == EndMethod::Matched && self.clocks.is_none())
                            .then(|| {
                                (0..tick)
                                    .rev()
                                    .find(|&p| self.timeline.is_none_or(|t| t.is_tick(dom, p)))
                                    .map_or(0, |p| p + 1)
                            });
                        let status = self.end_status(ep, space)?;
                        let frames: Vec<Frame> = match handoff {
                            Some(lo) => status
                                .range(lo..=tick)
                                .flat_map(|(_, s)| s.iter().cloned())
                                .collect::<BTreeSet<Frame>>()
                                .into_iter()
                                .collect(),
                            None => status
                                .get(&tick)
                                .map(|s| s.iter().cloned().collect())
                                .unwrap_or_default(),
                        };
                        if let Some(slot) = flag {
                            // Inside a larger expression: the status is a value the
                            // leaf reads, and the thread goes on either way.
                            let mut f2 = frame.clone();
                            f2[slot.0 as usize] = Some(i64::from(!frames.is_empty()));
                            work.insert((tick, target, dom, tags.clone(), f2));
                        } else {
                            // A guard: one thread per distinct matching frame, each
                            // taking the flowed-out variables with it.
                            for sub in frames {
                                let mut f2 = frame.clone();
                                for &(from, to) in &ep.flow_out {
                                    wide::copy_local(
                                        &mut f2,
                                        to,
                                        au.local_var(to),
                                        &sub,
                                        from,
                                        au.local_var(from),
                                    );
                                }
                                work.insert((tick, target, dom, tags.clone(), f2));
                            }
                        }
                    }
                }
            }
        }
        Ok(matches)
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::sva::ir::{AbortMode, LocalVarId};

    /// `leaf(i, t)` for a table of per-leaf boolean rows.
    fn rows(table: &'static [&'static [bool]]) -> impl Fn(LeafId, u32) -> bool {
        move |id, t| {
            table[id.0 as usize]
                .get(t as usize)
                .copied()
                .unwrap_or(false)
        }
    }

    /// `l0 ##1 l1`: guard l0, Delay{1,1}, guard l1, Match.
    fn a_then_b() -> Automaton {
        let mut a = Automaton::empty();
        let s0 = a.start;
        let (s1, s2, s3) = (a.new_state(), a.new_state(), a.new_state());
        a.add_edge(s0, Some(LeafId(0)), Transition::Epsilon, s1);
        a.add_edge(
            s1,
            None,
            Transition::Delay {
                min: 1,
                max: Some(1),
            },
            s2,
        );
        a.add_edge(s2, Some(LeafId(1)), Transition::Epsilon, s3);
        a.add_edge(s3, None, Transition::Match { actions: vec![] }, s3);
        a
    }

    #[test]
    fn concatenation_ends_one_tick_after_the_start() {
        let a = a_then_b();
        let tr = rows(&[&[true, false, true], &[false, true, false]]);
        let at0 = attempt(&a, 0, 3, &tr).unwrap();
        assert_eq!(at0.ends, BTreeSet::from([1]));
        assert!(!at0.admits_empty);
        // From tick 1: `a` is false there.
        assert!(attempt(&a, 1, 3, &tr).unwrap().ends.is_empty());
        // From tick 2: `a` holds but there is no tick 3 to sample `b` on.
        assert!(attempt(&a, 2, 3, &tr).unwrap().ends.is_empty());
    }

    #[test]
    fn delay_window_yields_every_end_tick_in_range() {
        let mut a = Automaton::empty();
        let s0 = a.start;
        let (s1, s2) = (a.new_state(), a.new_state());
        a.add_edge(
            s0,
            None,
            Transition::Delay {
                min: 1,
                max: Some(3),
            },
            s1,
        );
        a.add_edge(s1, Some(LeafId(0)), Transition::Epsilon, s2);
        a.add_edge(s2, None, Transition::Match { actions: vec![] }, s2);
        let tr = rows(&[&[false, true, false, true, true]]);
        assert_eq!(
            attempt(&a, 0, 5, &tr).unwrap().ends,
            BTreeSet::from([1, 3]),
            "tick 4 is outside the window, tick 2 fails the guard"
        );
    }

    #[test]
    fn unbounded_delay_stops_at_the_end_of_the_trace() {
        let mut a = Automaton::empty();
        let s0 = a.start;
        let s1 = a.new_state();
        a.add_edge(s0, None, Transition::Delay { min: 0, max: None }, s1);
        a.add_edge(s1, None, Transition::Match { actions: vec![] }, s1);
        let tr = rows(&[]);
        assert_eq!(
            attempt(&a, 1, 4, &tr).unwrap().ends,
            BTreeSet::from([1, 2, 3])
        );
    }

    /// `first_match(##[0:2] l0)` begun at `start`: the markers around a region
    /// that can match on three different ticks.
    fn first_of_window() -> Automaton {
        let mut a = Automaton::empty();
        let g = a.new_first_match_group();
        let s0 = a.start;
        let (s1, s2, s3, s4) = (a.new_state(), a.new_state(), a.new_state(), a.new_state());
        a.add_edge(s0, None, Transition::FirstMatchBegin { group: g }, s1);
        a.add_edge(
            s1,
            None,
            Transition::Delay {
                min: 0,
                max: Some(2),
            },
            s2,
        );
        a.add_edge(s2, Some(LeafId(0)), Transition::Epsilon, s3);
        a.add_edge(s3, None, Transition::FirstMatchEnd { group: g }, s4);
        a.add_edge(s4, None, Transition::Match { actions: vec![] }, s4);
        a
    }

    #[test]
    fn first_match_keeps_only_the_earliest_end() {
        let a = first_of_window();
        let tr = rows(&[&[false, true, true, true]]);
        assert_eq!(attempt(&a, 0, 4, &tr).unwrap().ends, BTreeSet::from([1]));
        // Without the markers all three would match: the guard alone is not
        // what narrows the result.
        let mut plain = a.clone();
        for st in &mut plain.states {
            for e in &mut st.edges {
                if matches!(
                    e.label,
                    Transition::FirstMatchBegin { .. } | Transition::FirstMatchEnd { .. }
                ) {
                    e.label = Transition::Epsilon;
                }
            }
        }
        assert_eq!(
            attempt(&plain, 0, 4, &tr).unwrap().ends,
            BTreeSet::from([1, 2]),
            "window is ticks 0..=2 and the guard holds on 1 and 2"
        );
    }

    #[test]
    fn first_match_regions_beginning_on_different_ticks_are_independent() {
        // `##[0:1] first_match(##[0:2] l0)`: begin tick 0 and begin tick 1 each
        // keep their own earliest end.
        let mut a = Automaton::empty();
        let g = a.new_first_match_group();
        let s0 = a.start;
        let (s1, s2, s3, s4, s5) = (
            a.new_state(),
            a.new_state(),
            a.new_state(),
            a.new_state(),
            a.new_state(),
        );
        a.add_edge(
            s0,
            None,
            Transition::Delay {
                min: 0,
                max: Some(1),
            },
            s1,
        );
        a.add_edge(s1, None, Transition::FirstMatchBegin { group: g }, s2);
        a.add_edge(
            s2,
            None,
            Transition::Delay {
                min: 0,
                max: Some(2),
            },
            s3,
        );
        a.add_edge(s3, Some(LeafId(0)), Transition::Epsilon, s4);
        a.add_edge(s4, None, Transition::FirstMatchEnd { group: g }, s5);
        a.add_edge(s5, None, Transition::Match { actions: vec![] }, s5);
        // leaf true on ticks 1 and 3. Begin 0: window 0..=2, earliest 1.
        // Begin 1: window 1..=3, earliest 1. So only tick 1 -- tick 3 is
        // blocked for begin 1 by begin 1's OWN earlier end.
        let tr = rows(&[&[false, true, false, true, false]]);
        assert_eq!(attempt(&a, 0, 5, &tr).unwrap().ends, BTreeSet::from([1]));
        // The discriminating case for keying the table by BEGIN tick: leaf
        // true on ticks 0 and 1. Begin 0's earliest end is 0; begin 1's is 1,
        // which a table keyed by group alone would wrongly block (0 < 1).
        let tr = rows(&[&[true, true, false, false, false]]);
        assert_eq!(attempt(&a, 0, 5, &tr).unwrap().ends, BTreeSet::from([0, 1]));
        // leaf true on ticks 2 and 3 only: begin 0 -> earliest 2; begin 1 ->
        // earliest 2. Tick 3 is never a first match.
        let tr = rows(&[&[false, false, true, true, false]]);
        assert_eq!(attempt(&a, 0, 5, &tr).unwrap().ends, BTreeSet::from([2]));
        // leaf true on tick 3 only: begin 0's window (0..=2) misses it, begin
        // 1's window reaches it, and nothing earlier blocks it.
        let tr = rows(&[&[false, false, false, true, false]]);
        assert_eq!(attempt(&a, 0, 5, &tr).unwrap().ends, BTreeSet::from([3]));
    }

    #[test]
    fn first_match_end_without_begin_is_a_named_error() {
        let mut a = Automaton::empty();
        let s0 = a.start;
        let s1 = a.new_state();
        a.add_edge(
            s0,
            None,
            Transition::FirstMatchEnd {
                group: FirstMatchId(7),
            },
            s1,
        );
        let tr = rows(&[]);
        assert_eq!(
            attempt(&a, 0, 2, &tr),
            Err(TraceError::EndWithoutBegin(FirstMatchId(7)))
        );
    }

    #[test]
    fn nested_begin_of_an_open_group_is_a_named_error() {
        let mut a = Automaton::empty();
        let g = FirstMatchId(0);
        let s0 = a.start;
        let (s1, s2) = (a.new_state(), a.new_state());
        a.add_edge(s0, None, Transition::FirstMatchBegin { group: g }, s1);
        a.add_edge(s1, None, Transition::FirstMatchBegin { group: g }, s2);
        let tr = rows(&[]);
        assert_eq!(attempt(&a, 0, 2, &tr), Err(TraceError::BeginWhileOpen(g)));
    }

    // -- T13: the local-variable frame ------------------------------------

    /// `eval` for a table of per-leaf closures over `(tick, frame)`.
    type Eval<'a> = &'a dyn Fn(LeafId, u32, &[Option<i64>]) -> Result<i64, TraceError>;

    /// `v0 = leaf0` (a 4-bit unsigned slot), then a guard `leaf1`, then a match.
    fn write_then_guard() -> Automaton {
        let mut a = Automaton::empty();
        let v0 = a.new_local_var(4, false);
        let s0 = a.start;
        let (s1, s2, s3) = (a.new_state(), a.new_state(), a.new_state());
        a.add_edge(
            s0,
            None,
            Transition::LocalVarWrite {
                var: v0,
                value: LeafId(0),
            },
            s1,
        );
        a.add_edge(
            s1,
            None,
            Transition::Delay {
                min: 1,
                max: Some(1),
            },
            s2,
        );
        a.add_edge(s2, Some(LeafId(1)), Transition::Epsilon, s3);
        a.add_edge(s3, None, Transition::Match { actions: vec![] }, s3);
        a
    }

    #[test]
    fn a_local_write_is_cast_to_the_slot_type_and_later_leaves_read_it() {
        let a = write_then_guard();
        // leaf 0 is the constant 0x1f (does not fit 4 bits: stores 0xf); leaf 1
        // is `v0 == 15`.
        let ev: Eval = &|id, _t, frame| match id.0 {
            0 => Ok(0x1f),
            1 => Ok(i64::from(read_local(frame, LocalVarId(0))? == 15)),
            _ => unreachable!(),
        };
        let r = attempt_with_locals(&a, 0, 3, ev).unwrap();
        assert_eq!(r.ends(), BTreeSet::from([1]));
        assert_eq!(
            r.matches,
            BTreeSet::from([(1, vec![Some(0xf)])]),
            "the frame at the match carries the cast value"
        );
        // The same automaton with a guard that wants the UNCAST value fails.
        let ev: Eval = &|id, _t, frame| match id.0 {
            0 => Ok(0x1f),
            1 => Ok(i64::from(read_local(frame, LocalVarId(0))? == 0x1f)),
            _ => unreachable!(),
        };
        assert!(
            attempt_with_locals(&a, 0, 3, ev)
                .unwrap()
                .matches
                .is_empty()
        );
    }

    #[test]
    fn reading_an_unassigned_slot_is_a_named_error() {
        let mut a = write_then_guard();
        // Drop the write: the guard now reads a slot nothing assigned.
        a.states[0].edges[0].label = Transition::Epsilon;
        let ev: Eval = &|id, _t, frame| match id.0 {
            1 => Ok(i64::from(read_local(frame, LocalVarId(0))? == 15)),
            _ => unreachable!(),
        };
        assert_eq!(
            attempt_with_locals(&a, 0, 3, ev),
            Err(TraceError::UnassignedRead(LocalVarId(0)))
        );
        let e = TraceError::UnassignedRead(LocalVarId(3));
        assert!(e.to_string().contains("unassigned local variable 3"), "{e}");
    }

    /// A forking thread carries its own COPY of the frame (16.10 rule (c)): two
    /// branches that assign different values reach the match with one frame each.
    #[test]
    fn forked_threads_keep_independent_frames() {
        let mut a = Automaton::empty();
        let v0 = a.new_local_var(8, false);
        let s0 = a.start;
        let (l, r, end) = (a.new_state(), a.new_state(), a.new_state());
        a.add_edge(s0, None, Transition::Epsilon, l);
        a.add_edge(s0, None, Transition::Epsilon, r);
        for (from, leaf) in [(l, 0), (r, 1)] {
            a.add_edge(
                from,
                None,
                Transition::LocalVarWrite {
                    var: v0,
                    value: LeafId(leaf),
                },
                end,
            );
        }
        a.add_edge(end, None, Transition::Match { actions: vec![] }, end);
        let ev: Eval = &|id, _t, _f| Ok(10 + i64::from(id.0));
        let r = attempt_with_locals(&a, 0, 1, ev).unwrap();
        assert_eq!(
            r.matches,
            BTreeSet::from([(0, vec![Some(10)]), (0, vec![Some(11)])])
        );
        assert_eq!(r.ends(), BTreeSet::from([0]));
    }

    /// `LocalVarCopy` casts to the destination's type and propagates
    /// "unassigned".
    #[test]
    fn a_local_copy_casts_to_the_destination_and_keeps_unassigned() {
        let mut a = Automaton::empty();
        let wide = a.new_local_var(8, true);
        let narrow = a.new_local_var(4, true);
        let never = a.new_local_var(8, true);
        let sink = a.new_local_var(8, true);
        let s0 = a.start;
        let (s1, s2, s3, s4) = (a.new_state(), a.new_state(), a.new_state(), a.new_state());
        a.add_edge(
            s0,
            None,
            Transition::LocalVarWrite {
                var: wide,
                value: LeafId(0),
            },
            s1,
        );
        a.add_edge(
            s1,
            None,
            Transition::LocalVarCopy {
                dst: narrow,
                src: wide,
            },
            s2,
        );
        // `sink` is assigned first, then overwritten with `never`'s "unassigned".
        a.add_edge(
            s2,
            None,
            Transition::LocalVarWrite {
                var: sink,
                value: LeafId(0),
            },
            s3,
        );
        a.add_edge(
            s3,
            None,
            Transition::LocalVarCopy {
                dst: sink,
                src: never,
            },
            s4,
        );
        a.add_edge(s4, None, Transition::Match { actions: vec![] }, s4);
        let ev: Eval = &|_, _, _| Ok(0x39);
        let r = attempt_with_locals(&a, 0, 1, ev).unwrap();
        // 0x39 is 57 in a signed 8-bit slot; truncated to 4 bits that is 0x9 = -7.
        assert_eq!(
            r.matches,
            BTreeSet::from([(0, vec![Some(0x39), Some(-7), None, None])])
        );
    }

    /// The plain boolean entry point has no frame, so a local edge is refused.
    #[test]
    fn the_plain_attempt_refuses_local_edges() {
        let a = write_then_guard();
        let tr = rows(&[]);
        assert_eq!(
            attempt(&a, 0, 3, &tr),
            Err(TraceError::UnsupportedEdge("LocalVarWrite"))
        );
        let mut b = Automaton::empty();
        let (x, y) = (b.new_local_var(1, false), b.new_local_var(1, false));
        let (s0, s1) = (b.start, b.new_state());
        b.add_edge(s0, None, Transition::LocalVarCopy { dst: x, src: y }, s1);
        assert_eq!(
            attempt(&b, 0, 3, &tr),
            Err(TraceError::UnsupportedEdge("LocalVarCopy"))
        );
    }

    // -- T14: match-item edges ---------------------------------------------

    /// `v0 = leaf0` then `v0++` then `v0--` `n` times as given, then a match.
    fn write_then_steps(width: u32, signed: bool, deltas: &[i64]) -> Automaton {
        let mut a = Automaton::empty();
        let v0 = a.new_local_var(width, signed);
        let mut cur = a.start;
        let next = a.new_state();
        a.add_edge(
            cur,
            None,
            Transition::LocalVarWrite {
                var: v0,
                value: LeafId(0),
            },
            next,
        );
        cur = next;
        for d in deltas {
            let next = a.new_state();
            a.add_edge(
                cur,
                None,
                Transition::LocalVarStep { var: v0, delta: *d },
                next,
            );
            cur = next;
        }
        a.add_edge(cur, None, Transition::Match { actions: vec![] }, cur);
        a
    }

    #[test]
    fn a_step_adds_its_delta_and_wraps_at_the_slot_width() {
        let ev: Eval = &|_, _, _| Ok(14);
        let a = write_then_steps(4, false, &[1, 1, 1]);
        // 14 -> 15 -> 0 -> 1 in a 4-bit unsigned slot.
        assert_eq!(
            attempt_with_locals(&a, 0, 1, ev).unwrap().matches,
            BTreeSet::from([(0, vec![Some(1)])])
        );
        let a = write_then_steps(4, true, &[1, 1]);
        // 14 is -2 in a signed 4-bit slot; stepping up gives -1 then 0.
        assert_eq!(
            attempt_with_locals(&a, 0, 1, ev).unwrap().matches,
            BTreeSet::from([(0, vec![Some(0)])])
        );
        let a = write_then_steps(8, false, &[-1, -1]);
        assert_eq!(
            attempt_with_locals(&a, 0, 1, ev).unwrap().matches,
            BTreeSet::from([(0, vec![Some(12)])])
        );
    }

    #[test]
    fn a_step_of_an_unassigned_slot_is_a_named_error() {
        let mut a = write_then_steps(8, false, &[1]);
        a.states[0].edges[0].label = Transition::Epsilon;
        let ev: Eval = &|_, _, _| Ok(0);
        assert_eq!(
            attempt_with_locals(&a, 0, 1, ev),
            Err(TraceError::UnassignedRead(LocalVarId(0)))
        );
    }

    /// A variable of 130 bits is written limb by limb (value limbs, then unknown
    /// limbs: leaf `i` is the i-th slot's word), stepped, and copied to a second
    /// one and to a narrow one: the whole variable moves, not just its head slot.
    #[test]
    fn a_wide_local_is_written_stepped_and_copied_as_a_whole() {
        let mut a = Automaton::empty();
        let w = a.new_local_var(130, false);
        let w2 = a.new_local_var(130, false);
        let n = a.new_local_var(8, false);
        assert_eq!(
            (w.0, w2.0, n.0, a.local_vars.len()),
            (0, 6, 12, 13),
            "three limbs of value and of unknown plane per wide variable"
        );
        let mut cur = a.start;
        for slot in 0..6u32 {
            let next = a.new_state();
            a.add_edge(
                cur,
                None,
                Transition::LocalVarWrite {
                    var: LocalVarId(slot),
                    value: LeafId(slot),
                },
                next,
            );
            cur = next;
        }
        for t in [
            Transition::LocalVarStep { var: w, delta: 1 },
            Transition::LocalVarCopy { dst: w2, src: w },
            Transition::LocalVarCopy { dst: n, src: w },
        ] {
            let next = a.new_state();
            a.add_edge(cur, None, t, next);
            cur = next;
        }
        a.add_edge(cur, None, Transition::Match { actions: vec![] }, cur);
        // value limbs [!0, 1, 3], unknown limbs [0, 0, 0]
        let words = [-1i64, 1, 3, 0, 0, 0];
        let ev: Eval = &|id, _t, _f| Ok(words[id.0 as usize]);
        let r = attempt_with_locals(&a, 0, 1, ev).unwrap();
        let limbs = [Some(0), Some(2), Some(3), Some(0), Some(0), Some(0)];
        let mut frame = limbs.to_vec();
        frame.extend(limbs);
        frame.push(Some(0));
        assert_eq!(
            r.matches,
            BTreeSet::from([(0, frame)]),
            "!0 + 1 carries into limb 1; the copies take every limb, the narrow one the low byte"
        );
    }

    /// Stepping a wide variable with an unknown bit makes it all `x`.
    #[test]
    fn a_step_of_a_wide_local_with_an_unknown_bit_is_unknown() {
        let mut a = Automaton::empty();
        let w = a.new_local_var(70, false);
        let mut cur = a.start;
        for slot in 0..4u32 {
            let next = a.new_state();
            a.add_edge(
                cur,
                None,
                Transition::LocalVarWrite {
                    var: LocalVarId(slot),
                    value: LeafId(slot),
                },
                next,
            );
            cur = next;
        }
        let next = a.new_state();
        a.add_edge(
            cur,
            None,
            Transition::LocalVarStep { var: w, delta: 1 },
            next,
        );
        a.add_edge(next, None, Transition::Match { actions: vec![] }, next);
        let words = [5i64, 0, 1, 0];
        let ev: Eval = &|id, _t, _f| Ok(words[id.0 as usize]);
        let r = attempt_with_locals(&a, 0, 1, ev).unwrap();
        assert_eq!(
            r.matches,
            BTreeSet::from([(0, vec![Some(0), Some(0), Some(-1), Some(0x3f)])])
        );
    }

    /// `(l0, call#0(l1, ref)) ##1 (l2, call#1()) `: both calls fire, in the
    /// order of the end points, with the sampled value of by-value arguments.
    fn two_calls() -> Automaton {
        let mut a = Automaton::empty();
        let s0 = a.start;
        let (s1, s2, s3, s4, s5) = (
            a.new_state(),
            a.new_state(),
            a.new_state(),
            a.new_state(),
            a.new_state(),
        );
        a.add_edge(s0, Some(LeafId(0)), Transition::Epsilon, s1);
        a.add_edge(
            s1,
            None,
            Transition::SubroutineCall {
                call: CallId(0),
                args: vec![CallArg::Value(LeafId(1)), CallArg::Ref, CallArg::Const],
            },
            s2,
        );
        a.add_edge(
            s2,
            None,
            Transition::Delay {
                min: 1,
                max: Some(1),
            },
            s3,
        );
        a.add_edge(s3, Some(LeafId(2)), Transition::Epsilon, s4);
        a.add_edge(
            s4,
            None,
            Transition::SubroutineCall {
                call: CallId(1),
                args: vec![],
            },
            s5,
        );
        a.add_edge(s5, None, Transition::Match { actions: vec![] }, s5);
        a
    }

    #[test]
    fn a_call_is_recorded_with_its_sampled_arguments() {
        let a = two_calls();
        // leaf 1 is the tick number plus 100: the sampled value at the call.
        let ev: Eval = &|id, t, _| match id.0 {
            1 => Ok(100 + i64::from(t)),
            _ => Ok(1),
        };
        let r = attempt_with_calls(&a, 0, 3, ev).unwrap();
        assert_eq!(r.attempt.ends(), BTreeSet::from([1]));
        assert_eq!(
            r.calls,
            BTreeSet::from([
                CallEvent {
                    tick: 0,
                    call: CallId(0),
                    args: vec![Some(100), None, None]
                },
                CallEvent {
                    tick: 1,
                    call: CallId(1),
                    args: vec![]
                },
            ])
        );
    }

    /// A call fires at its end point even when the sequence it is part of then
    /// fails (16.11): the second operand never holds, no match, yet call #0
    /// was still scheduled.
    #[test]
    fn a_call_fires_even_when_the_longer_sequence_fails() {
        let a = two_calls();
        let ev: Eval = &|id, _, _| match id.0 {
            2 => Ok(0),
            _ => Ok(1),
        };
        let r = attempt_with_calls(&a, 0, 3, ev).unwrap();
        assert!(r.attempt.matches.is_empty());
        assert_eq!(
            r.calls.iter().map(|c| c.call).collect::<Vec<_>>(),
            vec![CallId(0)]
        );
    }

    /// Items run in list order: a call placed between two writes sees only the
    /// first write.
    #[test]
    fn calls_and_writes_run_in_list_order() {
        let mut a = Automaton::empty();
        let v0 = a.new_local_var(8, false);
        let s0 = a.start;
        let (s1, s2, s3, s4) = (a.new_state(), a.new_state(), a.new_state(), a.new_state());
        a.add_edge(
            s0,
            None,
            Transition::LocalVarWrite {
                var: v0,
                value: LeafId(0),
            },
            s1,
        );
        a.add_edge(
            s1,
            None,
            Transition::SubroutineCall {
                call: CallId(0),
                args: vec![CallArg::Value(LeafId(1))],
            },
            s2,
        );
        a.add_edge(s2, None, Transition::LocalVarStep { var: v0, delta: 5 }, s3);
        a.add_edge(
            s3,
            None,
            Transition::SubroutineCall {
                call: CallId(1),
                args: vec![CallArg::Value(LeafId(1))],
            },
            s4,
        );
        a.add_edge(s4, None, Transition::Match { actions: vec![] }, s4);
        // leaf 0 is 3; leaf 1 reads v0.
        let ev: Eval = &|id, _, frame| match id.0 {
            0 => Ok(3),
            _ => read_local(frame, LocalVarId(0)),
        };
        let r = attempt_with_calls(&a, 0, 1, ev).unwrap();
        let by_call: Vec<_> = r.calls.iter().map(|c| (c.call.0, c.args[0])).collect();
        assert_eq!(by_call, vec![(0, Some(3)), (1, Some(8))]);
        assert_eq!(r.attempt.matches, BTreeSet::from([(0, vec![Some(8)])]));
    }

    #[test]
    fn the_plain_attempt_refuses_call_edges() {
        let a = two_calls();
        let tr = rows(&[&[true], &[true], &[true]]);
        assert_eq!(
            attempt(&a, 0, 3, &tr),
            Err(TraceError::UnsupportedEdge("SubroutineCall"))
        );
        let a = write_then_steps(4, false, &[1]);
        assert_eq!(
            attempt(&a, 0, 3, &tr),
            Err(TraceError::UnsupportedEdge("LocalVarWrite"))
        );
        let mut b = Automaton::empty();
        let v = b.new_local_var(1, false);
        let (s0, s1) = (b.start, b.new_state());
        b.add_edge(s0, None, Transition::LocalVarStep { var: v, delta: 1 }, s1);
        assert_eq!(
            attempt(&b, 0, 3, &tr),
            Err(TraceError::UnsupportedEdge("LocalVarStep"))
        );
    }

    #[test]
    fn abort_edges_are_refused_not_ignored() {
        let mut a = Automaton::empty();
        let s0 = a.start;
        let s1 = a.new_state();
        a.add_edge(
            s0,
            None,
            Transition::Abort {
                leaf: LeafId(0),
                mode: AbortMode::Accept,
            },
            s1,
        );
        let tr = rows(&[]);
        assert_eq!(
            attempt(&a, 0, 2, &tr),
            Err(TraceError::UnsupportedEdge("Abort"))
        );
        // The locals-aware entry point has no abort semantics either.
        let ev: Eval = &|_, _, _| Ok(1);
        assert_eq!(
            attempt_with_locals(&a, 0, 2, ev),
            Err(TraceError::UnsupportedEdge("Abort"))
        );
    }

    #[test]
    fn start_outside_the_trace_matches_nothing_and_admits_empty_passes_through() {
        let mut a = a_then_b();
        a.admits_empty = true;
        let tr = rows(&[&[true], &[true]]);
        let r = attempt(&a, 5, 3, &tr).unwrap();
        assert!(r.ends.is_empty());
        assert!(r.admits_empty);
    }

    /// `guard(leaf) ; Match`: the one-tick sequence `leaf`.
    fn one_tick(leaf: u32) -> Automaton {
        let mut a = Automaton::empty();
        let s0 = a.start;
        let s1 = a.new_state();
        a.add_edge(s0, Some(LeafId(leaf)), Transition::Epsilon, s1);
        a.add_edge(s1, None, Transition::Match { actions: vec![] }, s1);
        a
    }

    /// An automaton whose only thing is to test `sub`'s end point, then (if
    /// `then` is a leaf) require it, then match.
    fn tests_end_point(
        method: EndMethod,
        sub: Automaton,
        flow_out: Vec<(LocalVarId, LocalVarId)>,
        flag: Option<LocalVarId>,
        then: Option<LeafId>,
    ) -> Automaton {
        let mut a = Automaton::empty();
        a.local_vars = sub.local_vars.clone();
        let p = a.new_end_point(EndPoint {
            method,
            site: 0,
            automaton: sub,
            flow_out,
        });
        let s0 = a.start;
        let (s1, s2) = (a.new_state(), a.new_state());
        a.add_edge(s0, None, Transition::EndPoint { point: p, flag }, s1);
        a.add_edge(s1, then, Transition::Epsilon, s2);
        a.add_edge(s2, None, Transition::Match { actions: vec![] }, s2);
        a
    }

    /// 16.9.11: the end point status is a property of the instance, not of the
    /// attempt that tests it -- `l0 ##1 l1` ends on tick 1 whichever tick the
    /// testing sequence starts on.
    #[test]
    fn triggered_holds_where_the_instance_ends_whatever_the_start() {
        let a = tests_end_point(EndMethod::Triggered, a_then_b(), vec![], None, None);
        let ev: Eval = &|id, t, _| {
            let rows: [[i64; 4]; 2] = [[1, 0, 1, 0], [0, 1, 0, 0]];
            Ok(rows[id.0 as usize][t as usize])
        };
        for start in 0..4 {
            let r = attempt_with_locals(&a, start, 4, ev).unwrap();
            let want: BTreeSet<u32> = if start == 1 {
                BTreeSet::from([1])
            } else {
                BTreeSet::new()
            };
            assert_eq!(r.ends(), want, "start {start}");
        }
    }

    /// 16.9.11 / `zero_or_one_req`: a sequence that can match empty never makes
    /// `.triggered` true by its empty match, only by a nonempty one.
    #[test]
    fn an_empty_match_never_triggers() {
        let mut sub = one_tick(0);
        sub.admits_empty = true;
        let a = tests_end_point(EndMethod::Triggered, sub, vec![], None, None);
        let never: Eval = &|_, _, _| Ok(0);
        for start in 0..3 {
            assert!(
                attempt_with_locals(&a, start, 3, never)
                    .unwrap()
                    .matches
                    .is_empty(),
                "empty match fired the end point at start {start}"
            );
        }
        let once: Eval = &|_, t, _| Ok(i64::from(t == 1));
        assert_eq!(
            attempt_with_locals(&a, 1, 3, once).unwrap().ends(),
            BTreeSet::from([1])
        );
    }

    /// The flag form (`!s.triggered`): the thread goes on either way and the
    /// status lands in the slot the leaf reads.
    #[test]
    fn the_flag_form_stores_the_status_and_never_blocks() {
        let mut sub = one_tick(0);
        let flag = sub.new_local_var(1, false);
        let a = tests_end_point(
            EndMethod::Triggered,
            sub,
            vec![],
            Some(flag),
            Some(LeafId(1)),
        );
        // sub matches on ticks 0 and 2 only; leaf 1 is `!flag`.
        let ev: Eval = &|id, t, frame| match id.0 {
            0 => Ok(i64::from(t == 0 || t == 2)),
            _ => Ok(i64::from(read_local(frame, LocalVarId(0))? == 0)),
        };
        let r = attempt_with_locals(&a, 0, 4, ev).unwrap();
        assert!(r.matches.is_empty(), "tick 0 is triggered, `!flag` fails");
        let r = attempt_with_locals(&a, 1, 4, ev).unwrap();
        assert_eq!(r.matches, BTreeSet::from([(1, vec![Some(0)])]));
        let r = attempt_with_locals(&a, 3, 4, ev).unwrap();
        assert_eq!(r.matches, BTreeSet::from([(3, vec![Some(0)])]));
        let r = attempt_with_locals(&a, 2, 4, ev).unwrap();
        assert!(r.matches.is_empty());
    }

    /// 16.10: a local variable assigned in the instance flows out of the
    /// maximal application, one thread per distinct frame.
    #[test]
    fn a_maximal_application_forks_per_frame_and_flows_variables_out() {
        let mut sub = Automaton::empty();
        let dst = sub.new_local_var(8, false); // slot 0: the testing thread's
        let src = sub.new_local_var(8, false); // slot 1: the instance's own
        let s0 = sub.start;
        let (w1, w2, m) = (sub.new_state(), sub.new_state(), sub.new_state());
        sub.add_edge(s0, None, Transition::Epsilon, w1);
        sub.add_edge(s0, None, Transition::Epsilon, w2);
        sub.add_edge(
            w1,
            None,
            Transition::LocalVarWrite {
                var: src,
                value: LeafId(0),
            },
            m,
        );
        sub.add_edge(
            w2,
            None,
            Transition::LocalVarWrite {
                var: src,
                value: LeafId(1),
            },
            m,
        );
        sub.add_edge(m, None, Transition::Match { actions: vec![] }, m);
        let a = tests_end_point(EndMethod::Triggered, sub, vec![(src, dst)], None, None);
        let ev: Eval = &|id, t, _| Ok(10 * (i64::from(id.0) + 1) + i64::from(t));
        let r = attempt_with_locals(&a, 2, 3, ev).unwrap();
        assert_eq!(
            r.matches,
            BTreeSet::from([(2, vec![Some(12), None]), (2, vec![Some(22), None]),]),
            "two frames, two threads; the instance's own slot stays out of the thread"
        );
    }

    /// 16.13.5: `.matched` is true at a testing tick when the instance matched
    /// since the previous testing tick, up to and including the tick's own time.
    #[test]
    fn matched_hands_off_across_clocks() {
        let a = tests_end_point(EndMethod::Matched, one_tick(0), vec![], None, None);
        let clocks = TraceClocks {
            dest: vec![10, 20, 30],
            source: vec![5, 12, 18, 25, 31],
        };
        // The source clock's leaf holds on source ticks 0, 1, 2 and 4.
        let ev: Eval = &|_, t, _| Ok(i64::from(matches!(t, 0..=2 | 4)));
        let ends = |start| {
            attempt_with_clocks(&a, start, &clocks, ev)
                .unwrap()
                .attempt
                .ends()
        };
        assert_eq!(ends(0), BTreeSet::from([0]), "t=5 <= 10");
        assert_eq!(ends(1), BTreeSet::from([1]), "t=12 and t=18 in (10, 20]");
        assert!(
            ends(2).is_empty(),
            "t=25 does not hold, t=31 is past tick 30"
        );
        // A match at the very time of the testing tick is seen by it.
        let at_tick = TraceClocks {
            dest: vec![10, 20],
            source: vec![10, 15],
        };
        let only_first: Eval = &|_, t, _| Ok(i64::from(t == 0));
        let r = attempt_with_clocks(&a, 0, &at_tick, only_first).unwrap();
        assert_eq!(r.attempt.ends(), BTreeSet::from([0]));
        // ...and is not repeated at the next one.
        let r = attempt_with_clocks(&a, 1, &at_tick, only_first).unwrap();
        assert!(r.attempt.matches.is_empty());
    }

    #[test]
    fn matched_needs_a_clock_model_and_does_not_nest() {
        let a = tests_end_point(EndMethod::Matched, one_tick(0), vec![], None, None);
        let ev: Eval = &|_, _, _| Ok(1);
        // Without a per-domain clock model the instance runs over the run's own
        // ticks (one shared clock): the handoff is the tick itself.
        assert!(attempt_with_locals(&a, 0, 2, ev).is_ok());
        let clocks = TraceClocks {
            dest: vec![1, 2],
            source: vec![1, 2],
        };
        let inner = tests_end_point(EndMethod::Matched, one_tick(0), vec![], None, None);
        let outer = tests_end_point(EndMethod::Matched, inner, vec![], None, None);
        assert_eq!(
            attempt_with_clocks(&outer, 0, &clocks, ev),
            Err(TraceError::NestedMatched)
        );
        let bad = TraceClocks {
            dest: vec![2, 2],
            source: vec![1],
        };
        assert_eq!(
            attempt_with_clocks(&a, 0, &bad, ev),
            Err(TraceError::BadClocks)
        );
    }

    /// An instance's own match-item calls are reported once it has been tested.
    #[test]
    fn calls_inside_an_instance_are_reported() {
        let a = tests_end_point(EndMethod::Triggered, two_calls(), vec![], None, None);
        let ev: Eval = &|_, _, _| Ok(1);
        let r = attempt_with_calls(&a, 1, 3, ev).unwrap();
        assert_eq!(r.attempt.ends(), BTreeSet::from([1]));
        assert!(r.calls.iter().any(|c| c.call == CallId(1)));
    }

    #[test]
    fn the_plain_attempt_refuses_end_point_edges() {
        let a = tests_end_point(EndMethod::Triggered, one_tick(0), vec![], None, None);
        let tr = rows(&[&[true]]);
        assert_eq!(
            attempt(&a, 0, 1, &tr),
            Err(TraceError::UnsupportedEdge("EndPoint"))
        );
    }

    #[test]
    fn display_names_the_group() {
        let e = TraceError::EndWithoutBegin(FirstMatchId(3));
        assert!(e.to_string().contains("FirstMatchEnd(3)"), "{e}");
        let e = TraceError::BeginWhileOpen(FirstMatchId(4));
        assert!(e.to_string().contains("FirstMatchBegin(4)"), "{e}");
        let e = TraceError::UnsupportedEdge("Abort");
        assert!(e.to_string().contains("Abort"), "{e}");
    }

    #[test]
    fn tail_word_letters_flip_and_cut() {
        let w = TailWord::weak(2);
        assert_eq!(w.letter(1), None);
        assert_eq!(w.letter(2), Some(true));
        assert_eq!(w.letter(99), Some(true));
        assert_eq!(w.extent(), 2);
        let s = w.flip();
        assert_eq!(s, TailWord::strong(2));
        assert_eq!(s.letter(5), Some(false));
        // A `⊥`-tailed word cut at tick 4 keeps two `⊥` letters, then `⊤`.
        let cut = s.cut_then_top(4);
        assert_eq!(cut.letter(2), Some(false));
        assert_eq!(cut.letter(3), Some(false));
        assert_eq!(cut.letter(4), Some(true));
        assert_eq!(cut.extent(), 4);
        assert_eq!(cut.flip().letter(2), Some(true), "flip swaps mid letters");
        assert_eq!(cut.flip().letter(4), Some(false));
        // A cut inside the real samples drops everything after it.
        assert_eq!(s.cut_then_top(1), TailWord::weak(1));
        // Cutting a `⊤` tail adds no `⊥`.
        assert_eq!(w.cut_then_top(5), TailWord::weak(2));
    }

    /// `l0 ##1 l1` over `a ⊤` tail: a `⊤` letter satisfies every guard, `⊥` none.
    #[test]
    fn attempt_word_guards_follow_the_tail_letter() {
        let a = a_then_b();
        let table: &[&[bool]] = &[&[true], &[false]];
        let eval = |l: LeafId, t: u32, _: &[Option<i64>]| -> Result<i64, TraceError> {
            Ok(i64::from(
                table[l.0 as usize]
                    .get(t as usize)
                    .copied()
                    .unwrap_or(false),
            ))
        };
        let run = |w: &TailWord| {
            attempt_word(&a, a.start, &[], 0, w, 6, &eval)
                .unwrap()
                .into_iter()
                .map(|(e, _)| e)
                .collect::<Vec<_>>()
        };
        // `a` at tick 0, then the `⊤` tail supplies `b` at tick 1.
        assert_eq!(run(&TailWord::weak(1)), vec![1]);
        // A `⊥` tail never does: even a constant-true leaf is not satisfied by it.
        assert_eq!(run(&TailWord::strong(1)), Vec::<u32>::new());
        // Starting past the real samples on a `⊤` tail matches immediately.
        let on_tail = attempt_word(&a, a.start, &[], 3, &TailWord::weak(1), 6, &eval).unwrap();
        assert_eq!(
            on_tail.into_iter().map(|(e, _)| e).collect::<Vec<_>>(),
            vec![4]
        );
    }

    /// A call is scheduled where a thread REALLY is: one reached on a real tick
    /// is recorded with its sampled arguments, one reached on a `⊤` letter is
    /// not (16.11: the call is attached to an end point of a sampled sequence).
    #[test]
    fn attempt_word_calls_records_real_ticks_only() {
        let a = two_calls();
        let eval = |l: LeafId, t: u32, _: &[Option<i64>]| -> Result<i64, TraceError> {
            Ok(match l.0 {
                1 => 100 + i64::from(t),
                _ => 1,
            })
        };
        let run = |real: u32| {
            attempt_word_calls(
                &a,
                a.start,
                &[],
                0,
                &TailWord::weak(real),
                6,
                &eval,
                None,
                a.entry_clock,
            )
            .unwrap()
        };
        let (matches, calls) = run(1);
        assert_eq!(
            matches.into_iter().map(|(e, _)| e).collect::<Vec<_>>(),
            vec![1]
        );
        assert_eq!(
            calls.into_iter().collect::<Vec<_>>(),
            vec![CallEvent {
                tick: 0,
                call: CallId(0),
                args: vec![Some(100), None, None]
            }],
            "the second call would fire on tick 1, a `⊤` letter"
        );
        let (_, calls) = run(3);
        assert_eq!(
            calls.iter().map(|c| (c.tick, c.call.0)).collect::<Vec<_>>(),
            vec![(0, 0), (1, 1)]
        );
        // The set-returning wrapper still drops them: same matches either way.
        let plain = attempt_word(&a, a.start, &[], 0, &TailWord::weak(3), 6, &eval).unwrap();
        assert_eq!(plain, run(3).0);
    }

    /// A start state other than `Automaton::start` and an initial frame are honoured.
    #[test]
    fn attempt_word_starts_at_the_given_entry_with_the_given_frame() {
        let mut a = Automaton::empty();
        let v = a.new_local_var(8, false);
        let entry = a.new_state();
        let end = a.new_state();
        a.add_edge(entry, None, Transition::Match { actions: vec![] }, entry);
        let _ = end;
        let eval = |_: LeafId, _: u32, _: &[Option<i64>]| Ok(1);
        let frame = vec![Some(7)];
        let got = attempt_word(&a, entry, &frame, 0, &TailWord::weak(1), 3, &eval).unwrap();
        assert_eq!(
            got.into_iter().collect::<Vec<_>>(),
            vec![(0, vec![Some(7)])]
        );
        assert_eq!(v, LocalVarId(0));
    }

    // -- T28: multiclock timelines (16.13) ---------------------------------

    const C0: ClockId = ClockId(0);
    const C1: ClockId = ClockId(1);

    #[test]
    fn timeline_counts_strictly_subsequent_ticks_and_continues_into_the_tail() {
        // clock 0 ticks at 0, 2, 4; clock 1 at 1, 2; six real steps.
        let tl = Timeline::new(6, vec![vec![0, 2, 4], vec![1, 2]]).unwrap();
        assert_eq!(tl.real(), 6);
        assert!(tl.is_tick(C0, 2) && !tl.is_tick(C0, 3) && tl.is_tick(C1, 1));
        // `##1` from a tick of the OTHER clock is the nearest strictly later tick.
        assert_eq!(tl.kth_after(C1, 0, 1), 1);
        assert_eq!(
            tl.kth_after(C1, 1, 1),
            2,
            "strictly later: not tick 1 itself"
        );
        assert_eq!(
            tl.kth_after(C1, 2, 1),
            6,
            "list exhausted: the tail starts at `real`"
        );
        assert_eq!(tl.kth_after(C0, 0, 2), 4);
        assert_eq!(tl.kth_after(C0, 4, 3), 8, "every tail position is a tick");
        assert_eq!(
            tl.kth_after(C0, 9, 2),
            11,
            "past `real` every position ticks"
        );
        assert_eq!(tl.kth_after(C0, 3, 0), 3, "k = 0 is the position itself");
        // `next_tick` is at-or-after.
        assert_eq!(tl.next_tick(C0, 2), 2);
        assert_eq!(tl.next_tick(C0, 3), 4);
        assert_eq!(tl.next_tick(C0, 5), 6);
        assert_eq!(tl.next_tick(C1, 7), 7);
        // A clock with no list ticks everywhere.
        assert_eq!(tl.kth_after(ClockId(5), 1, 1), 2);
        assert_eq!(tl.next_tick(ClockId(5), 3), 3);
        let rows = Timeline::from_rows(&[&[true, false, true], &[false, true]]);
        assert_eq!(rows.real(), 3);
        assert!(rows.is_tick(C1, 1) && !rows.is_tick(C1, 0));
    }

    #[test]
    fn a_malformed_timeline_is_a_named_error() {
        assert_eq!(
            Timeline::new(4, vec![vec![2, 2]]),
            Err(TraceError::BadTimeline)
        );
        assert_eq!(
            Timeline::new(4, vec![vec![1, 4]]),
            Err(TraceError::BadTimeline),
            "a tick must be a real step"
        );
        assert!(
            TraceError::BadTimeline
                .to_string()
                .contains("strictly increasing")
        );
    }

    /// `l0 ##1 @(c1) l1` (or `##0` when `!strict`): guard l0 on clock 0, a
    /// `ClockSync` to clock 1, guard l1, match.
    fn cross_clock(strict: bool) -> Automaton {
        let mut a = Automaton::empty();
        let s0 = a.start;
        let (s1, s2, s3) = (a.new_state(), a.new_state(), a.new_state());
        a.add_edge(s0, Some(LeafId(0)), Transition::Epsilon, s1);
        a.add_edge(s1, None, Transition::ClockSync { to: C1, strict }, s2);
        a.add_edge(s2, Some(LeafId(1)), Transition::Epsilon, s3);
        a.add_edge(s3, None, Transition::Match { actions: vec![] }, s3);
        a
    }

    /// Ends of one attempt of `a` from `start` over `rows` (leaf rows) on `tl`.
    fn ends_on(
        a: &Automaton,
        start: u32,
        tl: &Timeline,
        leaves: &'static [&'static [bool]],
    ) -> Vec<u32> {
        let ev = move |l: LeafId, t: u32, _: &[Option<i64>]| -> Result<i64, TraceError> {
            Ok(i64::from(
                leaves[l.0 as usize]
                    .get(t as usize)
                    .copied()
                    .unwrap_or(false),
            ))
        };
        attempt_word_in(
            a,
            a.start,
            &[],
            start,
            &TailWord::weak(tl.real()),
            tl.real(),
            &ev,
            Some(tl),
            C0,
        )
        .unwrap()
        .into_iter()
        .map(|(e, _)| e)
        .collect()
    }

    /// 16.13.1: "the nearest strictly subsequent tick of the second clock".
    #[test]
    fn strict_clock_sync_waits_for_the_nearest_strictly_later_tick() {
        // Clock 0 ticks at 0 and 4; clock 1 at 0, 2, 3.
        let tl = Timeline::from_rows(&[
            &[true, false, false, false, true],
            &[true, false, true, true, false],
        ]);
        // l0 holds at 0; l1 holds at 0, 2, 3. `##1` skips the coincident tick 0
        // and lands on tick 2: only the l1 sample at 2 is read.
        let leaves: &'static [&'static [bool]] = &[
            &[true, false, false, false, false],
            &[true, false, false, true, false],
        ];
        assert!(
            ends_on(&cross_clock(true), 0, &tl, leaves).is_empty(),
            "tick 2 is the target and l1 is false there; tick 0 and 3 are not read"
        );
        let leaves: &'static [&'static [bool]] = &[
            &[true, false, false, false, false],
            &[true, false, true, true, false],
        ];
        assert_eq!(ends_on(&cross_clock(true), 0, &tl, leaves), vec![2]);
    }

    /// 16.13.1: `##0` may overlap: "the nearest possibly overlapping tick".
    #[test]
    fn nonstrict_clock_sync_may_overlap_the_current_tick() {
        let tl = Timeline::from_rows(&[
            &[true, false, false, false, true],
            &[true, false, true, true, false],
        ]);
        let leaves: &'static [&'static [bool]] = &[
            &[true, false, false, false, false],
            &[true, false, false, false, false],
        ];
        assert_eq!(
            ends_on(&cross_clock(false), 0, &tl, leaves),
            vec![0],
            "tick 0 is a tick of both clocks: the match overlaps"
        );
        // Where the clocks do not coincide the sync moves forward to clock 1's
        // next tick, exactly as `##1` would.
        let tl = Timeline::from_rows(&[&[true, false, false, false], &[false, false, true, false]]);
        let leaves: &'static [&'static [bool]] =
            &[&[true, false, false, false], &[false, false, true, false]];
        assert_eq!(ends_on(&cross_clock(false), 0, &tl, leaves), vec![2]);
        assert_eq!(ends_on(&cross_clock(true), 0, &tl, leaves), vec![2]);
    }

    /// An attempt starts at the first tick of its entry clock at or after `start`.
    #[test]
    fn an_attempt_aligns_its_start_to_the_entry_clock() {
        let a = a_then_b();
        let tl = Timeline::from_rows(&[&[false, false, true, false, true, false]]);
        let leaves: &'static [&'static [bool]] = &[
            &[false, false, true, false, false, false],
            &[false, false, false, false, true, false],
        ];
        // Started at step 0, the attempt waits for the first clock-0 tick (2), and
        // its `##1` is the NEXT tick of the clock (4), not step 3.
        assert_eq!(ends_on(&a, 0, &tl, leaves), vec![4]);
    }

    /// A `Delay` after a sync counts ticks of the NEW clock.
    #[test]
    fn delay_counts_ticks_of_the_threads_current_clock() {
        // `l0 ##1 @(c1) l1 ##2 l2`
        let mut a = cross_clock(true);
        let m = ThreadStateId(3);
        let (d, g, e) = (a.new_state(), a.new_state(), a.new_state());
        a.states[m.0 as usize].edges.clear();
        a.add_edge(
            m,
            None,
            Transition::Delay {
                min: 2,
                max: Some(2),
            },
            d,
        );
        a.add_edge(d, Some(LeafId(2)), Transition::Epsilon, g);
        a.add_edge(g, None, Transition::Match { actions: vec![] }, g);
        let _ = e;
        // Clock 1 ticks at 1, 3, 4, 6; clock 0 at 0 only.
        let tl = Timeline::from_rows(&[
            &[true, false, false, false, false, false, false],
            &[false, true, false, true, true, false, true],
        ]);
        let leaves: &'static [&'static [bool]] = &[
            &[true, false, false, false, false, false, false],
            &[false, true, false, false, false, false, false],
            &[false, false, false, false, true, false, true],
        ];
        // l1 at the sync tick 1; `##2` is the second later tick of clock 1: 4.
        // l2 holds at 4 (and at 6, which is `##3`, not matched).
        assert_eq!(ends_on(&a, 0, &tl, leaves), vec![4]);
    }

    /// With no timeline a sync is `##1` / `##0` over plain steps.
    #[test]
    fn without_a_timeline_a_clock_sync_is_plain_delay() {
        let table: &'static [&'static [bool]] = &[&[true, false, false], &[false, true, true]];
        let tr = rows(table);
        let strict = attempt(&cross_clock(true), 0, 3, &tr).unwrap();
        assert_eq!(strict.ends, BTreeSet::from([1]));
        let loose = attempt(&cross_clock(false), 0, 3, &tr).unwrap();
        assert!(
            loose.ends.is_empty(),
            "##0 reads l1 at tick 0, where it is false"
        );
    }
}