vj-sim 0.3.0

use super::*;
use crate::sva::ir::{Automaton, Transition};
use crate::sva::property::{PropId, SeqRef};
use std::cell::{Cell, RefCell};

/// A host over hand-written rows: leaf `l` is `row[l] != 0`; the clock ticks
/// when the driver says so; live leaves read `live`.
struct Mock {
    tick: Cell<bool>,
    live: RefCell<Vec<bool>>,
}

impl Host for Mock {
    fn clock_ticked(&self, _: ClockId, _: &[u128]) -> bool {
        self.tick.get()
    }
    fn leaf(&self, leaf: LeafId, row: &[u128], _: &[i64]) -> i64 {
        i64::from(row[leaf.0 as usize] != 0)
    }
    fn case_pair(&self, _: LeafId, _: LeafId, _: &[u128], _: &[i64]) -> bool {
        false
    }
    fn live(&self, leaf: LeafId, _: &[u128]) -> bool {
        self.live.borrow()[leaf.0 as usize]
    }
}

/// `l0 ##[min:max] l1` as a sequence.
fn seq2(au: &mut Automaton, a: u32, b: u32, min: u32, max: Option<u32>) -> SeqRef {
    let entry = au.new_state();
    let s1 = au.new_state();
    au.add_edge(entry, Some(LeafId(a)), Transition::Epsilon, s1);
    let s2 = au.new_state();
    au.add_edge(s1, None, Transition::Delay { min, max }, s2);
    let s3 = au.new_state();
    au.add_edge(s2, Some(LeafId(b)), Transition::Epsilon, s3);
    au.add_edge(
        s3,
        None,
        Transition::Match {
            actions: Vec::new(),
        },
        s3,
    );
    SeqRef::single(entry, false)
}

fn leaf_seq(au: &mut Automaton, l: u32) -> SeqRef {
    let entry = au.new_state();
    let s1 = au.new_state();
    au.add_edge(entry, Some(LeafId(l)), Transition::Epsilon, s1);
    au.add_edge(
        s1,
        None,
        Transition::Match {
            actions: Vec::new(),
        },
        s1,
    );
    SeqRef::single(entry, false)
}

/// `a |=> b`.
fn implication(disable: Option<u32>) -> PropertyIr {
    let mut au = Automaton::empty();
    let ante = leaf_seq(&mut au, 0);
    let cons_seq = leaf_seq(&mut au, 1);
    let props = vec![
        Prop::Seq {
            seq: cons_seq,
            strength: None,
        },
        Prop::Implication {
            ante,
            cons: PropId(0),
            overlapped: false,
        },
    ];
    PropertyIr {
        automaton: au,
        props,
        decls: Vec::new(),
        root: PropId(1),
        disable: disable.map(LeafId),
        nv_rules: Vec::new(),
    }
}

fn cfg(ir: PropertyIr, kind: AssertKind, leaves: usize) -> EngineConfig {
    EngineConfig {
        ir,
        kind,
        n_clocks: 1,
        leaf_reads: vec![Vec::new(); leaves],
        leaf_writes: vec![None; leaves],
        activated: false,
        captured: Vec::new(),
        disable_mixed: false,
        history_depth: 0,
        hist_clocks: 0,
        future: false,
        future_clock: 0,
        live_history: false,
        tick_history: false,
    }
}

type Tick = Vec<(EventKind, u64)>;

/// Drives `data` (one row per clock tick, plus the live values at the tick): a
/// data step, then a tick step that samples it. Returns the events of every
/// tick, in order.
fn drive(e: &mut Engine, data: &[(Vec<u128>, Vec<bool>)]) -> Vec<Tick> {
    let host = Mock {
        tick: Cell::new(false),
        live: RefCell::new(vec![false; 8]),
    };
    let mut now = 0;
    let mut out = Vec::new();
    for (row, live) in data {
        // The data step: values change, no tick.
        now += 5;
        host.tick.set(false);
        *host.live.borrow_mut() = vec![false; 8];
        let ev = e.fire(&host, now).unwrap();
        assert!(ev.is_empty());
        e.end_of_step(row.clone());
        // The tick step.
        now += 5;
        host.tick.set(true);
        let mut l = vec![false; 8];
        l[..live.len()].copy_from_slice(live);
        *host.live.borrow_mut() = l;
        let ev = e.fire(&host, now).unwrap();
        out.push(ev.iter().map(|x| (x.kind, x.attempt)).collect());
        e.end_of_step(row.clone());
    }
    out
}

fn row(a: u128, b: u128, c: u128) -> Vec<u128> {
    vec![a, b, c]
}

#[test]
fn implication_reports_pass_and_fail_per_attempt_in_start_order() {
    // The waveform of the sva_assert_basic fixture, sampled at its ticks.
    let mut e = Engine::new(cfg(implication(None), AssertKind::Assert, 2), row(0, 0, 0)).unwrap();
    let data: Vec<_> = [(0, 0), (1, 0), (0, 0), (1, 1), (0, 1), (0, 0)]
        .iter()
        .map(|&(a, b)| (row(a, b, 0), vec![]))
        .collect();
    use EventKind::{Fail, Pass};
    assert_eq!(
        drive(&mut e, &data),
        vec![
            vec![(Pass, 0)],
            vec![],
            vec![(Fail, 1), (Pass, 2)],
            vec![],
            vec![(Pass, 3), (Pass, 4)],
            vec![(Pass, 5)],
        ]
    );
    assert_eq!(e.stats().attempted, 6);
    assert_eq!(e.stats().failed, 1);
}

/// 16.14.3 / 16.14.8: `a |=> b` as a cover property on a waveform with a known
/// mix: attempts 0, 2, 4 and 5 succeed because `a` is false (vacuously),
/// attempt 3 succeeds nonvacuously, attempt 1 fails.
#[test]
fn cover_property_counts_attempts_successes_and_vacuous_successes() {
    let mut e = Engine::new(
        cfg(implication(None), AssertKind::CoverProperty, 2),
        row(0, 0, 0),
    )
    .unwrap();
    let data: Vec<_> = [(0, 0), (1, 0), (0, 0), (1, 1), (0, 1), (0, 0)]
        .iter()
        .map(|&(a, b)| (row(a, b, 0), vec![]))
        .collect();
    drive(&mut e, &data);
    let s = e.stats();
    assert_eq!(
        (s.attempted, s.passed, s.vacuous, s.failed, s.disabled),
        (6, 5, 4, 1, 0)
    );
}

#[test]
fn window_is_trimmed_when_attempts_decide() {
    let mut e = Engine::new(cfg(implication(None), AssertKind::Assert, 2), row(0, 0, 0)).unwrap();
    let data: Vec<_> = (0..50).map(|_| (row(0, 0, 0), vec![])).collect();
    drive(&mut e, &data);
    assert!(e.positions.len() <= 1, "window kept {}", e.positions.len());
}

#[test]
fn disable_true_while_pending_discards_the_attempt() {
    // Leaf 2 is the disable condition (live).
    let mut e = Engine::new(
        cfg(implication(Some(2)), AssertKind::Assert, 3),
        row(0, 0, 0),
    )
    .unwrap();
    // tick 0: a=1 pending; tick 1: disable true -> the pending attempt is
    // Disabled (not failed although b is 0), and the attempt that starts at the
    // disabled tick is disabled too (16.12: the window starts at the attempt).
    let data = vec![
        (row(1, 0, 0), vec![false, false, false]),
        (row(0, 0, 0), vec![false, false, true]),
        (row(0, 0, 0), vec![false, false, false]),
    ];
    use EventKind::Pass;
    assert_eq!(drive(&mut e, &data), vec![vec![], vec![], vec![(Pass, 2)]]);
    assert_eq!(e.stats().disabled, 2);
    assert_eq!(e.stats().failed, 0);
}

#[test]
fn restrict_is_never_checked() {
    let mut e = Engine::new(
        cfg(implication(None), AssertKind::Restrict, 2),
        row(0, 0, 0),
    )
    .unwrap();
    let data = vec![(row(1, 0, 0), vec![]), (row(0, 0, 0), vec![])];
    assert_eq!(drive(&mut e, &data), vec![Tick::new(), Tick::new()]);
    assert_eq!(e.stats().attempted, 0);
}

fn range_seq() -> PropertyIr {
    let mut au = Automaton::empty();
    let seq = seq2(&mut au, 0, 1, 1, Some(2));
    PropertyIr {
        automaton: au,
        props: vec![Prop::Seq {
            seq,
            strength: None,
        }],
        decls: Vec::new(),
        root: PropId(0),
        disable: None,
        nv_rules: Vec::new(),
    }
}

#[test]
fn cover_sequence_counts_every_match_cover_property_once() {
    // `a ##[1:2] b`; a at tick 0, b at ticks 1 and 2: the one attempt that starts
    // at tick 0 has two matches (16.14.3).
    let data = vec![
        (row(1, 0, 0), vec![]),
        (row(0, 1, 0), vec![]),
        (row(0, 1, 0), vec![]),
    ];
    let mut s = Engine::new(cfg(range_seq(), AssertKind::CoverSequence, 2), row(0, 0, 0)).unwrap();
    use EventKind::Match;
    assert_eq!(
        drive(&mut s, &data),
        vec![vec![], vec![(Match, 0)], vec![(Match, 0)]]
    );
    assert_eq!(s.stats().matched, 2);
    let mut p = Engine::new(cfg(range_seq(), AssertKind::CoverProperty, 2), row(0, 0, 0)).unwrap();
    use EventKind::Pass;
    assert_eq!(drive(&mut p, &data), vec![vec![], vec![(Pass, 0)], vec![]]);
    assert_eq!(p.stats().passed, 1);
    assert_eq!(p.stats().attempted, 3);
}

#[test]
fn cover_sequence_attempts_retire_after_the_span() {
    let mut s = Engine::new(cfg(range_seq(), AssertKind::CoverSequence, 2), row(0, 0, 0)).unwrap();
    let data: Vec<_> = (0..20).map(|_| (row(1, 0, 0), vec![])).collect();
    drive(&mut s, &data);
    assert!(
        s.attempts.len() <= 4,
        "{} attempts pending",
        s.attempts.len()
    );
    assert!(
        s.positions.len() <= 5,
        "{} positions kept",
        s.positions.len()
    );
}

/// A host for a two-clock sequence: leaf 0 is bit 0 and leaf 1 is bit 1 of the
/// position's own word; the driver says which clocks tick at each step.
struct TwoClocks {
    ticks: RefCell<[bool; 2]>,
}

impl Host for TwoClocks {
    fn clock_ticked(&self, clock: ClockId, _: &[u128]) -> bool {
        self.ticks.borrow()[clock.0 as usize]
    }
    fn leaf(&self, leaf: LeafId, row: &[u128], _: &[i64]) -> i64 {
        i64::from(row[0] >> leaf.0 & 1 != 0)
    }
    fn case_pair(&self, _: LeafId, _: LeafId, _: &[u128], _: &[i64]) -> bool {
        false
    }
    fn live(&self, _: LeafId, _: &[u128]) -> bool {
        false
    }
}

/// `@(clk0) l0 ##1 @(clk1) l1`, with an optional `l1[*1:$]`-style tail on clock 1
/// (`tail`): the cross-clock `##1` is a [`Transition::ClockSync`].
fn two_clock_seq(strict: bool, tail: bool) -> PropertyIr {
    let mut au = Automaton::empty();
    let entry = au.new_state();
    let s1 = au.new_state();
    au.add_edge(entry, Some(LeafId(0)), Transition::Epsilon, s1);
    let s2 = au.new_state();
    au.add_edge(
        s1,
        None,
        Transition::ClockSync {
            to: ClockId(1),
            strict,
        },
        s2,
    );
    let s3 = au.new_state();
    au.add_edge(s2, Some(LeafId(1)), Transition::Epsilon, s3);
    let end = if tail {
        // A second leaf-1 position one clock-1 tick later: `l1 ##1 l1`.
        let s4 = au.new_state();
        au.add_edge(
            s3,
            None,
            Transition::Delay {
                min: 1,
                max: Some(1),
            },
            s4,
        );
        let s5 = au.new_state();
        au.add_edge(s4, Some(LeafId(1)), Transition::Epsilon, s5);
        s5
    } else {
        s3
    };
    au.add_edge(
        end,
        None,
        Transition::Match {
            actions: Vec::new(),
        },
        end,
    );
    PropertyIr {
        automaton: au,
        props: vec![Prop::Seq {
            seq: SeqRef {
                entry,
                admits_empty: false,
                clock: ClockId(0),
                end_clock: ClockId(1),
            },
            strength: None,
        }],
        decls: Vec::new(),
        root: PropId(0),
        disable: None,
        nv_rules: Vec::new(),
    }
}

/// Runs `(clock ticks, end value)` steps; a step samples the end value of the one
/// before it (0 at the start). Returns each step's events.
fn two_clock_run(e: &mut Engine, steps: &[([bool; 2], u128)]) -> Vec<Tick> {
    let host = TwoClocks {
        ticks: RefCell::new([false; 2]),
    };
    let mut out = Vec::new();
    for (n, (ticks, end)) in steps.iter().enumerate() {
        *host.ticks.borrow_mut() = *ticks;
        let ev = e.fire(&host, 10 * (n as u64 + 1)).unwrap();
        out.push(ev.iter().map(|x| (x.kind, x.attempt)).collect());
        e.end_of_step(vec![*end]);
    }
    out
}

/// 16.13.1, 16.14.3: a `cover sequence` over two clocks. `l0` is sampled at ticks
/// of clock 0, the `##1` moves to the first tick of clock 1 strictly after it and
/// `l1` is sampled there; each attempt starts at a tick of clock 0.
#[test]
fn multiclock_cover_sequence_counts_matches_across_the_clock_change() {
    use EventKind::Match;
    let mut cfg = cfg(two_clock_seq(true, false), AssertKind::CoverSequence, 2);
    cfg.n_clocks = 2;
    let mut e = Engine::new(cfg, vec![0]).unwrap();
    // Bit 0 is `l0`, bit 1 is `l1`. A step samples the end value of the one before.
    let r = two_clock_run(
        &mut e,
        &[
            ([false, false], 0b00),
            ([true, false], 0b01), // clock 0 tick, l0 = 0: attempt 0 dies
            ([false, true], 0b10), // clock 1 tick, l1 = 0 (S = 01)
            ([true, false], 0b01), // clock 0 tick, l0 = 0 (S = 10): attempt 1 dies
            ([false, true], 0b11), // clock 1 tick, l1 = 0 (S = 01)
            ([true, false], 0b10), // clock 0 tick, l0 = 1 (S = 11): attempt 2 starts
            ([false, false], 0b10),
            ([false, true], 0b00), // clock 1 tick, l1 = 1 (S = 10): match
            ([true, true], 0b00),
            ([true, true], 0b00),
        ],
    );
    let mut expect = vec![Tick::new(); 10];
    expect[7] = vec![(Match, 2)];
    assert_eq!(r, expect, "{r:?}");
    assert_eq!(e.stats().matched, 1);
}

/// The `##1` of a clock change is strict (the new clock's tick must come
/// strictly after the old clock's), `##0` may land on the same instant.
#[test]
fn a_clock_change_is_strict_for_one_and_weak_for_zero() {
    use EventKind::Match;
    for (strict, at_same_instant) in [(true, None), (false, Some(1))] {
        let mut cfg = cfg(two_clock_seq(strict, false), AssertKind::CoverSequence, 2);
        cfg.n_clocks = 2;
        let mut e = Engine::new(cfg, vec![0]).unwrap();
        // One instant where both clocks tick and both leaves are true.
        let r = two_clock_run(&mut e, &[([false, false], 0b11), ([true, true], 0b00)]);
        let expect = match at_same_instant {
            Some(i) => {
                let mut v = vec![Tick::new(); 2];
                v[i] = vec![(Match, 0)];
                v
            }
            None => vec![Tick::new(); 2],
        };
        assert_eq!(r, expect, "strict={strict}: {r:?}");
    }
}

/// A multiclock attempt has no static span (its length is a function of the other
/// clock), yet it must still retire once it can match no more: a long run of
/// failed and matched attempts leaves nothing pending.
#[test]
fn multiclock_cover_sequence_attempts_retire() {
    let mut cfg = cfg(two_clock_seq(true, true), AssertKind::CoverSequence, 2);
    cfg.n_clocks = 2;
    let mut e = Engine::new(cfg, vec![0]).unwrap();
    let mut steps = Vec::new();
    for _ in 0..40 {
        steps.push(([true, false], 0b11));
        steps.push(([false, true], 0b11));
    }
    two_clock_run(&mut e, &steps);
    assert!(
        e.attempts.len() <= 4,
        "{} attempts pending",
        e.attempts.len()
    );
    assert!(
        e.positions.len() <= 8,
        "{} positions kept",
        e.positions.len()
    );
}

/// `expect (@(posedge clk) l0)`: one leaf, a plain sequence property.
fn expect_leaf0() -> PropertyIr {
    let mut au = Automaton::empty();
    let seq = leaf_seq(&mut au, 0);
    PropertyIr {
        automaton: au,
        props: vec![Prop::Seq {
            seq,
            strength: None,
        }],
        decls: Vec::new(),
        root: PropId(0),
        disable: None,
        nv_rules: Vec::new(),
    }
}

fn expect_cfg() -> EngineConfig {
    EngineConfig {
        activated: true,
        ..cfg(expect_leaf0(), AssertKind::Expect, 1)
    }
}

fn tick_host(tick: bool) -> Mock {
    Mock {
        tick: Cell::new(tick),
        live: RefCell::new(vec![false; 8]),
    }
}

#[test]
fn expect_first_evaluation_is_the_clocking_event_after_the_one_of_its_step() {
    // 16.17: "the first evaluation shall take place on the next clocking event".
    // The expect executes in a time step in which the clock ticks as well: that
    // tick (sampling l0 = 0) is not an evaluation; the next one (sampling
    // l0 = 1) is, and the property succeeds. Had the attempt started at the
    // first tick it would have failed.
    let host = tick_host(true);
    let mut e = Engine::new(expect_cfg(), vec![0]).unwrap();
    e.activate_tagged(10, Vec::new(), 7);
    let ev = e.fire(&host, 10).unwrap();
    assert!(
        ev.is_empty(),
        "no attempt starts at the activation step's tick"
    );
    assert_eq!(e.stats().attempted, 0);
    e.end_of_step(vec![1]);
    let ev = e.fire(&host, 20).unwrap();
    assert_eq!(ev.len(), 1);
    assert_eq!(ev[0].kind, EventKind::Pass);
    assert_eq!(ev[0].tag, 7, "the event carries the activation's tag");
    assert_eq!(e.stats().attempted, 1);
}

#[test]
fn expect_is_a_single_evaluation_thread_and_reports_failure() {
    // The property fails at its (first) clocking event: one failure report, and
    // nothing starts again until the expect statement is executed again.
    let host = tick_host(true);
    let mut e = Engine::new(expect_cfg(), vec![0]).unwrap();
    e.activate_tagged(10, Vec::new(), 1);
    assert!(e.fire(&host, 10).unwrap().is_empty());
    e.end_of_step(vec![0]);
    let ev = e.fire(&host, 20).unwrap();
    assert_eq!(ev.len(), 1);
    assert_eq!(ev[0].kind, EventKind::Fail);
    e.end_of_step(vec![1]);
    assert!(e.fire(&host, 30).unwrap().is_empty());
    e.end_of_step(vec![1]);
    assert!(e.fire(&host, 40).unwrap().is_empty());
    assert_eq!(e.stats().attempted, 1);
}

#[test]
fn expect_activated_in_a_step_without_a_tick_waits_for_the_next_tick() {
    let host = tick_host(false);
    let mut e = Engine::new(expect_cfg(), vec![1]).unwrap();
    e.activate_tagged(10, Vec::new(), 3);
    assert!(e.fire(&host, 10).unwrap().is_empty());
    e.end_of_step(vec![1]);
    host.tick.set(true);
    let ev = e.fire(&host, 20).unwrap();
    assert_eq!(ev.len(), 1);
    assert_eq!((ev[0].kind, ev[0].tag), (EventKind::Pass, 3));
}

#[test]
fn expect_activated_after_the_tick_of_its_step_was_evaluated_still_waits() {
    // The step's tick was already seen by an earlier firing of the same step.
    let host = tick_host(true);
    let mut e = Engine::new(expect_cfg(), vec![1]).unwrap();
    assert!(e.fire(&host, 10).unwrap().is_empty());
    e.activate_tagged(10, Vec::new(), 5);
    assert!(e.fire(&host, 10).unwrap().is_empty());
    assert_eq!(e.stats().attempted, 0);
    e.end_of_step(vec![1]);
    let ev = e.fire(&host, 20).unwrap();
    assert_eq!((ev[0].kind, ev[0].tag), (EventKind::Pass, 5));
}

// ---- 20.11: assertion control ---------------------------------------------------

use crate::sched::assert_control::{Q_ALL, Q_CHECKING, Q_FAIL, Q_PASS_NONVACUOUS};

/// One clock tick at `now` sampling `row`; the events it decides.
fn tick_at(e: &mut Engine, now: u64, row: Vec<u128>) -> Vec<Event> {
    let host = tick_host(true);
    // The previous step's final row is what a tick samples.
    e.end_of_step(row);
    let ev = e.fire(&host, now).unwrap();
    e.end_of_step(vec![0, 0, 0]);
    ev
}

/// `$assertoff` (20.11): no new attempt starts, an executing one runs to its
/// outcome and its action still happens; `$asserton` resumes starting them.
#[test]
fn checking_off_starts_no_attempts_but_leaves_executing_ones_alone() {
    let mut e = Engine::new(cfg(implication(None), AssertKind::Assert, 2), row(0, 0, 0)).unwrap();
    assert!(tick_at(&mut e, 10, row(1, 0, 0)).is_empty(), "a=1: pending");
    assert_eq!(e.stats().attempted, 1);
    e.set_checking(false);
    let ev = tick_at(&mut e, 20, row(0, 0, 0));
    assert_eq!(
        ev.iter().map(|x| (x.kind, x.attempt)).collect::<Vec<_>>(),
        vec![(EventKind::Fail, 0)],
        "the executing attempt fails (b is 0) although checking is off"
    );
    assert_eq!(e.stats().attempted, 1, "no attempt started at tick 20");
    assert!(tick_at(&mut e, 30, row(0, 0, 0)).is_empty());
    assert_eq!(e.stats().attempted, 1);
    e.set_checking(true);
    let ev = tick_at(&mut e, 40, row(0, 0, 0));
    assert_eq!(ev.len(), 1, "a = 0: the new attempt passes vacuously");
    assert_eq!(e.stats().attempted, 2);
}

/// `$assertkill` (20.11): executing attempts are aborted -- no outcome, no
/// action -- and the statistics are as they were.
#[test]
fn kill_aborts_executing_attempts_without_an_outcome() {
    let mut e = Engine::new(cfg(implication(None), AssertKind::Assert, 2), row(0, 0, 0)).unwrap();
    assert!(tick_at(&mut e, 10, row(1, 0, 0)).is_empty());
    e.kill();
    e.set_checking(false);
    assert!(
        tick_at(&mut e, 20, row(0, 0, 0)).is_empty(),
        "the aborted attempt does not fail"
    );
    let s = e.stats();
    assert_eq!((s.attempted, s.failed, s.passed), (1, 0, 0));
    assert!(e.positions.len() <= 1, "the window is released");
    // Attempts started after the kill are fresh ones.
    e.set_checking(true);
    let ev = tick_at(&mut e, 30, row(1, 0, 0));
    assert!(ev.is_empty());
    let ev = tick_at(&mut e, 40, row(0, 0, 0));
    assert_eq!(ev.iter().filter(|x| x.kind == EventKind::Fail).count(), 1);
}

/// A procedural instance that matured but has not started yet is an executing
/// attempt-to-be: `$assertkill` drops it too.
#[test]
fn kill_drops_matured_instances_that_have_not_started() {
    let host = tick_host(false);
    let mut e = Engine::new(
        EngineConfig {
            activated: true,
            ..cfg(implication(None), AssertKind::Assert, 2)
        },
        row(0, 0, 0),
    )
    .unwrap();
    e.activate_tagged(10, Vec::new(), 1);
    assert!(e.fire(&host, 10).unwrap().is_empty());
    e.kill();
    host.tick.set(true);
    e.end_of_step(row(1, 0, 0));
    assert!(e.fire(&host, 20).unwrap().is_empty());
    assert_eq!(e.stats().attempted, 0, "the instance never started");
}

/// The action flags in force when an attempt starts are the ones its outcome
/// carries (20.11: an assertion already executing is not affected by them).
#[test]
fn events_carry_the_action_flags_of_the_attempt_start() {
    let mut e = Engine::new(cfg(implication(None), AssertKind::Assert, 2), row(0, 0, 0)).unwrap();
    assert!(tick_at(&mut e, 10, row(1, 0, 0)).is_empty());
    e.set_action_flags(Q_CHECKING | Q_FAIL);
    // Attempt 0 started under `Q_ALL`, attempt 1 (a=0) starts under the new flags.
    let ev = tick_at(&mut e, 20, row(0, 0, 0));
    let by_attempt: Vec<(u64, u32)> = ev.iter().map(|x| (x.attempt, x.flags)).collect();
    assert_eq!(by_attempt, vec![(0, Q_ALL), (1, Q_CHECKING | Q_FAIL)]);
    assert_eq!(by_attempt[0].1 & Q_PASS_NONVACUOUS, Q_PASS_NONVACUOUS);
}

// ---- 16.11: subroutine calls attached to a sequence -----------------------------

use crate::sva::ir::{CallArg, CallId};

/// `(l0, call#0(l1)) ##1 (l1, call#1())`, ending in a match.
fn call_seq(au: &mut Automaton) -> SeqRef {
    let entry = au.new_state();
    let s1 = au.new_state();
    let s2 = au.new_state();
    let s3 = au.new_state();
    let s4 = au.new_state();
    let s5 = au.new_state();
    au.add_edge(entry, Some(LeafId(0)), Transition::Epsilon, s1);
    au.add_edge(
        s1,
        None,
        Transition::SubroutineCall {
            call: CallId(0),
            args: vec![CallArg::Value(LeafId(1))],
        },
        s2,
    );
    au.add_edge(
        s2,
        None,
        Transition::Delay {
            min: 1,
            max: Some(1),
        },
        s3,
    );
    au.add_edge(s3, Some(LeafId(1)), Transition::Epsilon, s4);
    au.add_edge(
        s4,
        None,
        Transition::SubroutineCall {
            call: CallId(1),
            args: vec![],
        },
        s5,
    );
    au.add_edge(
        s5,
        None,
        Transition::Match {
            actions: Vec::new(),
        },
        s5,
    );
    SeqRef::single(entry, false)
}

/// `call_seq |-> l2`, with an optional `disable iff` leaf.
fn call_implication(disable: Option<u32>) -> PropertyIr {
    let mut au = Automaton::empty();
    let ante = call_seq(&mut au);
    let cons = leaf_seq(&mut au, 2);
    PropertyIr {
        automaton: au,
        props: vec![
            Prop::Seq {
                seq: cons,
                strength: None,
            },
            Prop::Implication {
                ante,
                cons: PropId(0),
                overlapped: true,
            },
        ],
        decls: Vec::new(),
        root: PropId(1),
        disable: disable.map(LeafId),
        nv_rules: Vec::new(),
    }
}

/// `drive`, keeping whole events.
fn drive_events(e: &mut Engine, data: &[(Vec<u128>, Vec<bool>)]) -> Vec<Vec<Event>> {
    let host = tick_host(false);
    let mut now = 0;
    let mut out = Vec::new();
    for (row, live) in data {
        now += 5;
        host.tick.set(false);
        *host.live.borrow_mut() = vec![false; 8];
        assert!(e.fire(&host, now).unwrap().is_empty());
        e.end_of_step(row.clone());
        now += 5;
        host.tick.set(true);
        let mut l = vec![false; 8];
        l[..live.len()].copy_from_slice(live);
        *host.live.borrow_mut() = l;
        out.push(e.fire(&host, now).unwrap());
        e.end_of_step(row.clone());
    }
    out
}

/// A tick's events as `(kind, attempt, call and its args)`.
type Shown = Vec<(EventKind, u64, Option<(u32, Vec<Option<i64>>)>)>;

fn shown(events: &[Event]) -> Shown {
    events
        .iter()
        .map(|e| {
            (
                e.kind,
                e.attempt,
                e.call.as_ref().map(|c| (c.call.0, c.args.clone())),
            )
        })
        .collect()
}

fn calls_only(ticks: &[Vec<Event>]) -> Vec<Shown> {
    ticks
        .iter()
        .map(|t| {
            shown(t)
                .into_iter()
                .filter(|(k, _, _)| *k == EventKind::Call)
                .collect()
        })
        .collect()
}

/// 16.11: each call is executed at its end point, in the tick the sequence
/// reached it, with the value sampled there, and before the attempt's outcome.
#[test]
fn a_call_is_reported_at_its_end_point_before_the_outcome() {
    let mut e = Engine::new(
        cfg(call_implication(None), AssertKind::Assert, 3),
        row(0, 0, 0),
    )
    .unwrap();
    let data = vec![(row(1, 0, 1), vec![]), (row(0, 1, 1), vec![])];
    let ticks = drive_events(&mut e, &data);
    use EventKind::{Call, Pass};
    assert_eq!(shown(&ticks[0]), vec![(Call, 0, Some((0, vec![Some(0)])))]);
    assert_eq!(
        shown(&ticks[1]),
        vec![
            (Call, 0, Some((1, vec![]))),
            (Pass, 0, None),
            (Pass, 1, None)
        ]
    );
}

/// 16.11: the calls are executed whether or not the property holds.
#[test]
fn a_failing_attempt_still_executes_its_calls() {
    let mut e = Engine::new(
        cfg(call_implication(None), AssertKind::Assert, 3),
        row(0, 0, 0),
    )
    .unwrap();
    let data = vec![(row(1, 0, 1), vec![]), (row(0, 1, 0), vec![])];
    let ticks = drive_events(&mut e, &data);
    use EventKind::{Call, Fail, Pass};
    assert_eq!(
        shown(&ticks[1]),
        vec![
            (Call, 0, Some((1, vec![]))),
            (Fail, 0, None),
            (Pass, 1, None)
        ]
    );
    assert_eq!(e.stats().failed, 1);
}

/// A pending attempt is re-run on every tick; each call is reported once.
#[test]
fn a_pending_attempt_reports_each_call_once_however_often_it_is_re_run() {
    // `l0 ##[1:3] (l1, call#0(l1)) |-> l2`: end points at every tick where l1 holds.
    let mut au = Automaton::empty();
    let entry = au.new_state();
    let s1 = au.new_state();
    let s2 = au.new_state();
    let s3 = au.new_state();
    let s4 = au.new_state();
    au.add_edge(entry, Some(LeafId(0)), Transition::Epsilon, s1);
    au.add_edge(
        s1,
        None,
        Transition::Delay {
            min: 1,
            max: Some(3),
        },
        s2,
    );
    au.add_edge(s2, Some(LeafId(1)), Transition::Epsilon, s3);
    au.add_edge(
        s3,
        None,
        Transition::SubroutineCall {
            call: CallId(0),
            args: vec![CallArg::Value(LeafId(1))],
        },
        s4,
    );
    au.add_edge(
        s4,
        None,
        Transition::Match {
            actions: Vec::new(),
        },
        s4,
    );
    let ante = SeqRef::single(entry, false);
    let cons = leaf_seq(&mut au, 2);
    let ir = PropertyIr {
        automaton: au,
        props: vec![
            Prop::Seq {
                seq: cons,
                strength: None,
            },
            Prop::Implication {
                ante,
                cons: PropId(0),
                overlapped: true,
            },
        ],
        decls: Vec::new(),
        root: PropId(1),
        disable: None,
        nv_rules: Vec::new(),
    };
    let mut e = Engine::new(cfg(ir, AssertKind::Assert, 3), row(0, 0, 0)).unwrap();
    let data = vec![
        (row(1, 0, 1), vec![]),
        (row(0, 1, 1), vec![]),
        (row(0, 1, 1), vec![]),
        (row(0, 0, 1), vec![]),
    ];
    let ticks = drive_events(&mut e, &data);
    let one = vec![(EventKind::Call, 0, Some((0, vec![Some(1)])))];
    assert_eq!(
        calls_only(&ticks),
        vec![vec![], one.clone(), one, vec![]],
        "attempt 0 ends at ticks 1 and 2, each reported at its own tick, once"
    );
    // The attempt then passes at its last pending tick, after the calls.
    assert_eq!(shown(&ticks[3]).first(), Some(&(EventKind::Pass, 0, None)));
}

/// 16.12: a call at or after the tick `disable iff` was true is not the attempt's.
#[test]
fn a_disabled_attempt_executes_only_the_calls_before_the_disabling() {
    let mut e = Engine::new(
        cfg(call_implication(Some(3)), AssertKind::Assert, 4),
        row(0, 0, 0),
    )
    .unwrap();
    let data = vec![
        (row(1, 0, 1), vec![false, false, false, false]),
        (row(0, 1, 1), vec![false, false, false, true]),
    ];
    let ticks = drive_events(&mut e, &data);
    use EventKind::Call;
    assert_eq!(shown(&ticks[0]), vec![(Call, 0, Some((0, vec![Some(0)])))]);
    assert_eq!(shown(&ticks[1]), vec![], "call #1 is at the disabling tick");
    assert_eq!(e.stats().disabled, 2);
}

/// 16.14.3: a `cover sequence` executes the calls at every match.
#[test]
fn cover_sequence_executes_calls_at_every_end_point() {
    let mut au = Automaton::empty();
    let entry = au.new_state();
    let s1 = au.new_state();
    let s2 = au.new_state();
    let s3 = au.new_state();
    let s4 = au.new_state();
    au.add_edge(entry, Some(LeafId(0)), Transition::Epsilon, s1);
    au.add_edge(
        s1,
        None,
        Transition::Delay {
            min: 1,
            max: Some(2),
        },
        s2,
    );
    au.add_edge(s2, Some(LeafId(1)), Transition::Epsilon, s3);
    au.add_edge(
        s3,
        None,
        Transition::SubroutineCall {
            call: CallId(7),
            args: vec![],
        },
        s4,
    );
    au.add_edge(
        s4,
        None,
        Transition::Match {
            actions: Vec::new(),
        },
        s4,
    );
    let seq = SeqRef::single(entry, false);
    let ir = PropertyIr {
        automaton: au,
        props: vec![Prop::Seq {
            seq,
            strength: None,
        }],
        decls: Vec::new(),
        root: PropId(0),
        disable: None,
        nv_rules: Vec::new(),
    };
    let mut e = Engine::new(cfg(ir, AssertKind::CoverSequence, 2), row(0, 0, 0)).unwrap();
    let data = vec![
        (row(1, 0, 0), vec![]),
        (row(0, 1, 0), vec![]),
        (row(0, 1, 0), vec![]),
    ];
    let ticks = drive_events(&mut e, &data);
    use EventKind::{Call, Match};
    assert_eq!(shown(&ticks[0]), vec![]);
    assert_eq!(
        shown(&ticks[1]),
        vec![(Call, 0, Some((7, vec![]))), (Match, 0, None)]
    );
    assert_eq!(
        shown(&ticks[2]),
        vec![(Call, 0, Some((7, vec![]))), (Match, 0, None)]
    );
}

/// Calls inside an abort operand, an expect's property or an end-point instance
/// are refused loudly rather than run in a partly modelled way.
#[test]
fn unsupported_call_placements_are_refused_with_the_reason() {
    let with_abort = {
        let mut au = Automaton::empty();
        let seq = call_seq(&mut au);
        PropertyIr {
            automaton: au,
            props: vec![
                Prop::Seq {
                    seq,
                    strength: None,
                },
                Prop::Abort {
                    cond: LeafId(2),
                    p: PropId(0),
                    mode: AbortMode::Accept,
                },
            ],
            decls: Vec::new(),
            root: PropId(1),
            disable: None,
            nv_rules: Vec::new(),
        }
    };
    let err = Engine::new(cfg(with_abort, AssertKind::Assert, 3), row(0, 0, 0))
        .err()
        .expect("refused");
    assert!(err.0.contains("accept_on"), "{err}");

    let expect = EngineConfig {
        activated: true,
        ..cfg(call_implication(None), AssertKind::Expect, 3)
    };
    let err = Engine::new(expect, row(0, 0, 0)).err().expect("refused");
    assert!(err.0.contains("expect"), "{err}");

    let mut ir = expect_leaf0();
    let mut inner = Automaton::empty();
    call_seq(&mut inner);
    ir.automaton.new_end_point(crate::sva::ir::EndPoint {
        method: crate::sva::ir::EndMethod::Triggered,
        site: 0,
        automaton: inner,
        flow_out: Vec::new(),
    });
    let err = Engine::new(cfg(ir, AssertKind::Assert, 1), vec![0])
        .err()
        .expect("refused");
    assert!(err.0.contains(".triggered"), "{err}");

    // The same property as an assert is accepted.
    assert!(
        Engine::new(
            cfg(call_implication(None), AssertKind::Assert, 3),
            row(0, 0, 0)
        )
        .is_ok()
    );
}

/// A host over rows with a signal history (16.9.3): the signals are `[r, b]`
/// (`row_len` 2) and a position's row is `[r, b, r_prev, b_prev, r_prev2, ...]`.
/// Leaf 0 is "`r` now and not `back` ticks ago" (`$rose(r)` for `back` 1), leaf 1
/// is `b`.
struct HistHost {
    back: usize,
    tick: Cell<bool>,
}

impl Host for HistHost {
    fn clock_ticked(&self, _: ClockId, prev: &[u128]) -> bool {
        assert_eq!(prev.len(), 2, "the clock test gets the plain row");
        self.tick.get()
    }
    fn leaf(&self, leaf: LeafId, row: &[u128], _: &[i64]) -> i64 {
        assert_eq!(row.len(), 2 * (1 + self.back), "row + history");
        match leaf.0 {
            0 => i64::from(row[0] != 0 && row[2 * self.back] == 0),
            _ => i64::from(row[1] != 0),
        }
    }
    fn case_pair(&self, _: LeafId, _: LeafId, _: &[u128], _: &[i64]) -> bool {
        false
    }
    fn live(&self, _: LeafId, _: &[u128]) -> bool {
        false
    }
}

/// Runs `ticks` (the `[r, b]` sampled at each tick) through a `leaf0 |=> leaf1`
/// engine of history depth `back` whose initial row is `initial`.
fn hist_run(back: usize, initial: [u128; 2], ticks: &[[u128; 2]]) -> Vec<Tick> {
    let mut e = Engine::new(
        EngineConfig {
            history_depth: back,
            ..cfg(implication(None), AssertKind::Assert, 2)
        },
        initial.to_vec(),
    )
    .unwrap();
    let host = HistHost {
        back,
        tick: Cell::new(false),
    };
    let mut now = 0;
    let mut out = Vec::new();
    for row in ticks {
        now += 5;
        host.tick.set(false);
        assert!(e.fire(&host, now).unwrap().is_empty());
        e.end_of_step(row.to_vec());
        now += 5;
        host.tick.set(true);
        let ev = e.fire(&host, now).unwrap();
        out.push(ev.iter().map(|x| (x.kind, x.attempt)).collect());
        e.end_of_step(row.to_vec());
    }
    out
}

#[test]
fn a_position_carries_the_previous_ticks_rows_for_the_sampled_value_functions() {
    use EventKind::{Fail, Pass};
    // `$rose(r) |=> b`: r rises at tick 0 (the initial row is the previous one,
    // 16.5.1) and tick 3, and stays high at tick 1 and tick 4.
    let ticks = [[1, 0], [1, 1], [0, 0], [1, 0], [1, 0]];
    assert_eq!(
        hist_run(1, [0, 0], &ticks),
        vec![
            vec![],
            vec![(Pass, 0), (Pass, 1)],
            vec![(Pass, 2)],
            vec![],
            vec![(Fail, 3), (Pass, 4)],
        ]
    );
    // The default sampled value before the first tick is the initial row's: with
    // r already high there, tick 0 is not a rise and its attempt is vacuous.
    let r = hist_run(1, [1, 0], &ticks);
    assert_eq!(r[0], vec![(Pass, 0)], "{r:?}");
}

#[test]
fn history_depth_two_reaches_the_second_previous_tick() {
    use EventKind::Pass;
    // Leaf 0 is "r now and not two ticks ago", r high at ticks 0..=2: true at
    // tick 0 and tick 1 (two ticks before them is the initial, low row), false at
    // tick 2 (tick 0 was high). With depth 1 tick 1 would be false.
    let r = hist_run(2, [0, 0], &[[1, 1], [1, 1], [1, 1], [0, 0]]);
    assert_eq!(
        r,
        vec![
            vec![],
            vec![(Pass, 0)],
            vec![(Pass, 1), (Pass, 2)],
            vec![(Pass, 3)],
        ],
        "{r:?}"
    );
}

/// A multiclock assertion keeps a history per clock (16.9.3: a sampled value
/// function reads its own clock's previous ticks), so it is accepted.
#[test]
fn a_sampled_value_function_in_a_multiclock_assertion_is_accepted() {
    assert!(
        Engine::new(
            EngineConfig {
                history_depth: 1,
                n_clocks: 2,
                ..cfg(implication(None), AssertKind::Assert, 2)
            },
            vec![0, 0],
        )
        .is_ok()
    );
}

/// A host with per-clock ticks (set by the driver) and one-word rows. Leaf 0 is
/// whatever `l0` makes of the position row; `live` records the rows the live
/// leaf is asked over.
struct Multi {
    ticks: RefCell<Vec<bool>>,
    l0: fn(&[u128]) -> bool,
    live_rows: RefCell<Vec<Vec<u128>>>,
    live_fn: fn(&[u128]) -> bool,
}

impl Multi {
    fn new(l0: fn(&[u128]) -> bool) -> Self {
        Multi {
            ticks: RefCell::new(Vec::new()),
            l0,
            live_rows: RefCell::new(Vec::new()),
            live_fn: |_| false,
        }
    }
}

impl Host for Multi {
    fn clock_ticked(&self, clock: ClockId, _: &[u128]) -> bool {
        self.ticks.borrow()[clock.0 as usize]
    }
    fn leaf(&self, _: LeafId, row: &[u128], _: &[i64]) -> i64 {
        i64::from((self.l0)(row))
    }
    fn case_pair(&self, _: LeafId, _: LeafId, _: &[u128], _: &[i64]) -> bool {
        false
    }
    fn live(&self, _: LeafId, sampled: &[u128]) -> bool {
        self.live_rows.borrow_mut().push(sampled.to_vec());
        (self.live_fn)(sampled)
    }
}

/// Runs steps `(ticks, end value)` (step `n` samples the end value of step
/// `n - 1`, 0 before the first) and returns the events of each.
fn multi_run(e: &mut Engine, host: &Multi, steps: &[(&[bool], u128)]) -> Vec<Tick> {
    let mut out = Vec::new();
    for (n, (ticks, end)) in steps.iter().enumerate() {
        *host.ticks.borrow_mut() = ticks.to_vec();
        let ev = e.fire(host, 10 * (n as u64 + 1)).unwrap();
        out.push(ev.iter().map(|x| (x.kind, x.attempt)).collect());
        e.end_of_step(vec![*end]);
    }
    out
}

/// 16.9.3: `$rose(r, @(posedge fclk))` in an assertion clocked by another clock
/// reads the row sampled at the previous tick of `fclk`, a history-only clock
/// whose ticks make no position.
#[test]
fn a_history_only_clock_keeps_its_own_history_and_makes_no_position() {
    use EventKind::{Fail, Pass};
    // Row of a position: [own, history of clock 0, history of clock 1].
    let mut e = Engine::new(
        EngineConfig {
            n_clocks: 1,
            hist_clocks: 1,
            history_depth: 1,
            ..cfg(expect_leaf0(), AssertKind::Assert, 1)
        },
        vec![0],
    )
    .unwrap();
    let host = Multi::new(|row| {
        assert_eq!(row.len(), 3, "own row, then one history row per clock");
        row[0] != 0 && row[2] == 0
    });
    // The sampled values S are the end values one step earlier. The own clock
    // ticks at steps 3..=6, `fclk` at steps 2 and 4.
    let r = multi_run(
        &mut e,
        &host,
        &[
            (&[false, false], 0),
            (&[false, true], 1),
            (&[true, false], 1),
            (&[true, true], 0),
            (&[true, false], 1),
            (&[true, false], 1),
        ],
    );
    // Step 3: S = 1, fclk's last tick (step 2) sampled 0: rises. Step 4: S = 1,
    // the last STRICTLY prior fclk tick is still step 2: rises (the own clock's
    // previous tick, step 3, would say it did not). Step 5: S = 0. Step 6: S = 1
    // but step 4 sampled 1.
    assert_eq!(
        r,
        vec![
            vec![],
            vec![],
            vec![(Pass, 0)],
            vec![(Pass, 1)],
            vec![(Fail, 2)],
            vec![(Fail, 3)],
        ],
        "{r:?}"
    );
}

/// 16.9.4: a position waits for the next tick of the global clock strictly after
/// its own step, whatever clock made it; the attempt's verdict and its action come
/// then.
#[test]
fn a_future_function_holds_positions_for_the_next_global_tick() {
    use EventKind::{Fail, Pass};
    // Row of a position: [own, next global row] (no history).
    let mut e = Engine::new(
        EngineConfig {
            n_clocks: 1,
            hist_clocks: 1,
            future: true,
            future_clock: 1,
            ..cfg(expect_leaf0(), AssertKind::Assert, 1)
        },
        vec![0],
    )
    .unwrap();
    let host = Multi::new(|row| {
        assert_eq!(row.len(), 2, "own row, then the next global tick's");
        row[1] != 0
    });
    // Own ticks at steps 2, 3 and 6; global ticks at 4, 5 and 8. S4 = E3 = 1,
    // S5 = E4 = 0, S8 = E7 = 0.
    let r = multi_run(
        &mut e,
        &host,
        &[
            (&[false, false], 0),
            (&[true, false], 0),
            (&[true, false], 1),
            (&[false, true], 0),
            (&[false, true], 0),
            (&[true, false], 0),
            (&[false, false], 0),
            (&[false, true], 0),
        ],
    );
    assert_eq!(
        r,
        vec![
            vec![],
            vec![],
            vec![],
            vec![(Pass, 0), (Pass, 1)],
            vec![],
            vec![],
            vec![],
            vec![(Fail, 2)],
        ],
        "{r:?}"
    );
}

/// 16.12: a sampled value function in a disable condition reads the step's
/// sampled row and the history as of BEFORE the step's ticks.
#[test]
fn live_leaves_are_handed_the_position_shaped_row() {
    let mut ir = expect_leaf0();
    ir.disable = Some(LeafId(1));
    let mut e = Engine::new(
        EngineConfig {
            n_clocks: 1,
            history_depth: 1,
            live_history: true,
            ..cfg(ir, AssertKind::Assert, 2)
        },
        vec![0],
    )
    .unwrap();
    let host = Multi::new(|_| true);
    // Own clock ticks at steps 2 and 3; end values 5, 7, 9.
    let r = multi_run(&mut e, &host, &[(&[false], 5), (&[true], 7), (&[true], 9)]);
    assert_eq!(r.len(), 3);
    // Per step: [sampled row, the clock's last-tick row]. Step 2 samples 5 and its
    // history is still the initial row; step 3 samples 7 and the tick of step 2
    // recorded 5. Step 1 is no tick and nothing is pending, so the live values
    // (which only a tick's position or a pending attempt consumes) are not read.
    assert_eq!(
        host.live_rows.borrow().as_slice(),
        &[vec![5, 0], vec![7, 5]]
    );
}

// ---- 16.12 / 16.14.6.1: `disable iff` over captured values and signals -----------

/// `a |=> b` with `disable iff (<leaf 2: reads the captured item and a signal>)`,
/// activated per instance with one captured value.
fn mixed_cfg() -> EngineConfig {
    let mut ir = implication(Some(2));
    let v = ir.automaton.new_local_var(32, false);
    let mut c = cfg(ir, AssertKind::Assert, 3);
    c.activated = true;
    c.captured = vec![v];
    c.disable_mixed = true;
    c.leaf_reads[2] = vec![v];
    c
}

#[test]
fn mixed_disable_tuples_are_pruned_once_their_attempts_completed() {
    // Every instance carries a fresh captured value, so without pruning the
    // engine would keep (and re-evaluate at every step) one tuple per instance
    // of the whole run. Each instance completes at its own tick (`a` is low:
    // the implication holds vacuously), so only the last step's are live.
    let host = tick_host(true);
    let mut e = Engine::new(mixed_cfg(), vec![0, 0, 0]).unwrap();
    let mut most = 0;
    for n in 0..300u64 {
        let now = 10 * (n + 1);
        e.activate(now, vec![n as i64]);
        let ev = e.fire(&host, now).unwrap();
        assert!(ev.iter().all(|x| x.kind != EventKind::Fail));
        most = most.max(e.live_tuples());
        e.end_of_step(vec![0, 0, 0]);
    }
    assert_eq!(e.stats().attempted, 300);
    assert!(most <= 2, "{most} tuples live at once");
}

#[test]
fn mixed_disable_tuple_activated_after_the_steps_fire_is_recorded_by_the_next_fire() {
    // 16.14.6: an instance a Reactive-region procedure queues after the step's
    // first firing still starts at that step's tick; the same step's next
    // firing records its tuple's condition (the host fires again after every
    // activation), so the disable value of the start step is not lost.
    let host = tick_host(true);
    let mut e = Engine::new(mixed_cfg(), vec![0, 0, 0]).unwrap();
    assert!(e.fire(&host, 10).unwrap().is_empty());
    e.activate(10, vec![7]);
    assert_eq!(e.live_tuples(), 1);
    // The condition (leaf 2) is true at this step: the new attempt is disabled.
    host.live.borrow_mut()[2] = true;
    e.fire(&host, 10).unwrap();
    e.end_of_step(vec![1, 0, 0]);
    host.live.borrow_mut()[2] = false;
    let ev = e.fire(&host, 20).unwrap();
    assert!(ev.is_empty(), "the attempt was disabled at its start step");
    assert_eq!(e.stats().failed, 0);
}