vj_sim/sva/

ir.rs

//! T4 (`docs/superpowers/plans/2026-10-03-sva.md`): the automaton IR
//! skeleton -- plan §1.2's "a dedicated, interpreted automaton per
//! assertion, compiled once at elaboration time into a static transition
//! table (`vj-sim::sva::Automaton`), stepped by a small engine in
//! `vj-runtime::sva_engine`" decision, materialized as the types that
//! table is made of. This task builds the IR *types only* -- no builder
//! (that's T9/T10 onward, consuming `vj-codegen::sva::{ranges, op}`'s
//! already-recovered delay/repetition bounds and operator values) and no
//! engine (`vj-runtime::sva_engine`, a later task).
//!
//! Every ID below is a handle into whichever table its automaton (or the
//! engine stepping it) owns -- the same "small newtype handle, real storage
//! lives in a `slotmap`/`Vec` elsewhere" shape this crate already uses for
//! [`crate::netlist::InstanceId`]/[`crate::process::StmtId`]/[`crate::analysis::RegionId`]
//! and every other cross-module ID.
#![allow(dead_code)]

/// Identifies one compiled automaton -- the whole static transition table
/// for one concurrent assertion's property/sequence tree (16.12-16.13).
/// One per `AnalyzedAssertion` (`vj-codegen::sva`'s frontend-facing
/// sibling queries that type at elaboration time); a later task's builder
/// mints these as it compiles each assertion's tree.
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
pub struct AutomatonId(pub u32);

/// Identifies one state inside a specific [`AutomatonId`]'s transition
/// table. Scoped to its automaton (not globally unique on its own, the same
/// way `BlockId`/`SegId` are scoped to one process's CFG) -- a thread
/// record (not yet defined; owned by the engine, not this IR) pairs this
/// with its `AutomatonId` to name exactly where in exactly which automaton
/// a live thread is.
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
pub struct ThreadStateId(pub u32);

/// Identifies one compiled Boolean leaf (16.6) by its position in whichever
/// leaf table its automaton carries. T5's `vj-codegen::sva::leaf`
/// compiles each leaf to a `PredicateFn` (D8's `compile_iff_guard`
/// convention, reused verbatim per plan §1.2); this ID is how a
/// [`Transition`] names *which* compiled leaf to invoke, without this crate
/// (which has no `sv-lang`/codegen dependency, module doc comment) needing
/// to know anything about how leaves are compiled.
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
pub struct LeafId(pub u32);

/// Identifies one clock of an assertion (16.13, sva T28): the clocking events the
/// builder met, interned by structural equality, so two `@(posedge clk)` written
/// in different places are ONE clock and `@(posedge clk)` / `@(negedge clk)` are
/// two. `ClockId(0)` is the clock the assertion is clocked by (the event its
/// statement or the first clocking event met names): the clock every thread and
/// property starts in, and the only one a single-clock assertion has.
///
/// A [`Transition::Delay`] counts ticks of the clock its thread is in, and
/// [`Transition::ClockSync`] moves the thread to another one; which instants ARE
/// ticks of each clock is a fact about one simulation, handed to the interpreters
/// as a [`crate::sva::trace::Timeline`] (none: every instant is a tick of every
/// clock, the single-clock case).
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, PartialOrd, Ord)]
pub struct ClockId(pub u32);

/// Identifies one scheduled action -- a pass/fail/vacuous-pass report
/// (16.14.1-16.14.4, 17.7.3), a sequence/property coverage increment
/// (16.14.3), or a checker action block -- a later task (T29 onward, per
/// plan §1.4's generalized `MaturationQueue<ReportKind>`) defines the
/// payload each one carries; a [`Transition::Match`] names only *which*
/// actions fire, not what they do.
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
pub struct ActionId(pub u32);

/// Identifies one local-variable slot (16.10's assertion-variable
/// declarations and `local` formal arguments, 16.11's match-item writes) in a
/// thread's per-thread local variable frame. The frame is one slot per id,
/// `0..`[`Automaton::local_vars`]`.len()`, each either unassigned or holding a
/// value of the slot's [`LocalVarDecl`] type; a thread that forks (an `or`
/// branch, a delay window's several end ticks) takes its own COPY of the frame,
/// which is what gives every match thread its own latest assignments (16.10
/// rule (c)). T13 defines the slots and the edges that read/write/copy them;
/// the runtime heap handle that stores a live frame is the engine's (T29), so
/// here a slot is only the name a [`Transition::LocalVarWrite`]/
/// [`Transition::LocalVarCopy`] and a compiled leaf's read refer to.
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, PartialOrd, Ord)]
pub struct LocalVarId(pub u32);

/// The declared type of one local-variable slot: every value stored in the slot
/// is first cast to it (16.10 "the value of a local variable is a value of its
/// declared type"; 16.8.2 "cast to the type of" for an input/inout formal's
/// initial value and for the value written back to an output/inout actual). The
/// builder derives it from the variable's declared integral type; a non-integral
/// local variable is a loud build error, never a slot.
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
pub struct LocalVarDecl {
    /// Width in bits (`>= 1`).
    pub width: u32,
    /// Whether the type is signed: a signed value is sign-extended from its top
    /// bit after truncation, an unsigned one zero-extended.
    pub signed: bool,
}

impl LocalVarDecl {
    /// Whether the variable is wider than one frame slot (`> 64` bits) and so
    /// occupies [`slots`](Self::slots) consecutive frame slots, see
    /// [`Automaton::new_local_var`].
    pub fn is_wide(&self) -> bool {
        self.width > 64
    }

    /// How many 64-bit limbs one plane (value or unknown) of the variable has:
    /// `ceil(width / 64)`, and `1` for a narrow variable.
    pub fn limbs(&self) -> usize {
        (self.width as usize).div_ceil(64).max(1)
    }

    /// How many consecutive frame slots the variable occupies: `1` when it fits
    /// an `i64`, else `2 * limbs()` -- the value limbs (least significant
    /// first), then the unknown-plane limbs (`x`/`z` bits, same order). A wide
    /// variable is four-state; a narrow one is the two-state `i64` it always was.
    pub fn slots(&self) -> usize {
        if self.is_wide() { 2 * self.limbs() } else { 1 }
    }

    /// `value` fitted to this type: truncated to [`width`](Self::width) bits,
    /// then sign-extended when [`signed`](Self::signed). A slot holds an `i64`,
    /// so a type of 64 bits or more is the identity here: a wider variable is
    /// stored limb by limb in several slots ([`slots`](Self::slots), the
    /// helpers of [`crate::sva::wide`] fit it as a whole) and each limb slot is
    /// an ordinary 64-bit unsigned one.
    pub fn cast(&self, value: i64) -> i64 {
        if self.width == 0 || self.width >= 64 {
            return value;
        }
        let shift = 64 - self.width;
        if self.signed {
            (value << shift) >> shift
        } else {
            ((value as u64) << shift >> shift) as i64
        }
    }
}

/// One edge out of a [`ThreadStateId`] in a compiled automaton's static
/// transition table (plan §1.2/§1.4). This is the whole vocabulary a
/// sequence/property tree compiles down to -- every LRM operator (16.7's
/// concatenation, 16.9's `and`/`or`/`intersect`/`throughout`/`within`/
/// `first_match`, 16.12's property connectives, 17's checker actions) is
/// *built from* these shapes by a later task's builder, not added as one of
/// their own (T11's `first_match` markers are the one exception: "earliest
/// match" is a property of a whole evaluation attempt, which no path-local
/// edge can express). Matched exhaustively wherever it is consumed (the first such
/// site, [`Transition::kind_name`] below, exists precisely so a future
/// variant added here without updating every consumer fails to compile,
/// not silently mis-steps at runtime -- ARCHITECTURE §7 item 9's "every
/// kind match shouts" discipline, applied to a workspace-local enum
/// instead of a mirrored slang one).
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
pub enum Transition {
    /// A `##N`/`##[m:n]` cycle delay (16.7) or a `[*n:m]`/`[->n:m]`/
    /// `[=n:m]` repetition unrolled into a run of delay edges (16.9.2):
    /// this edge is only eligible once at least `min` ticks of the clock the
    /// thread is currently in (see [`ClockId`]) have
    /// elapsed since the automaton entered the state it leaves, and must
    /// be taken by `max` ticks (`None` = unbounded, the `$` form) or the
    /// thread never gets another chance to -- the engine (T9/T10) is the
    /// one enforcing that window, not this IR.
    Delay { min: u32, max: Option<u32> },
    /// A same-tick edge: zero elapsed ticks, consumed instantly. Used
    /// unconditionally (a sequence concatenation boundary with a zero-width
    /// operand, 16.9.2.1's empty-match rules, or any other place the
    /// builder needs to join two states with no delay and no condition) --
    /// but also, as of T9, paired with [`Edge::guard`] to model 16.9.1's
    /// Boolean-leaf point-sample itself ("the expression is evaluated...
    /// over 1 clock tick", which costs no ADDITIONAL elapsed time relative
    /// to the clock tick it is sampled on -- the thing that advances time
    /// in a sequence is the `##`/repetition operator *between* samples, not
    /// a sample's own evaluation): see `Edge`'s own doc comment in
    /// `vj-sim::sva::ir` for why.
    Epsilon,
    /// `disable iff`/property abort (16.12.14's `accept_on`/`reject_on`/
    /// `sync_accept_on`/`sync_reject_on`, and 16.6/16.15's plain `disable
    /// iff`): evaluated every simulation time step against current
    /// (unsampled) values per 16.6, not gated on this edge's own clock --
    /// the first tick `leaf` is true, the thread's run is decided per
    /// `mode` without waiting for (or caring about) this edge's own
    /// source/target states.
    Abort { leaf: LeafId, mode: AbortMode },
    /// This thread has reached its automaton's accept state: schedule
    /// `actions` into the Reactive-region maturation queue (plan §1.4's
    /// generalized `MaturationQueue<ReportKind>`, T2) rather than firing
    /// them inline -- matches never fire synchronously with the Observed
    /// step that discovers them (16.4.1-style maturation, generalized).
    Match { actions: Vec<ActionId> },
    /// A sequence match-item write (16.10/16.11): compute `value` (a
    /// compiled leaf, reused verbatim -- 16.11 restricts match-item
    /// expressions to the same side-effect-free leaf shape 16.6 does,
    /// T5's validation pass), cast it to `var`'s declared type
    /// ([`LocalVarDecl::cast`]) and store it into `var`'s slot of the thread's
    /// frame before taking this edge. A compound assignment (`v += e`) is the
    /// same edge: its `value` leaf is the whole `v + e`, which reads `v`'s own
    /// slot (T13).
    LocalVarWrite { var: LocalVarId, value: LeafId },
    /// A same-tick slot-to-slot copy (T13): `dst` takes `src`'s value, cast to
    /// `dst`'s declared type, or becomes UNASSIGNED when `src` is. The edge
    /// exists for the two places 16.8.2/16.9 need a value to move between
    /// threads' views of a variable without a leaf to compute it:
    ///
    /// - an `inout`/`output` `local` formal argument, whose value is written back
    ///   to the actual's local variable when the instance's match completes
    ///   (16.8.2);
    /// - the branching operators `and`/`intersect` (and their `throughout`/
    ///   `within` rewrites), whose second operand works on a SHADOW copy of every
    ///   variable the first operand touches, copied in before the operands start
    ///   and copied out afterwards for the variables that flow out only of the
    ///   second operand (16.10, F.5.4). The two operands of the lockstep product
    ///   share one frame, so without the shadow one operand's write would be
    ///   visible to the other.
    LocalVarCopy { dst: LocalVarId, src: LocalVarId },
    /// Start of a `first_match(R)` region (16.9.3, T11): zero elapsed ticks,
    /// like [`Epsilon`](Transition::Epsilon), but the thread taking it is
    /// stamped with `(group, current tick)` -- the tick `R` begins on.
    ///
    /// `first_match(R)` keeps only `R`'s matches that END EARLIEST for a
    /// given beginning (Annex F.5.2: `w |= first_match(R)` iff `w |= R` and no
    /// proper prefix of `w` satisfies `R`). Whether a match is the earliest
    /// is a fact about EVERY thread of the region, not about one path, so it
    /// is decided against an attempt-wide table the engine keeps, keyed
    /// `(group, begin tick)` -- see [`FirstMatchEnd`](Transition::FirstMatchEnd).
    /// Nested and repeated regions carry one stamp each (every `first_match`
    /// in a tree has its own [`FirstMatchId`], so stamps never collide).
    FirstMatchBegin { group: FirstMatchId },
    /// End of a `first_match(R)` region: a thread reaching this edge has just
    /// produced a match of `R` that ended on the current tick. The engine
    /// looks `(group, the tick this thread's `group` stamp holds)` up in the
    /// attempt's first-match table:
    ///
    /// - absent: record the current tick as the earliest end, and take the
    ///   edge;
    /// - present and equal to the current tick: take the edge (several
    ///   matches may end on that same earliest tick, and all of them are
    ///   matches of `first_match(R)`);
    /// - present and EARLIER: the thread dies (a shorter match of `R`, from
    ///   the same beginning, already exists).
    ///
    /// The entry is recorded whether or not the thread's continuation later
    /// succeeds: `first_match(R) ##1 c` discards the longer `R` matches even
    /// when the earliest one is followed by `!c`. Threads are stepped in tick
    /// order, so an earlier end tick is always seen before a later one.
    /// Taking this edge also drops the thread's `group` stamp.
    FirstMatchEnd { group: FirstMatchId },
    /// A sequence match-item increment/decrement (16.11, T14): `var` becomes
    /// `var + delta` (`delta` is `+1` for `x++`/`++x`, `-1` for `x--`/`--x`),
    /// cast to `var`'s declared type. It is a dedicated edge rather than a
    /// [`LocalVarWrite`](Transition::LocalVarWrite) because the new value is a
    /// function of the variable alone: no compiled leaf is needed to compute
    /// it. A match item's value is never observed (the statement form of
    /// `x++` discards it), so pre- and post-forms are the same edge.
    ///
    /// The variable must hold a value (16.10: an inc/dec reads it); the
    /// builder rejects every proof-of-unassigned and the interpreter fails the
    /// attempt with `UnassignedRead` for one it could not.
    LocalVarStep { var: LocalVarId, delta: i64 },
    /// A sequence match-item subroutine call (16.11, T14): at every nonempty
    /// end point of the sequence it is attached to, task or void function
    /// `call` is scheduled in the Reactive region (fire-and-forget: assertion
    /// evaluation neither waits on it nor receives anything back, and it runs
    /// even when a sequence this one is part of later fails). `args` is one
    /// entry per actual argument, in the formal order.
    ///
    /// The edge is a same-tick, unguarded pass-through for the thread; its
    /// only effect is the call event the engine (T29) schedules. By-value
    /// arguments are the SAMPLED value of their leaf under the thread's frame
    /// (consistent with the match that produced it); by-reference arguments
    /// are the actual itself, bound at call time. See [`CallArg`].
    SubroutineCall { call: CallId, args: Vec<CallArg> },
    /// The end point of another sequence instance (16.9.11, 16.13.5, 16.13.6): the
    /// value of `inst.triggered` / `inst.matched` for the instance
    /// [`Automaton::end_points`]`[point]`.
    ///
    /// The instance is evaluated INDEPENDENTLY of the thread that tests it: its
    /// automaton runs free, one attempt from every tick of its clock ("the result
    /// ... does not depend upon the starting point of the match of its operand
    /// sequence"), and the instance has reached its end point on a tick when some
    /// attempt has a NONEMPTY match ending there (16.9.11: an empty match never
    /// activates the method). The runtime sets that status in the Observed region
    /// and it persists for the rest of the time step, so a thread reads a status
    /// that already includes the tick it is on. The edge takes no time.
    ///
    /// - `flag == None`: the edge is a guard. A thread takes it only when the
    ///   instance reached its end point, and forks once per DISTINCT frame an
    ///   attempt matched with (16.10: "the thread evaluating the instance to which
    ///   triggered is applied will fork"), copying the matching frame's
    ///   [`EndPoint::flow_out`] slots into its own. This is the application of the
    ///   method as a whole maximal Boolean expression, the only one a local
    ///   variable flows out of.
    /// - `flag == Some(slot)`: the application sits inside a larger expression
    ///   (`!s.triggered`, `a && s.triggered`), so nothing flows out. The edge is
    ///   not a guard: it stores `1`/`0` (the instance did / did not reach its end
    ///   point on this tick) into the thread's frame slot `flag`, and the leaf that
    ///   holds the expression reads the slot where the application stands (a leaf
    ///   reads its flags in the pre-order of the calls inside it, see the builder's
    ///   `LeafLocals::end_flags`).
    ///
    /// For [`EndMethod::Matched`] the status is the instance's own clock's, held
    /// until the first tick of THIS automaton's clock at or after the match: see
    /// [`EndMethod`].
    EndPoint {
        point: EndPointId,
        flag: Option<LocalVarId>,
    },
    /// The clock change of a multiclocked sequence (16.13.1, sva T28): `s1 ##1 s2`
    /// (`strict`) or `s1 ##0 s2` (not `strict`) where `s1` ends in one clock and
    /// `s2` begins in another. The thread leaves the clock it is in and takes
    /// `to`:
    ///
    /// - `strict` (`##1`): "the nearest strictly subsequent tick" of `to` -- the
    ///   first tick of `to` AFTER the instant the thread is at, even when the old
    ///   clock's tick is also one of `to`'s;
    /// - not `strict` (`##0`): "the nearest possibly overlapping tick": the first
    ///   tick of `to` AT OR AFTER that instant, so no time passes when the two
    ///   clocks tick together.
    ///
    /// A fused edge pair would need the single-clock meaning of `Delay{1,1}` to
    /// be "one instant later", which only holds when every instant is a tick;
    /// this edge is that statement made for the clocks involved. With no
    /// timeline (every instant a tick of every clock) it is a `Delay{1,1}` /
    /// `Epsilon`. The sequences either side must not admit the empty match
    /// (16.13.1: "a maximal singly clocked subsequence ... shall admit only
    /// nonempty matches"), which the builder checks.
    ClockSync { to: ClockId, strict: bool },
}

/// Identifies one sequence instance whose end point an automaton tests, in its
/// [`Automaton::end_points`] table. Scoped to its automaton, like
/// [`ThreadStateId`].
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, PartialOrd, Ord)]
pub struct EndPointId(pub u32);

/// Which end-point method a [`Transition::EndPoint`] applies.
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
pub enum EndMethod {
    /// `.triggered` (16.9.11, 16.13.6): the instance's ending clock is the clock
    /// of the context the method appears in (the builder rejects any other), so
    /// the status is read on the same tick it is set.
    Triggered,
    /// `.matched` (16.13.5): the instance may run on another clock. Its status is
    /// SET at the instance's own end point and persists until the Observed region
    /// following the first tick of the testing clock after the match, so a
    /// testing tick sees every match since the previous testing tick, up to and
    /// including a match at the very time of the tick (a one-slot handoff
    /// between the two clock domains).
    Matched,
}

/// One sequence instance whose end point an automaton tests (see
/// [`Transition::EndPoint`]).
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct EndPoint {
    pub method: EndMethod,
    /// Which end-point application of the whole assertion this is, numbered by the
    /// builder across ALL nesting levels (the instance of an end point may itself
    /// test others), so a site keeps one identity however deep it sits: the key of
    /// the builder's per-site table (the instance expression and the clock it ends
    /// on, which the engine needs and this IR does not carry).
    pub site: u32,
    /// The instance's own automaton: built with NO local variable flowing in
    /// (16.10: a formal the instance reads must be assigned in the instance
    /// first), so every attempt starts with an all-unassigned frame. Its
    /// `local_vars` begin with the enclosing automaton's, so a slot id means the
    /// same variable in both.
    pub automaton: Automaton,
    /// `(slot in the instance's frame, slot in the testing thread's frame)` for
    /// every local variable that flows out of the maximal application of the
    /// method (see [`Transition::EndPoint`]); empty for the flag form.
    pub flow_out: Vec<(LocalVarId, LocalVarId)>,
}

/// Identifies one subroutine call site attached as a match item, in its
/// automaton's call table (a table the builder keeps next to the leaf table:
/// this IR knows only the handle, the runtime engine (T29) resolves it to the
/// task or void function to invoke).
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, PartialOrd, Ord)]
pub struct CallId(pub u32);

/// One actual argument of a [`Transition::SubroutineCall`] (16.11).
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
pub enum CallArg {
    /// A by-value (`input`) argument: the leaf's value, sampled at the end
    /// point. Every actual that mentions a local variable is by value
    /// (16.11: "a local variable cannot be passed by reference").
    Value(LeafId),
    /// A `ref`/`const ref` argument: the actual is an lvalue of the enclosing
    /// scope, bound to the formal at call time with no copy. The engine
    /// resolves the lvalue from the call table.
    Ref,
    /// A by-value argument that depends on nothing sampled and so has no leaf:
    /// a string literal or a constant of a type a leaf cannot carry (a real, a
    /// string). The kernel that runs the call lowers the actual itself; the
    /// event carries no value for it (`None`).
    Const,
}

/// Identifies one `first_match` region (16.9.3) inside its automaton: the key
/// the engine's first-match table is indexed by, together with the tick the
/// region began on. Minted by [`Automaton::new_first_match_group`]; every
/// `first_match` operator in an assertion (and every copy of it a repetition
/// unrolls into) has its own.
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, PartialOrd, Ord)]
pub struct FirstMatchId(pub u32);

impl Transition {
    /// A stable, short name per variant -- this enum's first exhaustive
    /// match site (module doc comment: no real consumer exists yet, so
    /// this is what keeps the "no wildcard arm" discipline load-bearing
    /// today instead of unchecked).
    pub fn kind_name(&self) -> &'static str {
        match self {
            Transition::Delay { .. } => "Delay",
            Transition::Epsilon => "Epsilon",
            Transition::Abort { .. } => "Abort",
            Transition::Match { .. } => "Match",
            Transition::LocalVarWrite { .. } => "LocalVarWrite",
            Transition::LocalVarCopy { .. } => "LocalVarCopy",
            Transition::FirstMatchBegin { .. } => "FirstMatchBegin",
            Transition::FirstMatchEnd { .. } => "FirstMatchEnd",
            Transition::LocalVarStep { .. } => "LocalVarStep",
            Transition::SubroutineCall { .. } => "SubroutineCall",
            Transition::EndPoint { .. } => "EndPoint",
            Transition::ClockSync { .. } => "ClockSync",
        }
    }
}

/// The four abort/accept actions 16.12.14 defines, as a cross product of
/// *direction* (does the thread succeed or fail when the condition fires)
/// and *synchronization* (does the abort happen as soon as the condition
/// is true mid-cycle ("asynchronous"), or only at the next clock tick
/// ("synchronous") -- the LRM's own `isSync` flag, `AbortAssertionExpr`
/// in `sv-lang-sys`'s vendored `AssertionExpr.h`, module doc comment of
/// `vj-codegen::sva::op`):
///
/// | | asynchronous | synchronous |
/// |---|---|---|
/// | accept | `accept_on` -> [`Accept`](AbortMode::Accept) | `sync_accept_on` -> [`SyncAccept`](AbortMode::SyncAccept) |
/// | reject | `reject_on` -> [`Reject`](AbortMode::Reject) | `sync_reject_on` -> [`SyncReject`](AbortMode::SyncReject) |
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
pub enum AbortMode {
    Accept,
    Reject,
    SyncAccept,
    SyncReject,
}

impl AbortMode {
    /// The number of variants (4, the full 16.12.14 cross product above).
    pub const COUNT: usize = 4;
    /// Every variant.
    pub const ALL: [AbortMode; Self::COUNT] = [
        AbortMode::Accept,
        AbortMode::Reject,
        AbortMode::SyncAccept,
        AbortMode::SyncReject,
    ];

    /// `true` for the `sync_*_on` forms (16.12.14: the abort is deferred to
    /// the next clock tick rather than applied as soon as the condition is
    /// true mid-cycle).
    pub fn is_sync(&self) -> bool {
        matches!(self, AbortMode::SyncAccept | AbortMode::SyncReject)
    }

    /// `true` if a true condition makes the thread succeed (`accept_on`/
    /// `sync_accept_on`); `false` if it makes the thread fail (`reject_on`/
    /// `sync_reject_on`).
    pub fn accepts(&self) -> bool {
        matches!(self, AbortMode::Accept | AbortMode::SyncAccept)
    }
}

/// One edge out of a [`ThreadStateId`] in a compiled [`Automaton`]: the
/// condition/action it carries ([`Transition`]) plus the state it leads to.
///
/// T9 (`docs/superpowers/plans/2026-10-03-sva.md`) adds this type (and
/// [`State`]/[`Automaton`] below) -- T4's own skeleton defined
/// [`Transition`]'s five label shapes but, by its own module doc comment
/// ("no lowering yet"), never wired a `target` state onto any of them, so
/// there was no way yet to connect two states into an actual graph. T9 is
/// the first task that builds a real automaton, so it is the one that
/// completes the IR with the missing graph structure.
///
/// **`guard`, a deliberate, documented addition beyond the plan's literal
/// text.** Plan §1.2 says a Boolean leaf (16.6) is evaluated by the engine
/// and "the automaton engine calls these compiled leaves" -- but it never
/// says *which* edge a leaf's truth value gates, and [`Transition`] itself
/// has no `LeafId` field on its `Delay`/`Epsilon`/`Match` variants (only
/// `Abort`/`LocalVarWrite` carry one, and for a different purpose: an abort
/// condition and a match-item's write value, neither of which is "the
/// per-tick Boolean this edge requires to be taken"). Without a place to put
/// that leaf reference, nothing in the IR could represent even the simplest
/// legal sequence, `a` (16.9.1: a lone Boolean expression as a sequence
/// matches over exactly one tick, true -> match, false -> no match) --
/// there is no way to say "this edge may be taken on a tick only if `a`
/// evaluates true" using `Transition` alone. `Edge::guard` closes that gap
/// at the EDGE level (not a sixth `Transition` variant, preserving T4's own
/// "every LRM operator is built from these five shapes... not a sixth"
/// design intent): `guard = Some(leaf)` means this edge is eligible only on
/// a tick where `leaf` evaluates true; `guard = None` means the edge's own
/// `label` is the only eligibility condition (a pure elapsed-tick window for
/// `Delay`, or unconditional for `Epsilon`/`Match`).
///
/// Two combinations matter in practice (both built by
/// `vj-codegen::sva::build`, T9):
/// - `guard = Some(leaf)` + `label = Epsilon`: 16.9.1's Boolean-leaf
///   point-sample -- "this tick, `leaf` must evaluate true", costing zero
///   ADDITIONAL elapsed ticks beyond the one it is sampled on (the thing
///   that advances a sequence's clock is a `##`/repetition operator
///   *between* samples, never a sample's own evaluation -- confirmed
///   against the well-known identity `a[*3]` spans exactly 2 ticks, i to
///   i+2, not 3, which only holds if a bare leaf's own cost is zero).
/// - `guard = None` + `label = Delay { min, max }`: the elapsed-tick window
///   a `##min:max` cycle delay (16.7) or an inter-repetition link (16.9.2's
///   implicit `##1` between consecutive repeats, or a wider search window
///   for `[->]`/`[=]`'s nonconsecutive/goto repeats) imposes between two
///   samples.
///
/// A guard has no polarity of its own: the gap of a goto/nonconsecutive
/// repetition (16.9.2, `b[->n]` == `(!b[*0:$] ##1 b)[*n]`) is guarded by a
/// SEPARATE leaf standing for the expression `!b`, which the builder marks
/// negated in its leaf table (`LeafTable::is_negated`). The negation must live
/// in the leaf, not on the edge, because it is a 4-state operator: `!x` is `x`,
/// which a Boolean context collapses to false, so `!b` holds only where `b` is
/// KNOWN false -- not wherever `b` fails to hold, which an edge flag over a
/// leaf already collapsed to a bool could not tell apart.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Edge {
    pub guard: Option<LeafId>,
    pub label: Transition,
    pub target: ThreadStateId,
}

/// One state's outgoing edges -- a row of the automaton's static transition
/// table (plan §1.2). A state with at least one `Transition::Match` edge
/// among its `edges` is an accepting state (per [`Transition::Match`]'s own
/// doc comment: reaching one schedules a pass/fail/cover report); this is a
/// derived property (see [`State::is_accepting`]), not a separate flag, so
/// it can never drift out of sync with the edges actually present.
#[derive(Clone, Debug, Default, PartialEq, Eq)]
pub struct State {
    pub edges: Vec<Edge>,
}

impl State {
    /// `true` if any of this state's edges is a [`Transition::Match`] --
    /// see the struct doc comment.
    pub fn is_accepting(&self) -> bool {
        self.edges
            .iter()
            .any(|e| matches!(e.label, Transition::Match { .. }))
    }
}

/// A compiled automaton (plan §1.2's "a dedicated, interpreted automaton per
/// assertion, compiled once at elaboration time into a static transition
/// table") -- one sequence/property tree's whole static shape, addressed by
/// [`ThreadStateId`] (an index into `states`), plus which state a freshly
/// spawned thread starts in. Pure data, no `sv-lang` dependency (this
/// module's own doc comment), so it is equally usable by
/// `vj-codegen::sva::build` (which constructs one from an `AssertionExpr`
/// tree, under the `frontend` feature) and by the eventual
/// `vj-runtime::sva_engine` (which only ever interprets an already-built
/// one, with `vj-sim`'s `frontend` feature off, per this crate's own
/// `default-features = false` contract with `vj-runtime`).
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Automaton {
    pub states: Vec<State>,
    pub start: ThreadStateId,
    /// `true` when the sequence this automaton was built from admits the
    /// EMPTY match (16.9.2.1: a match spanning zero clock ticks, e.g.
    /// `a[*0]`, `a[*0:2]`). The empty match is not a path through `states`
    /// (a path always consumes at least the tick it starts on), so it cannot
    /// be an accepting state; this flag carries it separately. A sequence
    /// that admits the empty match and nothing else can never match when used
    /// as a property (16.9.2.1 "a sequence that admits only an empty match
    /// cannot be used as a property"); one that admits both matches on its
    /// non-empty paths only -- consumers decide how to treat the empty match
    /// (T10 only records it; the property layers that care are T19+).
    pub admits_empty: bool,
    /// How many [`FirstMatchId`]s this automaton uses (`0..first_match_groups`):
    /// the size of the per-attempt first-match table the engine allocates
    /// (keyed by group and begin tick, see [`Transition::FirstMatchBegin`]).
    pub first_match_groups: u32,
    /// The local-variable slots (`LocalVarId(i)` is `local_vars[i]`): the size
    /// and element types of the per-thread frame the engine allocates, see
    /// [`LocalVarId`]. Every slot of every instance expansion has its own entry
    /// (a slot is never reused for a different variable), so the frame is as
    /// wide as the assertion's total number of local-variable declarations plus
    /// the and/intersect shadows.
    pub local_vars: Vec<LocalVarDecl>,
    /// The sequence instances whose end points this automaton tests
    /// (`EndPointId(i)` is `end_points[i]`), each a whole automaton of its own.
    pub end_points: Vec<EndPoint>,
    /// The clock a thread is in at [`Automaton::start`] (sva T28): the clock of the
    /// sequence's first Boolean operand. [`ClockId`]`(0)` unless the sequence opens
    /// with a clocking event of its own that is not the assertion's.
    pub entry_clock: ClockId,
}

impl Automaton {
    /// An automaton with one (unreachable until wired) state and no edges --
    /// the empty table a builder starts folding states/edges into.
    pub fn empty() -> Self {
        let mut a = Automaton {
            states: Vec::new(),
            start: ThreadStateId(0),
            admits_empty: false,
            first_match_groups: 0,
            local_vars: Vec::new(),
            end_points: Vec::new(),
            entry_clock: ClockId(0),
        };
        let s = a.new_state();
        a.start = s;
        a
    }

    /// Mints the next local variable, of the given integral type, and returns its
    /// (head) slot. A variable wider than 64 bits gets [`LocalVarDecl::slots`]
    /// consecutive slots: the head carries the declared type and value limb 0, the
    /// rest are plain 64-bit unsigned limb slots (value limbs 1.., then the
    /// unknown limbs), so everything that names a variable by its head slot
    /// (reads, copies, steps) reaches the others by position.
    pub fn new_local_var(&mut self, width: u32, signed: bool) -> LocalVarId {
        let id = LocalVarId(self.local_vars.len() as u32);
        let decl = LocalVarDecl { width, signed };
        self.local_vars.push(decl);
        for _ in 1..decl.slots() {
            self.local_vars.push(LocalVarDecl {
                width: 64,
                signed: false,
            });
        }
        id
    }

    /// Borrows `id`'s declared type. `id` must be a slot this automaton minted
    /// (see [`Automaton::add_edge`]'s identical note).
    pub fn local_var(&self, id: LocalVarId) -> &LocalVarDecl {
        &self.local_vars[id.0 as usize]
    }

    /// Registers a sequence instance whose end point this automaton tests.
    pub fn new_end_point(&mut self, point: EndPoint) -> EndPointId {
        let id = EndPointId(self.end_points.len() as u32);
        self.end_points.push(point);
        id
    }

    /// Borrows `id`'s instance (an id this automaton minted, like
    /// [`Automaton::local_var`]).
    pub fn end_point(&self, id: EndPointId) -> &EndPoint {
        &self.end_points[id.0 as usize]
    }

    /// Mints the next [`FirstMatchId`] (one per `first_match` region).
    pub fn new_first_match_group(&mut self) -> FirstMatchId {
        let id = FirstMatchId(self.first_match_groups);
        self.first_match_groups += 1;
        id
    }

    /// Allocates a fresh state with no outgoing edges and returns its id.
    pub fn new_state(&mut self) -> ThreadStateId {
        let id = ThreadStateId(self.states.len() as u32);
        self.states.push(State::default());
        id
    }

    /// Appends one edge to `from`'s row. `from` must be a state this same
    /// `Automaton` has already allocated (via [`Automaton::new_state`]) --
    /// out-of-range ids panic (a builder-internal invariant, never reachable
    /// from untrusted input: every `ThreadStateId` this crate's builder ever
    /// hands to this method came from this same `Automaton`'s own
    /// `new_state`, per the one caller that exists today,
    /// `vj-codegen::sva::build`).
    pub fn add_edge(
        &mut self,
        from: ThreadStateId,
        guard: Option<LeafId>,
        label: Transition,
        target: ThreadStateId,
    ) {
        self.states[from.0 as usize].edges.push(Edge {
            guard,
            label,
            target,
        });
    }

    /// Borrows `id`'s row.
    pub fn state(&self, id: ThreadStateId) -> &State {
        &self.states[id.0 as usize]
    }

    /// An upper bound on how many clock ticks past its start tick any match of
    /// this automaton can end: the sum of every delay edge's upper bound (a simple
    /// path takes each edge at most once, and a repetition is already unrolled into
    /// delay edges), or `None` when some delay is unbounded (`##[1:$]`, `[*]`) or a
    /// [`Transition::ClockSync`] / end-point edge makes the span a function of
    /// another clock. A cover-sequence attempt (16.14.3) that has run this long has
    /// reported every match it ever will.
    pub fn max_span(&self) -> Option<u32> {
        // A loop through a delay edge (the unbounded repetition `s[*lo:$]` is a
        // loop of delay-1 edges) takes that edge any number of times: the sum
        // below would count it once and retire the attempt while it can still
        // match.
        for (u, state) in self.states.iter().enumerate() {
            for edge in &state.edges {
                let Transition::Delay { min, max } = &edge.label else {
                    continue;
                };
                if (*max).unwrap_or(u32::MAX).max(*min) == 0 {
                    continue;
                }
                let mut seen = vec![false; self.states.len()];
                let mut stack = vec![edge.target.0 as usize];
                while let Some(s) = stack.pop() {
                    if s == u {
                        return None;
                    }
                    if std::mem::replace(&mut seen[s], true) {
                        continue;
                    }
                    stack.extend(self.states[s].edges.iter().map(|e| e.target.0 as usize));
                }
            }
        }
        let mut total: u32 = 0;
        for edge in self.states.iter().flat_map(|s| &s.edges) {
            match &edge.label {
                Transition::Delay { min, max } => {
                    total = total.checked_add((*max)?.max(*min))?;
                }
                Transition::ClockSync { .. } => return None,
                // The instance runs free on its own; the testing thread only
                // reads its status, in no time (see [`Automaton::end_point_lookback`]).
                Transition::EndPoint { .. }
                | Transition::Epsilon
                | Transition::Abort { .. }
                | Transition::Match { .. }
                | Transition::LocalVarWrite { .. }
                | Transition::LocalVarCopy { .. }
                | Transition::FirstMatchBegin { .. }
                | Transition::FirstMatchEnd { .. }
                | Transition::LocalVarStep { .. }
                | Transition::SubroutineCall { .. } => {}
            }
        }
        Some(total)
    }

    /// For every sequence instance this automaton (or an instance of it) tests:
    /// its clock, and how many of that clock's ticks before a testing thread's
    /// position an attempt of it may have started and still end there (`None`
    /// for an instance with no bounded span, an unbounded repetition: its status
    /// needs every past start).
    pub fn end_point_lookback(&self) -> Vec<(ClockId, Option<u32>)> {
        let mut out = Vec::new();
        for ep in &self.end_points {
            let inner = ep.automaton.end_point_lookback();
            let deepest = inner.iter().try_fold(0u32, |m, (_, n)| n.map(|n| m.max(n)));
            let span = ep
                .automaton
                .max_span()
                .zip(deepest)
                .and_then(|(own, d)| own.checked_add(d));
            out.push((ep.automaton.entry_clock, span));
            out.extend(inner);
        }
        out
    }

    /// Whether any edge of this automaton (not of its end-point instances, see
    /// [`Automaton::end_points_have_calls`]) attaches a subroutine call (16.11).
    pub fn has_calls(&self) -> bool {
        self.states
            .iter()
            .flat_map(|s| &s.edges)
            .any(|e| matches!(e.label, Transition::SubroutineCall { .. }))
    }

    /// Whether a sequence instance an end-point method tests (at any depth)
    /// attaches a subroutine call.
    pub fn end_points_have_calls(&self) -> bool {
        self.end_points
            .iter()
            .any(|p| p.automaton.has_calls() || p.automaton.end_points_have_calls())
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn transition_kind_name_covers_every_variant() {
        assert_eq!(Transition::Delay { min: 0, max: None }.kind_name(), "Delay");
        assert_eq!(Transition::Epsilon.kind_name(), "Epsilon");
        assert_eq!(
            Transition::Abort {
                leaf: LeafId(0),
                mode: AbortMode::Accept
            }
            .kind_name(),
            "Abort"
        );
        assert_eq!(Transition::Match { actions: vec![] }.kind_name(), "Match");
        assert_eq!(
            Transition::LocalVarWrite {
                var: LocalVarId(0),
                value: LeafId(0)
            }
            .kind_name(),
            "LocalVarWrite"
        );
        assert_eq!(
            Transition::FirstMatchBegin {
                group: FirstMatchId(0)
            }
            .kind_name(),
            "FirstMatchBegin"
        );
        assert_eq!(
            Transition::FirstMatchEnd {
                group: FirstMatchId(0)
            }
            .kind_name(),
            "FirstMatchEnd"
        );
        assert_eq!(
            Transition::ClockSync {
                to: ClockId(1),
                strict: true
            }
            .kind_name(),
            "ClockSync"
        );
    }

    /// T28: clocks are small ordered handles, and a fresh automaton starts in the
    /// assertion's own clock.
    #[test]
    fn clock_ids_order_and_default_to_the_assertion_clock() {
        assert!(ClockId(0) < ClockId(1));
        assert_eq!(Automaton::empty().entry_clock, ClockId(0));
    }

    /// T14: the two match-item edges have their own names, and a call's
    /// arguments are by-value leaves or by-reference markers.
    #[test]
    fn match_item_edges_have_their_own_kind_names() {
        assert_eq!(
            Transition::LocalVarStep {
                var: LocalVarId(0),
                delta: 1
            }
            .kind_name(),
            "LocalVarStep"
        );
        let call = Transition::SubroutineCall {
            call: CallId(3),
            args: vec![CallArg::Value(LeafId(1)), CallArg::Ref, CallArg::Const],
        };
        assert_eq!(call.kind_name(), "SubroutineCall");
        assert_ne!(CallArg::Value(LeafId(0)), CallArg::Ref);
        assert_ne!(CallArg::Const, CallArg::Ref);
        assert!(CallId(1) < CallId(2));
    }

    /// 16.11: `has_calls` sees a call edge of the automaton itself and, apart,
    /// one hidden in a sequence instance an end-point method tests.
    #[test]
    fn call_edges_are_found_on_the_automaton_and_in_its_end_points() {
        let call = || Transition::SubroutineCall {
            call: CallId(0),
            args: vec![],
        };
        let mut plain = Automaton::empty();
        let s1 = plain.new_state();
        plain.add_edge(plain.start, None, Transition::Epsilon, s1);
        assert!(!plain.has_calls() && !plain.end_points_have_calls());

        let mut direct = plain.clone();
        direct.add_edge(s1, None, call(), s1);
        assert!(direct.has_calls() && !direct.end_points_have_calls());

        let mut inner = plain.clone();
        let s2 = inner.new_state();
        inner.add_edge(s1, None, call(), s2);
        let mut outer = plain.clone();
        outer.new_end_point(EndPoint {
            method: EndMethod::Triggered,
            site: 0,
            automaton: inner,
            flow_out: Vec::new(),
        });
        assert!(!outer.has_calls());
        assert!(outer.end_points_have_calls());
    }

    /// T15: end points are minted densely from 0, each carrying its own
    /// automaton, and the edge that tests one has its own kind name.
    #[test]
    fn end_points_are_minted_densely_and_have_a_kind_name() {
        let mut a = Automaton::empty();
        assert!(a.end_points.is_empty());
        let sub = Automaton::empty();
        let p0 = a.new_end_point(EndPoint {
            method: EndMethod::Triggered,
            site: 0,
            automaton: sub.clone(),
            flow_out: Vec::new(),
        });
        let p1 = a.new_end_point(EndPoint {
            method: EndMethod::Matched,
            site: 1,
            automaton: sub,
            flow_out: vec![(LocalVarId(0), LocalVarId(1))],
        });
        assert_eq!((p0, p1), (EndPointId(0), EndPointId(1)));
        assert_eq!(a.end_point(p0).method, EndMethod::Triggered);
        assert_eq!(a.end_point(p1).method, EndMethod::Matched);
        assert_eq!(a.end_point(p1).flow_out, [(LocalVarId(0), LocalVarId(1))]);
        assert!(p0 < p1);
        let edge = Transition::EndPoint {
            point: p0,
            flag: Some(LocalVarId(2)),
        };
        assert_eq!(edge.kind_name(), "EndPoint");
        assert_ne!(
            edge,
            Transition::EndPoint {
                point: p0,
                flag: None
            }
        );
    }

    #[test]
    fn local_var_copy_has_its_own_kind_name() {
        assert_eq!(
            Transition::LocalVarCopy {
                dst: LocalVarId(1),
                src: LocalVarId(0)
            }
            .kind_name(),
            "LocalVarCopy"
        );
    }

    /// T13: local-variable slots are minted densely from 0 and carry the
    /// declared type the engine casts every write to (16.10: the value of a
    /// local variable is always a value of its declared type).
    #[test]
    fn local_vars_are_minted_densely_with_their_declared_type() {
        let mut a = Automaton::empty();
        assert!(a.local_vars.is_empty());
        let x = a.new_local_var(32, true);
        let y = a.new_local_var(4, false);
        assert_eq!((x, y), (LocalVarId(0), LocalVarId(1)));
        assert_eq!(
            a.local_var(x),
            &LocalVarDecl {
                width: 32,
                signed: true
            }
        );
        assert_eq!(
            a.local_var(y),
            &LocalVarDecl {
                width: 4,
                signed: false
            }
        );
        assert!(LocalVarId(0) < LocalVarId(1));
    }

    /// T13: [`LocalVarDecl::cast`] is the one place a value is fitted to a
    /// local variable's type: truncate to the width, then sign-extend for a
    /// signed type -- exactly SystemVerilog's integral cast.
    #[test]
    fn local_var_decl_cast_truncates_then_extends() {
        let u4 = LocalVarDecl {
            width: 4,
            signed: false,
        };
        assert_eq!(u4.cast(0x1f), 0xf, "unsigned keeps the low bits");
        assert_eq!(u4.cast(-1), 0xf, "a negative value wraps");
        let s4 = LocalVarDecl {
            width: 4,
            signed: true,
        };
        assert_eq!(s4.cast(0xf), -1, "bit 3 set sign-extends");
        assert_eq!(s4.cast(0x7), 7);
        assert_eq!(s4.cast(0x18), -8, "0x18 truncates to 0x8, which is -8");
        let i32d = LocalVarDecl {
            width: 32,
            signed: true,
        };
        assert_eq!(i32d.cast(1 << 31), i64::from(i32::MIN));
        assert_eq!(i32d.cast(-5), -5);
        let u1 = LocalVarDecl {
            width: 1,
            signed: false,
        };
        assert_eq!((u1.cast(2), u1.cast(3)), (0, 1));
        // 64 bits and wider (the interpreter's value is an i64) are unchanged.
        let w64 = LocalVarDecl {
            width: 64,
            signed: false,
        };
        assert_eq!(w64.cast(-1), -1);
        let w128 = LocalVarDecl {
            width: 128,
            signed: true,
        };
        assert_eq!(w128.cast(i64::MIN), i64::MIN);
    }

    /// T11: first-match groups are minted densely from 0, and the count is
    /// what the engine sizes its per-attempt table by.
    #[test]
    fn first_match_groups_are_minted_densely() {
        let mut a = Automaton::empty();
        assert_eq!(a.first_match_groups, 0);
        assert_eq!(a.new_first_match_group(), FirstMatchId(0));
        assert_eq!(a.new_first_match_group(), FirstMatchId(1));
        assert_eq!(a.first_match_groups, 2);
        assert!(FirstMatchId(0) < FirstMatchId(1));
    }

    #[test]
    fn abort_mode_arity_and_16_12_14_cross_product() {
        assert_eq!(AbortMode::ALL.len(), AbortMode::COUNT);
        // accept_on: async, accepts.
        assert!(!AbortMode::Accept.is_sync());
        assert!(AbortMode::Accept.accepts());
        // reject_on: async, rejects.
        assert!(!AbortMode::Reject.is_sync());
        assert!(!AbortMode::Reject.accepts());
        // sync_accept_on: sync, accepts.
        assert!(AbortMode::SyncAccept.is_sync());
        assert!(AbortMode::SyncAccept.accepts());
        // sync_reject_on: sync, rejects.
        assert!(AbortMode::SyncReject.is_sync());
        assert!(!AbortMode::SyncReject.accepts());
    }

    #[test]
    fn ids_are_distinct_and_hashable() {
        use std::collections::HashSet;
        let mut set = HashSet::new();
        for i in 0..4u32 {
            assert!(set.insert(AutomatonId(i)));
        }
        assert_ne!(ThreadStateId(0), ThreadStateId(1));
        assert_ne!(LeafId(0), LeafId(1));
        assert_ne!(ActionId(0), ActionId(1));
        assert_ne!(LocalVarId(0), LocalVarId(1));
    }

    /// T9: [`Automaton::empty`]/`new_state`/`add_edge` wire up a real graph,
    /// and [`State::is_accepting`] tracks exactly the states with a `Match`
    /// edge, no more and no less.
    #[test]
    fn automaton_wiring_and_is_accepting() {
        let mut a = Automaton::empty();
        assert!(
            !a.admits_empty,
            "a fresh automaton admits no empty match until a builder says so"
        );
        let start = a.start;
        let mid = a.new_state();
        let accept = a.new_state();
        a.add_edge(start, Some(LeafId(0)), Transition::Epsilon, mid);
        assert!(
            !a.state(start).is_accepting(),
            "start has only a guarded Epsilon edge, no Match edge yet"
        );
        a.add_edge(mid, None, Transition::Match { actions: vec![] }, accept);
        assert!(
            a.state(mid).is_accepting(),
            "mid now has a Match edge among its others"
        );
        assert!(
            !a.state(accept).is_accepting(),
            "accept itself has no outgoing edges at all yet"
        );
        assert_eq!(a.state(start).edges.len(), 1);
        assert_eq!(a.state(start).edges[0].guard, Some(LeafId(0)));
        assert_eq!(a.state(start).edges[0].target, mid);
    }

    /// T29: the span bound sums the delay edges of a straight-line automaton,
    /// but a loop through a delay edge (`s[*lo:$]`) has no bound: counting its
    /// edge once retired a cover-sequence attempt after three matches of
    /// `x ##2 y[*3:$]` while it could still match.
    #[test]
    fn max_span_is_unbounded_through_a_delay_loop() {
        let mut a = Automaton::empty();
        let (s0, s1) = (a.start, a.new_state());
        a.add_edge(
            s0,
            None,
            Transition::Delay {
                min: 2,
                max: Some(2),
            },
            s1,
        );
        assert_eq!(a.max_span(), Some(2));
        let s2 = a.new_state();
        a.add_edge(
            s1,
            None,
            Transition::Delay {
                min: 1,
                max: Some(1),
            },
            s2,
        );
        a.add_edge(s2, None, Transition::Epsilon, s1);
        assert_eq!(
            a.max_span(),
            None,
            "a delay inside a loop repeats unboundedly"
        );
        // A loop of only epsilon edges takes no time: the bound stays finite.
        let mut b = Automaton::empty();
        let (t0, t1) = (b.start, b.new_state());
        b.add_edge(
            t0,
            None,
            Transition::Delay {
                min: 1,
                max: Some(1),
            },
            t1,
        );
        b.add_edge(t1, None, Transition::Epsilon, t1);
        assert_eq!(b.max_span(), Some(1));
    }
}