vj-codegen 0.1.0

//! The property builder against the LRM, judged by the reference evaluator.
//!
//! Neither iverilog nor Verilator can run a Clause 16 property, so the oracle for
//! every test here is the LRM text itself: the expected verdicts are worked out by
//! hand from the clause the test cites, and every equivalence the LRM states
//! ("`a implies b` is equivalent to `not a or b`") is checked EXHAUSTIVELY over
//! every trace of the signals involved up to a length bound, from every start
//! tick, under both the `assert` and the `cover` reading of a bare sequence.
use std::collections::BTreeMap;

use sv_lang::{AnalysisFlags, Compilation, Session, SyntaxTree};
use sv_sim_sim::sva::ir::LeafId;
use sv_sim_sim::sva::property::{Evaluator, PropEnv, Verdict};
use sv_sim_sim::sva::trace::{self, Timeline, TraceError};

use super::super::LeafLocals;
use super::*;

/// An `x` sample (the evaluator hands the environment its own comparison, and
/// the environment here says an `x` selector matches no label, 12.5 / 16.12.16).
const X: i64 = i64::MIN;

/// Compiles `decls` and one concurrent assertion `stmt` inside an `always_ff`
/// (the scaffold of `build::tests::with_assertion`), builds the PROPERTY at its
/// root and hands the result, the syntax tree and the diagnostics to `f`.
fn with_property<R>(
    decls: &str,
    stmt: &str,
    allow_errors: bool,
    f: impl FnOnce(Result<(PropertyIr, LeafTable<'_>), LoweringError>, &SyntaxTree) -> R,
) -> R {
    let src = format!(
        "module m;\n\
         logic clk, sysclk, a, b, c, d, e, x, y, z, reset;\n\
         logic [7:0] bb;\n\
         logic [1:0] dly;\n\
         int n;\n\
         parameter my_delay = 2;\n\
         {decls}\n\
         always_ff @(posedge clk) begin\n\
           {stmt}\n\
         end\n\
         endmodule\n"
    );
    let session = Session::new();
    let mut comp = Compilation::new(&session).unwrap();
    comp.add_source(&src).unwrap();
    let design = comp.compile().unwrap();
    let diags = design.diagnostics();
    if !allow_errors {
        assert!(
            !diags.has_errors(),
            "fixture has compile errors:\n{}\n{src}",
            diags.rendered()
        );
    }
    let m = design
        .top_instances()
        .next()
        .unwrap()
        .instance_body()
        .unwrap();
    let analysis = design.analyze(AnalysisFlags::NONE, 1).unwrap();
    let proc = analysis.procedures(m).next().unwrap();
    let Some(assertion) = analysis.assertions(proc.symbol()).next() else {
        panic!(
            "slang dropped the assertion; analysis diagnostics:\n{}",
            analysis.diagnostics().rendered()
        );
    };
    let tree = design.syntax_trees().into_iter().next().unwrap();
    let root = assertion.root().as_assertion_expr().unwrap();
    let (root, root_clock) = if root.kind() == AssertionExprKind::Clocking {
        let kids = root.children();
        (kids[1].as_assertion_expr().unwrap(), Some(kids[0]))
    } else {
        (root, None)
    };
    f(build_property(root, root_clock, (&tree).into(), &m), &tree)
}

/// `prop` as the whole of `assert property (@(posedge clk) ...)`.
fn ap(prop: &str) -> String {
    format!("assert property (@(posedge clk) {prop});")
}

/// The error [`build_property`] returns for a design slang accepts.
fn rejected(decls: &str, prop: &str) -> String {
    with_property(decls, &ap(prop), false, |r, _| match r {
        Ok(_) => panic!("`{prop}` was expected to be rejected"),
        Err(e) => e.to_string(),
    })
}

/// [`rejected`] for a design slang itself diagnoses.
fn rejected_lenient(decls: &str, prop: &str) -> String {
    with_property(decls, &ap(prop), true, |r, _| match r {
        Ok(_) => panic!("`{prop}` was expected to be rejected"),
        Err(e) => e.to_string(),
    })
}

/// Builds `prop` and panics (with the error) if the builder refuses it.
fn builds(decls: &str, prop: &str) {
    with_property(decls, &ap(prop), false, |r, _| {
        r.unwrap_or_else(|e| panic!("`{prop}` failed to build: {e}"));
    });
}

/// The samples of the named signals, one per tick: `0`-`9` is that integer, `x`
/// is [`X`].
type Rows = BTreeMap<String, Vec<i64>>;

fn rows(spec: &[(&str, &str)]) -> Rows {
    spec.iter()
        .map(|(name, samples)| {
            (
                name.to_string(),
                samples
                    .chars()
                    .map(|c| match c {
                        'x' => X,
                        d => i64::from(d.to_digit(10).expect("a digit or x")),
                    })
                    .collect(),
            )
        })
        .collect()
}

/// The property's leaves evaluated on [`Rows`].
struct Sigs<'a, 'd> {
    leaves: &'a LeafTable<'d>,
    rows: &'a Rows,
    /// Samples strictly between tick `t` and `t + 1` (the asynchronous abort
    /// conditions of 16.12.14), per signal.
    between: BTreeMap<String, Vec<i64>>,
    /// The ticks of each clock of a multiclock assertion (T28); `None` for the
    /// single-clock tests, where every step of the rows is a tick.
    timeline: Option<Timeline>,
}

impl<'a, 'd> Sigs<'a, 'd> {
    fn new(leaves: &'a LeafTable<'d>, rows: &'a Rows) -> Self {
        Sigs {
            leaves,
            rows,
            between: BTreeMap::new(),
            timeline: None,
        }
    }

    /// The leaf's value as the compiled predicate gives it: the 4-state value of
    /// the leaf expression with an `x` read as 0 (a Boolean context makes it
    /// false), or for a negated leaf (the gap of a goto repetition) `!expr` as a
    /// Boolean, so an `x` expression makes it false too.
    fn eval(
        &self,
        leaf: LeafId,
        tick: u32,
        frame: &[Option<i64>],
        table: &BTreeMap<String, Vec<i64>>,
    ) -> Result<i64, TraceError> {
        let v = self.raw(leaf, tick, frame, table)?;
        // A value leaf (a match item's right-hand side) is read as the integer it
        // is; only a Boolean guard is collapsed, and only a negated one (which is
        // always a guard) needs the 4-state negation first.
        Ok(if self.leaves.is_negated(leaf) {
            i64::from(not4(v) == 1)
        } else if v == X {
            0
        } else {
            v
        })
    }

    /// The 4-state value of the leaf's own expression (`x` is [`X`]).
    fn raw(
        &self,
        leaf: LeafId,
        tick: u32,
        frame: &[Option<i64>],
        table: &BTreeMap<String, Vec<i64>>,
    ) -> Result<i64, TraceError> {
        let sig = |name: &str, t: u32| -> i64 {
            table
                .get(name)
                .unwrap_or_else(|| panic!("the trace has no signal `{name}`"))[t as usize]
        };
        eval_leaf(
            self.leaves.get(leaf),
            self.leaves.locals_of(leaf),
            frame,
            tick,
            &sig,
        )
    }
}

impl PropEnv for Sigs<'_, '_> {
    fn value(&self, leaf: LeafId, tick: u32, frame: &[Option<i64>]) -> Result<i64, TraceError> {
        self.eval(leaf, tick, frame, self.rows)
    }

    fn case_match(
        &self,
        selector: LeafId,
        label: LeafId,
        tick: u32,
        frame: &[Option<i64>],
    ) -> Result<bool, TraceError> {
        let s = self.raw(selector, tick, frame, self.rows)?;
        let l = self.raw(label, tick, frame, self.rows)?;
        // 12.5 case equality: an `x`/`z` selector equals only the same `x`/`z`,
        // and no label here is one.
        Ok(s != X && s == l)
    }

    fn between(&self, leaf: LeafId, after: u32) -> Result<bool, TraceError> {
        if self.between.is_empty() {
            return Ok(false);
        }
        let frame: Vec<Option<i64>> = Vec::new();
        Ok(self.eval(leaf, after, &frame, &self.between)? != 0)
    }

    fn timeline(&self) -> Option<&Timeline> {
        self.timeline.as_ref()
    }
}

/// 4-state logical negation (11.4.7): `!x` is `x`.
fn not4(v: i64) -> i64 {
    if v == X { X } else { i64::from(v == 0) }
}

/// The value of the leaf expression `e`: signals from `sig(name, tick)`, a local
/// variable from the thread's `frame`. The subset of expressions the fixtures use;
/// anything else panics rather than guessing.
fn eval_leaf<'d>(
    e: Expression<'d>,
    locals: &LeafLocals<'d>,
    frame: &[Option<i64>],
    tick: u32,
    sig: &dyn Fn(&str, u32) -> i64,
) -> Result<i64, TraceError> {
    let kids = e.as_sem_node().children();
    let sub = |i: usize| -> Result<i64, TraceError> {
        let k = kids[i]
            .as_expression()
            .expect("an operand of a leaf expression is an expression");
        eval_leaf(k, locals, frame, tick, sig)
    };
    match e.kind() {
        ExpressionKind::IntegerLiteral => Ok(e
            .integer_literal_value()
            .and_then(|v| v.as_i64())
            .expect("an integer literal fits an i64")),
        ExpressionKind::NamedValue => {
            let sym = e.referenced_symbol().expect("a named value has a symbol");
            match locals.reads.iter().find(|(s, _)| *s == sym) {
                Some((_, slot)) => trace::read_local(frame, *slot),
                None => Ok(sig(sym.name(), tick)),
            }
        }
        ExpressionKind::LValueReference => trace::read_local(
            frame,
            locals
                .lvalue
                .expect("an LValueReference leaf has an lvalue"),
        ),
        ExpressionKind::Conversion => sub(0),
        ExpressionKind::UnaryOp => match e.unary_op() {
            Some(sv_lang::UnaryOp::LogicalNot) => Ok(not4(sub(0)?)),
            other => panic!("test evaluator: unary operator {other:?}"),
        },
        ExpressionKind::BinaryOp => {
            let (l, r) = (sub(0)?, sub(1)?);
            use sv_lang::BinaryOp as B;
            // 4-state (11.4): an `x` operand makes arithmetic, relational and
            // `==`/`!=` results `x`, `&&`/`||` follow Table 11-4, and only the
            // case operators compare `x` as a value.
            let ambiguous = l == X || r == X;
            let four = |v: i64| if ambiguous { X } else { v };
            match e.binary_op() {
                Some(B::Add) => Ok(four(l.wrapping_add(r))),
                Some(B::Subtract) => Ok(four(l.wrapping_sub(r))),
                Some(B::Equality) => Ok(four(i64::from(l == r))),
                Some(B::Inequality) => Ok(four(i64::from(l != r))),
                Some(B::CaseEquality) => Ok(i64::from(l == r)),
                Some(B::CaseInequality) => Ok(i64::from(l != r)),
                Some(B::GreaterThan) => Ok(four(i64::from(l > r))),
                Some(B::GreaterThanEqual) => Ok(four(i64::from(l >= r))),
                Some(B::LessThan) => Ok(four(i64::from(l < r))),
                Some(B::LessThanEqual) => Ok(four(i64::from(l <= r))),
                // A known zero decides `&&`; a known nonzero decides `||`.
                Some(B::LogicalAnd) => Ok(if l == 0 || r == 0 { 0 } else { four(1) }),
                Some(B::LogicalOr) => Ok(if (l != X && l != 0) || (r != X && r != 0) {
                    1
                } else {
                    four(0)
                }),
                Some(B::BinaryAnd) => Ok(if l == 0 || r == 0 { 0 } else { four(l & r) }),
                Some(B::BinaryOr) => Ok(four(l | r)),
                other => panic!("test evaluator: binary operator {other:?}"),
            }
        }
        other => panic!("test evaluator: expression kind {other:?}"),
    }
}

/// The verdict of `prop` on `signals` (a trace as long as every row) from `start`,
/// `strong` being a `cover property` directive's reading of a bare sequence.
fn verdict(decls: &str, prop: &str, signals: &[(&str, &str)], start: u32, strong: bool) -> Verdict {
    verdict_in(decls, prop, signals, start, strong, false)
}

/// [`verdict`] for a design that slang itself diagnoses (`allow_errors`).
fn verdict_in(
    decls: &str,
    prop: &str,
    signals: &[(&str, &str)],
    start: u32,
    strong: bool,
    allow_errors: bool,
) -> Verdict {
    let table = rows(signals);
    let len = table.values().next().expect("a signal").len() as u32;
    with_property(decls, &ap(prop), allow_errors, |r, _| {
        let (ir, leaves) = r.unwrap_or_else(|e| panic!("`{prop}` failed to build: {e}"));
        let env = Sigs::new(&leaves, &table);
        Evaluator::new(&ir, &env, strong)
            .verdict(len, start)
            .unwrap_or_else(|e| panic!("`{prop}` failed to evaluate: {e}"))
    })
}

/// `assert` reading, start tick 0.
fn assert_verdict(decls: &str, prop: &str, signals: &[(&str, &str)]) -> Verdict {
    verdict(decls, prop, signals, 0, false)
}

/// Every assignment of the boolean signals `names` over `len` ticks.
fn all_traces(names: &[&str], len: usize) -> Vec<Rows> {
    all_traces_over(names, len, &[0, 1])
}

/// [`all_traces`] with every sample drawn from `digits` (`[0, 1, X]` for the
/// 4-state traces).
fn all_traces_over(names: &[&str], len: usize, digits: &[i64]) -> Vec<Rows> {
    let base = digits.len() as u32;
    let cells = names.len() * len;
    (0..base.pow(cells as u32))
        .map(|m| {
            names
                .iter()
                .enumerate()
                .map(|(i, name)| {
                    (
                        name.to_string(),
                        (0..len)
                            .map(|t| digits[(m / base.pow((i * len + t) as u32) % base) as usize])
                            .collect(),
                    )
                })
                .collect()
        })
        .collect()
}

/// The verdict of `prop` over every trace of the boolean signals `names` of 1..=
/// `max_len` ticks, from every start tick, under both readings of a bare sequence,
/// as a flat list.
fn all_verdicts(decls: &str, prop: &str, names: &[&str], max_len: usize) -> Vec<Verdict> {
    all_verdicts_over(decls, prop, names, max_len, &[0, 1])
}

/// [`all_verdicts`] over traces whose samples come from `digits`.
fn all_verdicts_over(
    decls: &str,
    prop: &str,
    names: &[&str],
    max_len: usize,
    digits: &[i64],
) -> Vec<Verdict> {
    with_property(decls, &ap(prop), false, |r, _| {
        let (ir, leaves) = r.unwrap_or_else(|e| panic!("`{prop}` failed to build: {e}"));
        let mut out = Vec::new();
        for len in 1..=max_len {
            for table in all_traces_over(names, len, digits) {
                let env = Sigs::new(&leaves, &table);
                for strong in [false, true] {
                    let ev = Evaluator::new(&ir, &env, strong);
                    for start in 0..len as u32 {
                        out.push(
                            ev.verdict(len as u32, start)
                                .unwrap_or_else(|e| panic!("`{prop}` failed to evaluate: {e}")),
                        );
                    }
                }
            }
        }
        out
    })
}

/// `lhs` and `rhs` have the same verdict on every trace (see [`all_verdicts`]), and
/// that verdict is not the same everywhere (a degenerate comparison proves
/// nothing). Returns the verdicts.
fn equivalent(decls: &str, lhs: &str, rhs: &str, names: &[&str], max_len: usize) -> Vec<Verdict> {
    let l = all_verdicts(decls, lhs, names, max_len);
    let r = all_verdicts(decls, rhs, names, max_len);
    assert_eq!(l.len(), r.len());
    if let Some(i) = (0..l.len()).find(|&i| l[i] != r[i]) {
        panic!(
            "`{lhs}` and `{rhs}` differ at case #{i}: {:?} vs {:?}",
            l[i], r[i]
        );
    }
    assert!(
        l.iter().any(|v| *v != l[0]),
        "`{lhs}` has the same verdict ({:?}) on every trace: the comparison is vacuous",
        l[0]
    );
    l
}

/// `rec` (a recursive formulation) and `flat` (the operator it is documented to
/// be) hold on the same traces: they never differ in whether the property FAILS.
///
/// They are not the same verdict everywhere. A recursive property is `|=>` at
/// every step, and Annex F's `1 |=> p` is vacuous at the last real tick (the
/// antecedent `1 ##1 1` cannot match through the `⊥` letters of the strong tail),
/// so the recursion holds STRONGLY on a trace where the operator it spells only
/// holds (`always p` has `p` owed on every `⊥` letter, F.5.1). `rec` may be
/// stronger than `flat`, never weaker and never differently failing.
fn weakly_equivalent(decls: &str, rec: &str, flat: &str, names: &[&str], max_len: usize) {
    let r = all_verdicts(decls, rec, names, max_len);
    let f = all_verdicts(decls, flat, names, max_len);
    assert_eq!(r.len(), f.len());
    for i in 0..r.len() {
        assert!(
            r[i] == f[i] || (r[i] == Verdict::HoldsStrongly && f[i] == Verdict::Holds),
            "`{rec}` and `{flat}` differ at case #{i}: {:?} vs {:?}",
            r[i],
            f[i]
        );
    }
    assert!(
        f.contains(&Verdict::Fails) && f.iter().any(|v| *v != Verdict::Fails),
        "`{flat}` fails on every trace or on none: the comparison is vacuous"
    );
}

/// The source text of every leaf, by `LeafId`.
fn leaf_texts(leaves: &LeafTable<'_>, tree: &SyntaxTree) -> Vec<String> {
    (0..leaves.len() as u32)
        .map(|i| {
            let e = leaves.get(LeafId(i));
            match e.syntax(tree) {
                Some(n) => n.text().split_whitespace().collect::<Vec<_>>().join(""),
                None => format!("<{:?}>", e.kind()),
            }
        })
        .collect()
}

// -- T19: sequence properties, strong/weak, nondegeneracy, typed formals --------

/// 16.12.2: a sequence used as a property is weak under `assert`/`assume` and
/// strong under `cover`. On an unbounded delay `a ##[1:$] b` no finite trace
/// refutes either reading, and neither has matched yet, so both are pending
/// (`Holds`: nothing failed yet) until the match arrives -- Table 40-3 `aundf`:
/// the weak attempt neither passes nor fails, it is not a pass at its first tick.
/// Likewise on a bounded sequence cut short.
#[test]
fn t19_bare_sequence_is_weak_under_assert_and_strong_under_cover() {
    let never_b = &[("a", "100"), ("b", "000")];
    assert_eq!(
        verdict("", "a ##[1:$] b", never_b, 0, false),
        Verdict::Holds,
        "assert: weak, no finite prefix refutes it but nothing matched yet"
    );
    assert_eq!(
        verdict("", "a ##[1:$] b", never_b, 0, true),
        Verdict::Holds,
        "cover: strong, the match is still owed"
    );
    // The match is there: both readings hold strongly.
    let hit = &[("a", "100"), ("b", "001")];
    assert_eq!(
        verdict("", "a ##[1:$] b", hit, 0, false),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        verdict("", "a ##[1:$] b", hit, 0, true),
        Verdict::HoldsStrongly
    );
    // The bounded sequence is pending when the trace ends after its first letter,
    // and refuted when its delay window closes without the match, either way.
    let cut = &[("b", "1"), ("c", "0")];
    assert_eq!(verdict("", "b ##1 c", cut, 0, false), Verdict::Holds);
    assert_eq!(verdict("", "b ##1 c", cut, 0, true), Verdict::Holds);
    let bad = &[("b", "10"), ("c", "00")];
    assert_eq!(verdict("", "b ##1 c", bad, 0, false), Verdict::Fails);
    assert_eq!(verdict("", "b ##1 c", bad, 0, true), Verdict::Fails);
    let full = &[("b", "10"), ("c", "01")];
    assert_eq!(
        verdict("", "b ##1 c", full, 0, false),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        verdict("", "b ##1 c", full, 0, true),
        Verdict::HoldsStrongly
    );
}

/// 16.12.2: `strong(seq)` and `weak(seq)` fix the strength whatever the directive
/// says, and parentheses around either are transparent.
#[test]
fn t19_strong_and_weak_ignore_the_directive() {
    let sig = &[("a", "100"), ("b", "000")];
    for cover in [false, true] {
        for text in ["strong(a ##[1:$] b)", "(strong(a ##[1:$] b))"] {
            assert_eq!(
                verdict("", text, sig, 0, cover),
                Verdict::Holds,
                "{text} needs its match (cover={cover})"
            );
        }
        for text in ["weak(a ##[1:$] b)", "((weak(a ##[1:$] b)))"] {
            assert_eq!(
                verdict("", text, sig, 0, cover),
                Verdict::Holds,
                "{text} is only refutable, not yet matched (cover={cover})"
            );
        }
    }
    let hit = &[("a", "100"), ("b", "001")];
    assert_eq!(
        verdict("", "strong(a ##[1:$] b)", hit, 0, false),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        verdict("", "weak(a ##[1:$] b)", hit, 0, false),
        Verdict::HoldsStrongly
    );
    // A bounded strong sequence whose window closes unmatched fails outright.
    let miss = &[("a", "1000"), ("b", "0001")];
    assert_eq!(
        verdict("", "strong(a ##[1:2] b)", miss, 0, false),
        Verdict::Fails
    );
}

/// 16.12.2: a sequence property holds when SOME match exists.
#[test]
fn t19_sequence_property_holds_on_any_match() {
    let sig = &[("a", "1000"), ("b", "0010")];
    assert_eq!(
        verdict("", "a ##[1:3] b", sig, 0, false),
        Verdict::HoldsStrongly
    );
    // The window is `##[1:2]`: b at tick 2 still lands.
    assert_eq!(
        verdict("", "a ##[1:2] b", sig, 0, false),
        Verdict::HoldsStrongly
    );
    // `##1` misses it: refuted.
    assert_eq!(verdict("", "a ##1 b", sig, 0, false), Verdict::Fails);
    // The trace ends inside the window: pending under either reading.
    let cut = &[("a", "100"), ("b", "000")];
    assert_eq!(verdict("", "a ##[1:5] b", cut, 0, false), Verdict::Holds);
    assert_eq!(verdict("", "a ##[1:5] b", cut, 0, true), Verdict::Holds);
    // A start tick other than 0: the attempt at tick 1 sees `a` false.
    assert_eq!(verdict("", "a ##1 b", sig, 1, false), Verdict::Fails);
}

/// 16.12.22 (a): a sequence used as a property shall be nondegenerate and shall
/// not admit any empty match. The LRM's own examples: `(1'b1) intersect (1'b1 ##1
/// 1'b1)` never matches (the operands have different lengths), `1'b1[*0]` admits
/// only the empty match and `a[*0:2]` admits both.
#[test]
fn t19_nondegeneracy_of_a_sequence_property() {
    let never = rejected_lenient("", "(1'b1) intersect (1'b1 ##1 1'b1)");
    assert!(never.contains("16.12.22"), "{never}");
    assert!(never.contains("never match"), "{never}");

    let empty_only = rejected_lenient("", "1'b1[*0]");
    assert!(empty_only.contains("16.12.22"), "{empty_only}");
    assert!(empty_only.contains("only the empty match"), "{empty_only}");

    let both = rejected_lenient("", "a[*0:2]");
    assert!(both.contains("16.12.22"), "{both}");
    assert!(both.contains("empty match"), "{both}");

    // The same rule through `strong(...)`/`weak(...)`.
    for text in ["strong(a[*0:2])", "weak(a[*0:2])", "weak(1'b1[*0])"] {
        let msg = rejected_lenient("", text);
        assert!(msg.contains("16.12.22"), "{text}: {msg}");
    }

    // Nondegenerate ones build. `1'b0` is a Boolean and degeneracy is structural
    // (16.12.22), so it is not rejected; neither is a repetition that cannot be
    // empty or an `a ##0 b`.
    for text in [
        "a[*1:2]",
        "a ##1 b",
        "1'b0",
        "a[*2]",
        "a ##0 b",
        "a[->1]",
        "(a[*0:2]) ##1 b",
    ] {
        builds("", text);
    }
}

/// 16.12.2: `1'b0` is a Boolean, not a degenerate sequence, so it is a property
/// that is false at its start.
#[test]
fn t19_constant_false_boolean_is_a_failing_property() {
    let sig = &[("a", "1")];
    assert_eq!(assert_verdict("", "1'b0", sig), Verdict::Fails);
    assert_eq!(assert_verdict("", "1'b1", sig), Verdict::HoldsStrongly);
}

/// 16.12.18: a property formal may be untyped, `sequence`, `property` or a data
/// type, and a `local input` data formal is initialised from its actual.
#[test]
fn t19_typed_property_formals() {
    // `property` formal bound to a sequence expression.
    let decls = "property p(property q); q; endproperty";
    assert_eq!(
        assert_verdict(decls, "p(a ##1 b)", &[("a", "10"), ("b", "01")]),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        assert_verdict(decls, "p(a ##1 b)", &[("a", "10"), ("b", "00")]),
        Verdict::Fails
    );

    // `sequence` formal.
    let decls = "property p(sequence s); s; endproperty";
    assert_eq!(
        assert_verdict(decls, "p(a ##2 b)", &[("a", "100"), ("b", "001")]),
        Verdict::HoldsStrongly
    );

    // Untyped formal in a sequence position.
    let decls = "property p(x1); x1 ##1 b; endproperty";
    assert_eq!(
        assert_verdict(decls, "p(a)", &[("a", "10"), ("b", "01")]),
        Verdict::HoldsStrongly
    );

    // A data-typed formal, folded into the delay of the body (a constant).
    let decls = "property p(int k); a ##k b; endproperty";
    assert_eq!(
        assert_verdict(decls, "p(2)", &[("a", "100"), ("b", "001")]),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        assert_verdict(decls, "p(1)", &[("a", "100"), ("b", "001")]),
        Verdict::Fails
    );

    // A property formal bound to a NAMED property: the actual is a property
    // instance, and the formal's reference expands to it.
    let decls = "property inner; a ##1 b; endproperty\n\
                 property p(property q); q; endproperty";
    assert_eq!(
        assert_verdict(decls, "p(inner)", &[("a", "10"), ("b", "01")]),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        assert_verdict(decls, "p(inner)", &[("a", "10"), ("b", "00")]),
        Verdict::Fails
    );

    // A named property with no formals at all.
    let decls = "property p; a ##1 b; endproperty";
    assert_eq!(
        assert_verdict(decls, "p", &[("a", "10"), ("b", "01")]),
        Verdict::HoldsStrongly
    );
}

/// 16.12.19: a `local input` formal of a property is initialised from its actual
/// when the property is evaluated, and a declared local variable is initialised from
/// its initialiser. The IR holds both as one `Let` around the body.
#[test]
fn t19_local_input_formal_and_declared_local_initialisation() {
    let decls = "property p(local input int v); a ##1 (n == v); endproperty";
    with_property(decls, &ap("p(3)"), false, |r, tree| {
        let (ir, leaves) = r.unwrap();
        let Prop::Let { writes, .. } = ir.prop(ir.root) else {
            panic!("the instance with a local formal is a Let: {:?}", ir.props);
        };
        assert_eq!(writes.len(), 1);
        assert_eq!(leaf_texts(&leaves, tree)[writes[0].1.0 as usize], "3");
    });
    assert_eq!(
        assert_verdict(decls, "p(3)", &[("a", "10"), ("n", "03")]),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        assert_verdict(decls, "p(3)", &[("a", "10"), ("n", "04")]),
        Verdict::Fails
    );

    // The initialiser of a declared local runs after the formals' writes.
    let decls = "property p(local input int f); int v = f + 1; a ##1 (n == v); endproperty";
    assert_eq!(
        assert_verdict(decls, "p(7)", &[("a", "10"), ("n", "08")]),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        assert_verdict(decls, "p(7)", &[("a", "10"), ("n", "07")]),
        Verdict::Fails
    );
}

/// 16.12.19 / 16.10: a local variable of a property assigned by a match item inside
/// a sequence is visible to the rest of that sequence.
#[test]
fn t19_local_variable_assigned_inside_the_property_sequence() {
    let decls = "property p; int v; (a, v = n) ##1 (n == v + 1); endproperty";
    assert_eq!(
        assert_verdict(decls, "p", &[("a", "10"), ("n", "45")]),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        assert_verdict(decls, "p", &[("a", "10"), ("n", "44")]),
        Verdict::Fails
    );
}

/// The compile diagnostics slang renders for `decls` + `prop`.
fn slang_errors(decls: &str, prop: &str) -> String {
    let src = format!(
        "module m;\nlogic clk, a, b;\nint n;\n{decls}\nalways_ff @(posedge clk) begin\n{}\nend\nendmodule\n",
        ap(prop)
    );
    let session = Session::new();
    let mut comp = Compilation::new(&session).unwrap();
    comp.add_source(&src).unwrap();
    let design = comp.compile().unwrap();
    design.diagnostics().rendered().to_string()
}

/// 16.12.19: the local variable formals of a property are inputs. slang enforces
/// it at the declaration, so the design never reaches the builder; the builder's
/// own check (for a tree slang let through) is exercised by construction only.
#[test]
fn t19_local_formal_of_a_property_must_be_input() {
    let msg = slang_errors("property p(local output int v); a; endproperty", "p(n)");
    assert!(
        msg.contains("error"),
        "slang accepted a local output formal: {msg:?}"
    );
}

/// A `disable iff` in the declaration of a property instantiated as the whole
/// property spec is the spec's `disable iff` (T27): it builds, and the condition is
/// recorded rather than dropped. (The full set of T27 tests is in `disable`.)
#[test]
fn t19_disable_iff_inside_a_property_is_the_specs_disable_iff() {
    with_property(
        "property p; disable iff (reset) a ##1 b; endproperty",
        &ap("p"),
        false,
        |r, _| {
            let (ir, _) = r.expect("`p` builds");
            assert!(
                ir.disable.is_some(),
                "the `disable iff` condition was dropped"
            );
        },
    );
}

// -- T20: not / or / and / if-else / case (16.12.3-6, 16.12.16) -----------------

/// 16.12.3: `not p` evaluates to the opposite of `p`.
#[test]
fn t20_not_is_the_opposite() {
    assert_eq!(assert_verdict("", "not a", &[("a", "1")]), Verdict::Fails);
    assert_eq!(
        assert_verdict("", "not a", &[("a", "0")]),
        Verdict::HoldsStrongly
    );
    // A property under `not`: `not (if (a) b)` holds exactly where `a` is true and
    // `b` is not.
    assert_eq!(
        assert_verdict("", "not (if (a) b)", &[("a", "1"), ("b", "0")]),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        assert_verdict("", "not (if (a) b)", &[("a", "1"), ("b", "1")]),
        Verdict::Fails
    );
    assert_eq!(
        assert_verdict("", "not (if (a) b)", &[("a", "0"), ("b", "1")]),
        Verdict::Fails
    );
    // Negation is involutive on every trace.
    equivalent("", "not not (a ##1 b)", "a ##1 b", &["a", "b"], 3);
    equivalent(
        "",
        "not not (if (a) (b ##1 c))",
        "if (a) (b ##1 c)",
        &["a", "b", "c"],
        3,
    );
}

/// 16.12.3: "The not operator switches the strength of a property": negating a
/// WEAK sequential property gives a strong one and the other way round, so the
/// advice is `not strong(a ##[1:$] b)` where a failure of `a ##[1:$] b` is meant.
///
/// Worked out from F.5.3.1/F.5.3.2 on the trace `a=1,0,0 / b=0,0,0`: the weak
/// verdict of `not P` is the negation of the STRONG-tail verdict of `P` and vice
/// versa. `weak(a ##[1:$] b)` holds on `a 0 0 ⊥^ω` (every cut can still be matched
/// by a later `b`, `⊤`s, F.5.3.1), so the weak verdict of `not (a ##[1:$] b)`
/// is false: the assertion FAILS at once, the pitfall of the LRM's `a1`. But
/// `strong(a ##[1:$] b)` does not hold on the `⊥` tail, so `not strong(...)`
/// holds weakly and is only pending (its strong verdict needs the `⊤` tail to
/// refute, which it does not): `Holds`.
#[test]
fn t20_not_switches_the_strength_of_a_sequence() {
    let sig = &[("a", "100"), ("b", "000")];
    assert_eq!(
        verdict("", "not (a ##[1:$] b)", sig, 0, false),
        Verdict::Fails
    );
    assert_eq!(
        verdict("", "not strong(a ##[1:$] b)", sig, 0, false),
        Verdict::Holds
    );
    // The weak form negated is the strong form negated plus the failure above: the
    // two differ on some trace, never the other way round, so `not strong` is
    // never the stricter of the two.
    let weak = all_verdicts("", "not (a ##[1:$] b)", &["a", "b"], 3);
    let strong = all_verdicts("", "not strong(a ##[1:$] b)", &["a", "b"], 3);
    assert_eq!(weak.len(), strong.len());
    assert!(weak.iter().zip(&strong).any(|(w, s)| w != s));
    // `not` of a bounded sequence is judged the same either way by Annex F: the
    // `⊥` letter refutes `weak(a ##1 b)` as it does `strong(a ##1 b)`.
    equivalent("", "not (a ##1 b)", "not strong(a ##1 b)", &["a", "b"], 3);
}

/// 16.12.4/16.12.5: `or`/`and` of two properties; De Morgan holds through `not`.
#[test]
fn t20_and_or_of_properties() {
    for (text, a, b, want) in [
        ("(not a) or (not b)", "1", "1", Verdict::Fails),
        ("(not a) or (not b)", "1", "0", Verdict::HoldsStrongly),
        ("(not a) or (not b)", "0", "1", Verdict::HoldsStrongly),
        ("(not a) or (not b)", "0", "0", Verdict::HoldsStrongly),
        ("(not a) and (not b)", "1", "0", Verdict::Fails),
        ("(not a) and (not b)", "0", "1", Verdict::Fails),
        ("(not a) and (not b)", "0", "0", Verdict::HoldsStrongly),
    ] {
        assert_eq!(
            assert_verdict("", text, &[("a", a), ("b", b)]),
            want,
            "{text} at a={a} b={b}"
        );
    }
    equivalent("", "(not a) and (not b)", "not (a or b)", &["a", "b"], 3);
    equivalent(
        "",
        "(if (a) b) and (if (c) d)",
        "not ((not (if (a) b)) or (not (if (c) d)))",
        &["a", "b", "c", "d"],
        3,
    );
    // `or` is a sequence operator when both operands are sequences and a property
    // operator when one is a property; mixing the two is a property `or` whose
    // sequence operand is a sequence property.
    equivalent(
        "",
        "(a ##1 b) or (not c)",
        "(not c) or (a ##1 b)",
        &["a", "b", "c"],
        3,
    );
}

/// 16.12.6: `if (c) p` is true if `c` is false or `p` holds; `if (c) p else q`
/// takes the branch `c` selects at the START tick.
#[test]
fn t20_if_else_property() {
    let decls = "";
    // c false: `if` without `else` is vacuously true.
    assert_eq!(
        assert_verdict(
            decls,
            "if (a) (b ##1 c)",
            &[("a", "0"), ("b", "00"), ("c", "00")]
        ),
        Verdict::HoldsStrongly
    );
    // c true, `b ##1 c` holds.
    assert_eq!(
        assert_verdict(
            decls,
            "if (a) (b ##1 c)",
            &[("a", "10"), ("b", "10"), ("c", "01")]
        ),
        Verdict::HoldsStrongly
    );
    // c true, the branch fails.
    assert_eq!(
        assert_verdict(
            decls,
            "if (a) (b ##1 c)",
            &[("a", "10"), ("b", "10"), ("c", "00")]
        ),
        Verdict::Fails
    );
    // else branch taken when the condition is false.
    assert_eq!(
        assert_verdict(
            decls,
            "if (a) (b ##1 c) else (d ##1 e)",
            &[
                ("a", "00"),
                ("b", "10"),
                ("c", "01"),
                ("d", "10"),
                ("e", "00")
            ]
        ),
        Verdict::Fails
    );
    assert_eq!(
        assert_verdict(
            decls,
            "if (a) (b ##1 c) else (d ##1 e)",
            &[
                ("a", "00"),
                ("b", "00"),
                ("c", "00"),
                ("d", "10"),
                ("e", "01")
            ]
        ),
        Verdict::HoldsStrongly
    );
    // The condition is read at the start tick only: a true at tick 1 does not
    // select the `then` branch of an attempt started at tick 0.
    assert_eq!(
        assert_verdict(
            decls,
            "if (a) (b ##1 c) else (d ##1 e)",
            &[
                ("a", "01"),
                ("b", "00"),
                ("c", "00"),
                ("d", "10"),
                ("e", "01")
            ]
        ),
        Verdict::HoldsStrongly
    );
    // The F.3.4.3 rewrite: `if (c) p else q` is `(c and p) or (not c and q)`... with
    // the Boolean `c` read as a property.
    equivalent(
        "",
        "if (a) (b ##1 c) else (not b)",
        "(a and (b ##1 c)) or ((not a) and (not b))",
        &["a", "b", "c"],
        3,
    );
    equivalent("", "if (a) (not b)", "(not a) or (not b)", &["a", "b"], 3);
}

/// 16.12.16 `p_delay`: a delay decoded from a 2-bit variable, `default: 0` failing
/// on an `x`/`z` selector.
#[test]
fn t20_case_p_delay() {
    let decls = "property p_delay(logic [1:0] delay);\n\
                 case (delay)\n\
                 2'd0   : a && b;\n\
                 2'd1   : a ##2 b;\n\
                 2'd2   : a ##4 b;\n\
                 2'd3   : a ##8 b;\n\
                 default: 0;\n\
                 endcase\n\
                 endproperty";
    let run = |dly: char, a: &str, b: &str| {
        let n = a.len();
        let d: String = std::iter::repeat_n(dly, n).collect();
        assert_verdict(decls, "p_delay(dly)", &[("dly", &d), ("a", a), ("b", b)])
    };
    // delay 0: a && b at the start tick.
    assert_eq!(run('0', "1", "1"), Verdict::HoldsStrongly);
    assert_eq!(run('0', "10", "01"), Verdict::Fails);
    // delay 1 is `a ##2 b`.
    assert_eq!(run('1', "100", "001"), Verdict::HoldsStrongly);
    assert_eq!(run('1', "100", "010"), Verdict::Fails);
    // delay 2 is `a ##4 b`, delay 3 is `a ##8 b`.
    assert_eq!(run('2', "10000", "00001"), Verdict::HoldsStrongly);
    assert_eq!(run('2', "10000", "00100"), Verdict::Fails);
    assert_eq!(run('3', "100000000", "000000001"), Verdict::HoldsStrongly);
    assert_eq!(run('3', "100000000", "000010000"), Verdict::Fails);
    // `default: 0` makes an x selector a failure (case equality, 12.5).
    assert_eq!(run('x', "1", "1"), Verdict::Fails);
    // The selector is read at the start tick of the attempt: an attempt started
    // at tick 1 sees `dly == 0` there and wants `a && b` at tick 1, whatever the
    // selector was at tick 0.
    let table = &[("dly", "10"), ("a", "01"), ("b", "01")];
    assert_eq!(
        verdict(decls, "p_delay(dly)", table, 1, false),
        Verdict::HoldsStrongly
    );
    let table = &[("dly", "10"), ("a", "01"), ("b", "00")];
    assert_eq!(
        verdict(decls, "p_delay(dly)", table, 1, false),
        Verdict::Fails
    );
}

/// 16.12.16: with no `default` and no matching item the case is vacuously true; the
/// first matching item wins and a later one is never evaluated.
#[test]
fn t20_case_without_default_and_first_match() {
    let decls = "";
    let prop = "case (dly) 2'd0: a; 2'd1: b; endcase";
    let sig = |dly: &'static str, a: &'static str, b: &'static str| {
        assert_verdict(decls, prop, &[("dly", dly), ("a", a), ("b", b)])
    };
    assert_eq!(sig("0", "1", "0"), Verdict::HoldsStrongly);
    assert_eq!(sig("0", "0", "1"), Verdict::Fails);
    assert_eq!(sig("1", "0", "1"), Verdict::HoldsStrongly);
    assert_eq!(sig("1", "1", "0"), Verdict::Fails);
    // 2 and 3 match no item: vacuously true; so is an x selector.
    assert_eq!(sig("2", "0", "0"), Verdict::HoldsStrongly);
    assert_eq!(sig("3", "0", "0"), Verdict::HoldsStrongly);
    assert_eq!(sig("x", "0", "0"), Verdict::HoldsStrongly);
    // Several labels on one item; the first matching ITEM is taken even when a
    // later item also lists the value.
    let prop = "case (dly) 2'd0, 2'd2: a; 2'd2: b; default: 0; endcase";
    let sig = |dly: &'static str, a: &'static str, b: &'static str| {
        assert_verdict(decls, prop, &[("dly", dly), ("a", a), ("b", b)])
    };
    assert_eq!(sig("2", "1", "0"), Verdict::HoldsStrongly, "item 0 wins");
    assert_eq!(sig("2", "0", "1"), Verdict::Fails, "item 0 wins");
    assert_eq!(sig("3", "1", "1"), Verdict::Fails, "default");
}

/// 16.12.16: the `case` property is the if/else chain of its items, so a
/// sequence body keeps its ##-delays across the arms.
#[test]
fn t20_case_equals_the_if_chain() {
    equivalent(
        "",
        "case (a) 1: (b ##1 c); default: (not b); endcase",
        "if (a == 1) (b ##1 c) else (not b)",
        &["a", "b", "c"],
        3,
    );
}

// -- T21: implication and followed-by (16.12.7, 16.12.9) ------------------------

/// 16.12.7: with no match of the antecedent the implication is true; for a match
/// the consequent starts at the match's end point (overlapped), so a Boolean
/// consequent is read on the very tick the antecedent ends.
#[test]
fn t21_overlapped_implication_truth_table() {
    for (a, b, want) in [
        ("0", "0", Verdict::HoldsStrongly),
        ("0", "1", Verdict::HoldsStrongly),
        ("1", "1", Verdict::HoldsStrongly),
        ("1", "0", Verdict::Fails),
    ] {
        assert_eq!(
            assert_verdict("", "a |-> b", &[("a", a), ("b", b)]),
            want,
            "a |-> b at a={a} b={b}"
        );
    }
    // A consequent that has not finished when the trace stops is pending, not failed.
    assert_eq!(
        assert_verdict("", "a |-> ##1 b", &[("a", "1"), ("b", "0")]),
        Verdict::Holds
    );
    assert_eq!(
        assert_verdict("", "a |-> ##1 b", &[("a", "10"), ("b", "01")]),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        assert_verdict("", "a |-> ##1 b", &[("a", "10"), ("b", "00")]),
        Verdict::Fails
    );
}

/// 16.12.7 (Figure 16-14's `data_end`): the consequent `##[1:5] b` starts at the
/// match of the antecedent and succeeds when `b` shows up in the window.
#[test]
fn t21_data_end_window() {
    let decls = "property data_end; a |-> ##[1:5] b; endproperty";
    let a = "01000000";
    // The attempt that starts at tick 1 (the antecedent holds there): the window is
    // ticks 2..=6.
    for (b, want) in [
        ("00000010", Verdict::HoldsStrongly),
        ("00100000", Verdict::HoldsStrongly),
        ("00000001", Verdict::Fails),
        ("01000000", Verdict::Fails),
    ] {
        assert_eq!(
            verdict(decls, "data_end", &[("a", a), ("b", b)], 1, false),
            want,
            "b = {b}"
        );
    }
    // An attempt whose antecedent is false succeeds vacuously, whatever `b` does.
    assert_eq!(
        verdict(decls, "data_end", &[("a", a), ("b", "00000000")], 0, false),
        Verdict::HoldsStrongly
    );
}

/// 16.12.7: "for every match of the antecedent ... the evaluation of the consequent
/// beginning at the end point of the match succeeds": every match is checked
/// separately, at its own end point.
#[test]
fn t21_every_antecedent_match_is_checked() {
    let decls = "";
    let prop = "(a ##[1:2] b) |-> c";
    let sig = |a: &'static str, b: &'static str, c: &'static str| {
        assert_verdict(decls, prop, &[("a", a), ("b", b), ("c", c)])
    };
    // Matches end at ticks 1 and 2.
    assert_eq!(sig("1000", "0110", "0110"), Verdict::HoldsStrongly);
    assert_eq!(sig("1000", "0110", "0100"), Verdict::Fails);
    assert_eq!(sig("1000", "0110", "0010"), Verdict::Fails);
    // A single match.
    assert_eq!(sig("1000", "0010", "0010"), Verdict::HoldsStrongly);
    // The antecedent never matches.
    assert_eq!(sig("1000", "0001", "0000"), Verdict::HoldsStrongly);
    // The LRM's own pair, `(a ##1 b ##1 c) |-> (d ##1 e)`.
    let prop = "(a ##1 b ##1 c) |-> (d ##1 e)";
    let sig = |d: &'static str, e: &'static str, b: &'static str| {
        assert_verdict(
            decls,
            prop,
            &[("a", "1000"), ("b", b), ("c", "0010"), ("d", d), ("e", e)],
        )
    };
    assert_eq!(sig("0010", "0001", "0100"), Verdict::HoldsStrongly);
    assert_eq!(sig("0010", "0000", "0100"), Verdict::Fails);
    // "if the sequence does not match, the result is true".
    assert_eq!(sig("0000", "0000", "0000"), Verdict::HoldsStrongly);
}

/// 16.12.7: for `|=>` the consequent starts on the tick after a nonempty match;
/// an empty match triggers it on the start tick itself, and
/// `s |=> p` is `s ##1 `true |-> p`.
#[test]
fn t21_nonoverlapped_implication() {
    let decls = "";
    for (a, b, want) in [
        ("10", "01", Verdict::HoldsStrongly),
        ("10", "10", Verdict::Fails),
        ("10", "00", Verdict::Fails),
        ("00", "00", Verdict::HoldsStrongly),
    ] {
        assert_eq!(
            assert_verdict(decls, "a |=> b", &[("a", a), ("b", b)]),
            want,
            "a |=> b at a={a} b={b}"
        );
    }
    // The tick after the match does not exist yet: nothing has been violated and
    // `##1 1` has not matched, so the implication holds (`a ##1 1` needs a tick).
    assert_eq!(
        assert_verdict(decls, "a |=> b", &[("a", "1"), ("b", "0")]),
        Verdict::HoldsStrongly
    );
    // The documented equivalence, on every trace, for several antecedents (one of
    // them admitting the empty match, whose consequent starts on the start tick) and
    // several consequents.
    for ante in ["a", "a ##[1:2] b", "a[*0:1]", "a[*0:1] ##1 b", "a ##0 b"] {
        for cons in ["c", "b ##1 c", "not c", "if (b) c"] {
            let rewritten = format!("{ante} ##1 1'b1 |-> {cons}");
            let direct = format!("{ante} |=> {cons}");
            equivalent(decls, &direct, &rewritten, &["a", "b", "c"], 3);
        }
    }
}

/// 16.12.7: the two nested spellings of `write_to_addr` are the same property,
/// and `|->` is right associative.
#[test]
fn t21_nested_implication() {
    let decls = "";
    equivalent(
        decls,
        "(a & b) ##0 c[*2] |-> ##[1:2] d",
        "(a & b) |-> c[*2] |-> ##[1:2] d",
        &["a", "b", "c", "d"],
        4,
    );
    equivalent(
        decls,
        "a |-> b |-> c",
        "a |-> (b |-> c)",
        &["a", "b", "c"],
        3,
    );
    // The nest means "a ##0 b |-> c" and "a ##1 b |-> c" for `|->`/`|=>`.
    equivalent(
        decls,
        "a |-> (b |-> c)",
        "(a ##0 b) |-> c",
        &["a", "b", "c"],
        3,
    );
    equivalent(
        decls,
        "a |=> (b |-> c)",
        "(a ##1 b) |-> c",
        &["a", "b", "c"],
        3,
    );
}

/// 16.12.9: followed-by requires a match (an implication without one is
/// vacuously true), and the consequent must hold from ONE of the matches.
#[test]
fn t21_followed_by() {
    let decls = "";
    // No match of the antecedent: `|->` is true, `#-#` is false.
    assert_eq!(
        assert_verdict(decls, "a |-> b", &[("a", "0"), ("b", "0")]),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        assert_verdict(decls, "a #-# b", &[("a", "0"), ("b", "1")]),
        Verdict::Fails
    );
    assert_eq!(
        assert_verdict(decls, "a #-# b", &[("a", "1"), ("b", "1")]),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        assert_verdict(decls, "a #-# b", &[("a", "1"), ("b", "0")]),
        Verdict::Fails
    );
    // One of two matches suffices (`|->` would need both).
    let prop = "(a ##[1:2] b) #-# c";
    let sig =
        |c: &'static str| assert_verdict(decls, prop, &[("a", "1000"), ("b", "0110"), ("c", c)]);
    assert_eq!(sig("0010"), Verdict::HoldsStrongly);
    assert_eq!(sig("0100"), Verdict::HoldsStrongly);
    assert_eq!(sig("0000"), Verdict::Fails);
    assert_eq!(
        assert_verdict(
            decls,
            "(a ##[1:2] b) |-> c",
            &[("a", "1000"), ("b", "0110"), ("c", "0010")]
        ),
        Verdict::Fails
    );
    // `#=#`: the consequent starts one tick after the match.
    for (a, b, want) in [
        ("10", "01", Verdict::HoldsStrongly),
        ("10", "10", Verdict::Fails),
        ("00", "01", Verdict::Fails),
    ] {
        assert_eq!(
            assert_verdict(decls, "a #=# b", &[("a", a), ("b", b)]),
            want,
            "a #=# b at a={a} b={b}"
        );
    }
}

/// 16.12.9: the followed-by operators are the duals of the implication operators.
#[test]
fn t21_followed_by_is_the_dual_of_implication() {
    let decls = "";
    for ante in ["a", "a ##[1:2] b", "a[*0:1] ##1 b"] {
        for cons in ["c", "c ##1 d", "if (c) d"] {
            equivalent(
                decls,
                &format!("{ante} #-# {cons}"),
                &format!("not ({ante} |-> not ({cons}))"),
                &["a", "b", "c", "d"],
                3,
            );
            equivalent(
                decls,
                &format!("{ante} #=# {cons}"),
                &format!("not ({ante} |=> not ({cons}))"),
                &["a", "b", "c", "d"],
                3,
            );
        }
    }
    // And a followed-by is NOT an implication: they differ where the antecedent
    // never matches.
    let l = all_verdicts(decls, "a #-# b", &["a", "b"], 2);
    let r = all_verdicts(decls, "a |-> b", &["a", "b"], 2);
    assert!(l.iter().zip(&r).any(|(x, y)| x != y));
}

/// 16.12.9: `s #-# strong(s1)` is `strong(s ##0 s1)` and `s #=# strong(s1)` is
/// `strong(s ##1 s1)`, empty antecedent matches included.
///
/// The two spellings agree on every trace EXCEPT while the antecedent is still
/// pending when the trace stops. There the evaluator follows Annex F.3.4.3.6
/// literally, `r #-# p` is `not (r |-> not p)`: on the strong (`⊥`) tail the
/// antecedent cannot finish, the implication is vacuously true and its negation
/// FAILS, whereas `strong(r ##0 s1)` is merely pending (it holds, not strongly).
/// The LRM's two statements disagree on that finite prefix; the equivalence is exact
/// on complete words, which is what the clause describes. The test pins both halves:
/// every difference is that exact (Fails, Holds) pair, and a `strong(...)` verdict
/// that is not pending is always matched.
#[test]
fn t21_followed_by_of_a_strong_sequence() {
    let decls = "";
    let names = ["a", "b", "c", "d"];
    let mut pending_corner = 0;
    for ante in ["a", "a ##1 b", "a ##[1:2] b", "a[*0:1]"] {
        for cons in ["c", "c ##[1:2] d"] {
            for (op, gap) in [("#-#", "##0"), ("#=#", "##1")] {
                let fb = format!("{ante} {op} strong({cons})");
                let st = format!("strong({ante} {gap} {cons})");
                let l = all_verdicts(decls, &fb, &names, 3);
                let r = all_verdicts(decls, &st, &names, 3);
                assert_eq!(l.len(), r.len());
                for (i, (x, y)) in l.iter().zip(&r).enumerate() {
                    if x != y {
                        assert_eq!(
                            (*x, *y),
                            (Verdict::Fails, Verdict::Holds),
                            "`{fb}` and `{st}` differ at case #{i} other than in the pending corner"
                        );
                        pending_corner += 1;
                    }
                }
                assert!(
                    l.iter().any(|v| *v != l[0]),
                    "`{fb}` has the same verdict on every trace"
                );
            }
        }
    }
    assert!(pending_corner > 0, "the pending corner is documented above");
    // The corner, concretely: the antecedent `a ##1 b` needs a tick the trace lacks.
    let sig = &[("a", "1"), ("b", "0"), ("c", "0")];
    assert_eq!(
        assert_verdict(decls, "a ##1 b #-# strong(c)", sig),
        Verdict::Fails
    );
    assert_eq!(
        assert_verdict(decls, "strong(a ##1 b ##0 c)", sig),
        Verdict::Holds
    );
    // Once the antecedent has matched the two agree.
    let sig = &[("a", "10"), ("b", "01"), ("c", "01")];
    for text in ["a ##1 b #-# strong(c)", "strong(a ##1 b ##0 c)"] {
        assert_eq!(assert_verdict(decls, text, sig), Verdict::HoldsStrongly);
    }
}

/// 16.12.22 (b)/(c): the antecedent of `|->` (and `#-#`) shall be nondegenerate (an
/// empty match is fine), that of `|=>` (and `#=#`) shall admit a match (empty-only
/// is fine); the consequent is a property, so a sequence there is held to (a).
#[test]
fn t21_nondegeneracy_of_antecedents() {
    let never = "(1'b1) intersect (1'b1 ##1 1'b1)";
    let empty_only = "1'b1[*0]";
    let both = "a[*0:2]";
    for op in ["|->", "#-#"] {
        for bad in [never, empty_only] {
            let msg = rejected_lenient("", &format!("{bad} {op} b"));
            assert!(msg.contains("16.12.22 (b)"), "{bad} {op}: {msg}");
            assert!(msg.contains("overlapped implication"), "{bad} {op}: {msg}");
        }
        builds("", &format!("{both} {op} b"));
        builds("", &format!("a {op} b"));
    }
    for op in ["|=>", "#=#"] {
        let msg = rejected_lenient("", &format!("{never} {op} b"));
        assert!(msg.contains("16.12.22 (c)"), "{op}: {msg}");
        assert!(msg.contains("at least one match"), "{op}: {msg}");
        builds("", &format!("{empty_only} {op} b"));
        builds("", &format!("{both} {op} b"));
        builds("", &format!("a {op} b"));
    }
    for op in ["|->", "|=>", "#-#", "#=#"] {
        let msg = rejected_lenient("", &format!("a {op} a[*0:1]"));
        assert!(msg.contains("16.12.22 (a)"), "{op}: {msg}");
    }
}

/// 16.12.19 / F.5.4: the antecedent's local variables flow into the consequent of
/// `|->`, `|=>`, `#-#` and `#=#`.
#[test]
fn t21_antecedent_local_variables_flow_into_the_consequent() {
    // `v` is `n` on the tick `a` holds; the consequent wants `n == v + 1` one tick on.
    for body in [
        "(a, v = n) |-> ##1 (n == v + 1)",
        "(a, v = n) |=> (n == v + 1)",
        "(a, v = n) #-# ##1 (n == v + 1)",
        "(a, v = n) #=# (n == v + 1)",
    ] {
        let decls = format!("property p; int v; {body}; endproperty");
        assert_eq!(
            assert_verdict(&decls, "p", &[("a", "10"), ("n", "45")]),
            Verdict::HoldsStrongly,
            "{body}"
        );
        assert_eq!(
            assert_verdict(&decls, "p", &[("a", "10"), ("n", "44")]),
            Verdict::Fails,
            "{body}"
        );
    }
    // Through a nested implication and into an `if` condition of the consequent.
    let decls = "property p; int v; (a, v = n) |-> (b |-> ##1 (n == v + 1)); endproperty";
    let t = |a, b, n| assert_verdict(decls, "p", &[("a", a), ("b", b), ("n", n)]);
    assert_eq!(t("10", "10", "45"), Verdict::HoldsStrongly);
    assert_eq!(t("10", "10", "44"), Verdict::Fails);
    let decls = "property p; int v; (a, v = n) |-> (if (n == v) (b ##1 c)); endproperty";
    let t = |b, c| assert_verdict(decls, "p", &[("a", "10"), ("n", "00"), ("b", b), ("c", c)]);
    assert_eq!(t("10", "01"), Verdict::HoldsStrongly);
    assert_eq!(t("10", "00"), Verdict::Fails);
}

/// F.5.4: a variable assigned by one operand of an operator other than the four
/// above is not visible to the other operand; reading it is a loud error.
#[test]
fn t21_variables_do_not_flow_across_other_operators() {
    for body in [
        "((a, v = n) |-> b) and (c |-> (n == v))",
        "((a, v = n) |-> b) or (c |-> (n == v))",
        "if (c) ((a, v = n) |-> b) else (d |-> (n == v))",
        "not ((a, v = n) |-> b) and (c |-> (n == v))",
    ] {
        let msg = rejected_lenient(&format!("property p; int v; {body}; endproperty"), "p");
        assert!(msg.contains("does not flow"), "{body}: {msg}");
    }
}

// -- T22: implies / iff (16.12.8) -----------------------------------------------

/// 16.12.8: `p1 implies p2` is true iff `p1` is false or `p2` is true.
#[test]
fn t22_implies_truth_table() {
    for (a, b, want) in [
        ("0", "0", Verdict::HoldsStrongly),
        ("0", "1", Verdict::HoldsStrongly),
        ("1", "1", Verdict::HoldsStrongly),
        ("1", "0", Verdict::Fails),
    ] {
        assert_eq!(
            assert_verdict("", "a implies b", &[("a", a), ("b", b)]),
            want,
            "a implies b at a={a} b={b}"
        );
    }
    // Over properties, with delays: `p1` is evaluated from the start tick, not from
    // the end of anything.
    let prop = "(a ##1 b) implies (c ##1 d)";
    let sig = |c: &'static str, d: &'static str| {
        assert_verdict("", prop, &[("a", "10"), ("b", "01"), ("c", c), ("d", d)])
    };
    assert_eq!(sig("10", "01"), Verdict::HoldsStrongly);
    assert_eq!(sig("10", "00"), Verdict::Fails);
    // `p1` false: true whatever `p2` does.
    assert_eq!(
        assert_verdict(
            "",
            prop,
            &[("a", "00"), ("b", "01"), ("c", "00"), ("d", "00")]
        ),
        Verdict::HoldsStrongly
    );
}

/// 16.12.8 / F.3.4.3.2: `p1 implies p2` is `not p1 or p2`, strengths and pending
/// verdicts included.
#[test]
fn t22_implies_is_not_or() {
    let names = ["a", "b", "c", "d"];
    equivalent("", "a implies b", "(not a) or b", &names, 3);
    equivalent(
        "",
        "(a ##1 b) implies (c ##1 d)",
        "(not (a ##1 b)) or (c ##1 d)",
        &names,
        3,
    );
    equivalent(
        "",
        "(a ##[1:$] b) implies strong(c ##1 d)",
        "(not (a ##[1:$] b)) or strong(c ##1 d)",
        &names,
        3,
    );
    equivalent(
        "",
        "(if (a) b) implies (a |-> c)",
        "(not (if (a) b)) or (a |-> c)",
        &names,
        3,
    );
}

/// 16.12.8: `p1 iff p2` is true iff both are false or both are true.
#[test]
fn t22_iff_truth_table() {
    for (a, b, want) in [
        ("0", "0", Verdict::HoldsStrongly),
        ("0", "1", Verdict::Fails),
        ("1", "0", Verdict::Fails),
        ("1", "1", Verdict::HoldsStrongly),
    ] {
        assert_eq!(
            assert_verdict("", "a iff b", &[("a", a), ("b", b)]),
            want,
            "a iff b at a={a} b={b}"
        );
    }
    let names = ["a", "b", "c", "d"];
    // F.3.4.3.2: `p1 iff p2` is `(p1 implies p2) and (p2 implies p1)`.
    equivalent("", "a iff b", "(a implies b) and (b implies a)", &names, 3);
    equivalent(
        "",
        "(a ##1 b) iff (c |-> d)",
        "((a ##1 b) implies (c |-> d)) and ((c |-> d) implies (a ##1 b))",
        &names,
        3,
    );
    // Symmetric.
    equivalent(
        "",
        "(a ##1 b) iff (c ##1 d)",
        "(c ##1 d) iff (a ##1 b)",
        &names,
        3,
    );
    // `iff` with a pending side keeps the pending verdict of the side.
    equivalent(
        "",
        "(a ##[1:$] b) iff c",
        "((a ##[1:$] b) implies c) and (c implies (a ##[1:$] b))",
        &names,
        3,
    );
}

/// Table 16-3: `implies` and `iff` are both right associative (slang does the
/// parsing; the builder must not regroup what it is handed).
#[test]
fn t22_implies_and_iff_associativity() {
    let names = ["a", "b", "c"];
    equivalent(
        "",
        "a implies b implies c",
        "a implies (b implies c)",
        &names,
        3,
    );
    equivalent("", "a iff b iff c", "a iff (b iff c)", &names, 3);
    // `a implies b` is not `(a implies b) implies c`: the grouping matters.
    let l = all_verdicts("", "a implies b implies c", &names, 2);
    let r = all_verdicts("", "(a implies b) implies c", &names, 2);
    assert!(l.iter().zip(&r).any(|(x, y)| x != y));
}

/// F.5.4: nothing flows between the operands of `implies`/`iff`, and nothing out.
#[test]
fn t22_variables_do_not_flow_across_implies_and_iff() {
    for body in [
        "((a, v = n) |-> b) implies (c |-> (n == v))",
        "((a, v = n) |-> b) iff (c |-> (n == v))",
        "(c |-> (n == v)) implies ((a, v = n) |-> b)",
    ] {
        let msg = rejected_lenient(&format!("property p; int v; {body}; endproperty"), "p");
        assert!(msg.contains("does not flow"), "{body}: {msg}");
    }
    // Each operand may use the variables that reached the operator.
    let decls = "property p; int v; (a, v = n) |-> ((n == v) implies (b iff c)); endproperty";
    builds(decls, "p");
}

// -- T23: nexttime / always (16.12.10, 16.12.11) --------------------------------

/// The `(n, strong)` of every `nexttime`/`s_nexttime` node of the built property,
/// in build order (a verdict cannot tell the weak form from the strong one: they
/// differ in how an attempt that is still pending at the end of the trace is
/// finally judged, so the flag is pinned on the IR).
fn nexttimes(decls: &str, prop: &str) -> Vec<(u32, bool)> {
    with_property(decls, &ap(prop), false, |r, _| {
        let (ir, _) = r.unwrap_or_else(|e| panic!("`{prop}` failed to build: {e}"));
        ir.props
            .iter()
            .filter_map(|p| match p {
                Prop::Nexttime { n, strong, .. } => Some((*n, *strong)),
                _ => None,
            })
            .collect()
    })
}

/// [`nexttimes`] for `always`/`s_always`: `(lo, hi, strong)`.
fn always_nodes(decls: &str, prop: &str) -> Vec<(u32, Option<u32>, bool)> {
    with_property(decls, &ap(prop), false, |r, _| {
        let (ir, _) = r.unwrap_or_else(|e| panic!("`{prop}` failed to build: {e}"));
        ir.props
            .iter()
            .filter_map(|p| match p {
                Prop::Always { lo, hi, strong, .. } => Some((*lo, *hi, *strong)),
                _ => None,
            })
            .collect()
    })
}

/// 16.12.10 p1/p2: `nexttime a` is true if the clock ticks once more and `a`
/// holds there, or if it does not tick again; `s_nexttime a` needs the tick.
#[test]
fn t23_nexttime_and_s_nexttime() {
    for prop in ["nexttime a", "s_nexttime a"] {
        for (a, want) in [
            ("01", Verdict::HoldsStrongly),
            ("00", Verdict::Fails),
            ("10", Verdict::Fails),
            ("011", Verdict::HoldsStrongly),
            // No next tick yet: nothing has failed, nothing is proven.
            ("1", Verdict::Holds),
            ("0", Verdict::Holds),
        ] {
            assert_eq!(
                assert_verdict("", prop, &[("a", a)]),
                want,
                "{prop} on a={a}"
            );
        }
    }
    assert_eq!(nexttimes("", "nexttime a"), [(1, false)]);
    assert_eq!(nexttimes("", "s_nexttime a"), [(1, true)]);
    // The start tick is the evaluation attempt's, not tick 0.
    assert_eq!(
        verdict("", "nexttime a", &[("a", "0101")], 2, false),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        verdict("", "nexttime a", &[("a", "0110")], 2, false),
        Verdict::Fails
    );
}

/// 16.12.10 p7/p8: `nexttime [2] a` and `s_nexttime [2] a`.
#[test]
fn t23_indexed_nexttime() {
    for prop in ["nexttime [2] a", "s_nexttime [2] a"] {
        for (a, want) in [
            ("001", Verdict::HoldsStrongly),
            ("101", Verdict::HoldsStrongly),
            ("000", Verdict::Fails),
            ("110", Verdict::Fails),
            // Fewer than two more ticks so far.
            ("00", Verdict::Holds),
            ("0", Verdict::Holds),
        ] {
            assert_eq!(
                assert_verdict("", prop, &[("a", a)]),
                want,
                "{prop} on a={a}"
            );
        }
    }
    assert_eq!(nexttimes("", "nexttime [2] a"), [(2, false)]);
    assert_eq!(nexttimes("", "s_nexttime [2] a"), [(2, true)]);
    // The index is a constant expression: a parameter, an arithmetic expression.
    assert_eq!(nexttimes("", "nexttime [my_delay] a"), [(2, false)]);
    assert_eq!(nexttimes("", "s_nexttime [my_delay + 1] a"), [(3, true)]);
    // ... or a formal of the enclosing property.
    assert_eq!(
        nexttimes("property p(int k); nexttime [k] a; endproperty", "p(3)"),
        [(3, false)]
    );
}

/// 16.12.10: `nexttime a` is `nexttime [1] a`, `nexttime [0]` is the alignment
/// operator, indices add up, and the strong form is the dual of the weak one
/// (F.3.4.3): `s_nexttime p` is `not nexttime not p`.
#[test]
fn t23_nexttime_equivalences() {
    let names = ["a", "b"];
    equivalent("", "nexttime a", "nexttime [1] a", &names, 5);
    equivalent("", "s_nexttime a", "s_nexttime [1] a", &names, 5);
    equivalent("", "nexttime [0] a", "a", &names, 5);
    equivalent("", "s_nexttime [0] a", "a", &names, 5);
    equivalent("", "nexttime [2] a", "nexttime nexttime a", &names, 5);
    equivalent(
        "",
        "s_nexttime [3] a",
        "s_nexttime s_nexttime [2] a",
        &names,
        5,
    );
    equivalent("", "s_nexttime a", "not nexttime not a", &names, 5);
    equivalent("", "nexttime a", "not s_nexttime not a", &names, 5);
    // Over a sequence operand and a property operand.
    equivalent(
        "",
        "s_nexttime (a ##1 b)",
        "not nexttime not (a ##1 b)",
        &names,
        4,
    );
    equivalent(
        "",
        "nexttime [2] (a |-> ##1 b)",
        "nexttime nexttime (a |-> ##1 b)",
        &names,
        5,
    );
    // The four of them are different properties.
    let weak = all_verdicts("", "nexttime [2] a", &names, 4);
    let other = all_verdicts("", "nexttime [1] a", &names, 4);
    assert_ne!(weak, other);
}

/// 16.12.10 p3/p4: `nexttime always a` and `s_nexttime always a`: `a` at every
/// tick from the next one on, with the next tick required only by the strong form.
#[test]
fn t23_nexttime_always() {
    for prop in ["nexttime always a", "s_nexttime always a"] {
        for (a, want) in [
            // `always` never has proof on a finite trace: more ticks may come.
            ("0111", Verdict::Holds),
            ("1", Verdict::Holds),
            ("0", Verdict::Holds),
            ("0101", Verdict::Fails),
            ("1110", Verdict::Fails),
        ] {
            assert_eq!(
                assert_verdict("", prop, &[("a", a)]),
                want,
                "{prop} on a={a}"
            );
        }
    }
    assert_eq!(nexttimes("", "nexttime always a"), [(1, false)]);
    assert_eq!(nexttimes("", "s_nexttime always a"), [(1, true)]);
    assert_eq!(always_nodes("", "nexttime always a"), [(0, None, false)]);
}

/// 16.12.11: `always [lo:hi] p` holds at every tick of the range, whether or not
/// all of them exist; `always p` is `always [0:$] p`.
#[test]
fn t23_always_truth_table() {
    for prop in ["always a", "always [0:$] a"] {
        for (a, want) in [
            ("111", Verdict::Holds),
            ("1", Verdict::Holds),
            ("101", Verdict::Fails),
            ("011", Verdict::Fails),
            ("110", Verdict::Fails),
        ] {
            assert_eq!(
                assert_verdict("", prop, &[("a", a)]),
                want,
                "{prop} on a={a}"
            );
        }
    }
    // 16.12.11 p2 `always [2:5] a`, p3 `s_always [2:5] a`: `a` at the second through
    // fifth ticks after the start; the other ticks do not matter.
    for prop in ["always [2:5] a", "s_always [2:5] a"] {
        for (a, want) in [
            // Ticks 2..=5 all exist and hold.
            ("00111100", Verdict::HoldsStrongly),
            ("11111111", Verdict::HoldsStrongly),
            ("00111101", Verdict::HoldsStrongly),
            // One of the ticks 2..=5 fails.
            ("00101100", Verdict::Fails),
            ("00111000", Verdict::Fails),
            ("11011111", Verdict::Fails),
            // The range has not all been seen yet: pending.
            ("0011", Verdict::Holds),
            ("0", Verdict::Holds),
            ("00111", Verdict::Holds),
            // ... and decided as soon as the fifth tick has been seen.
            ("001111", Verdict::HoldsStrongly),
        ] {
            assert_eq!(
                assert_verdict("", prop, &[("a", a)]),
                want,
                "{prop} on a={a}"
            );
        }
    }
    assert_eq!(always_nodes("", "always [2:5] a"), [(2, Some(5), false)]);
    assert_eq!(always_nodes("", "s_always [2:5] a"), [(2, Some(5), true)]);
    assert_eq!(always_nodes("", "always a"), [(0, None, false)]);
    // 16.12.11 p4 `always [2:$] a`: every tick from the second on, none required.
    for (a, want) in [
        ("0011", Verdict::Holds),
        ("00", Verdict::Holds),
        ("0010", Verdict::Fails),
        ("1111110", Verdict::Fails),
    ] {
        assert_eq!(
            assert_verdict("", "always [2:$] a", &[("a", a)]),
            want,
            "always [2:$] a on a={a}"
        );
    }
    assert_eq!(always_nodes("", "always [2:$] a"), [(2, None, false)]);
    // The bounds are constant expressions, formals included.
    assert_eq!(
        always_nodes("", "always [my_delay:my_delay + 3] a"),
        [(2, Some(5), false)]
    );
    assert_eq!(
        always_nodes(
            "property p(int lo, int hi); s_always [lo:hi] a; endproperty",
            "p(1, 4)"
        ),
        [(1, Some(4), true)]
    );
}

/// 16.12.11: `always [lo:hi] p` is `p` at every one of its ticks, so it is the
/// conjunction of the `nexttime [k] p`; the strong forms are the duals.
#[test]
fn t23_always_equivalences() {
    let names = ["a"];
    equivalent("", "always a", "always [0:$] a", &names, 7);
    equivalent(
        "",
        "always [2:5] a",
        "nexttime [2] a and nexttime [3] a and nexttime [4] a and nexttime [5] a",
        &names,
        7,
    );
    equivalent(
        "",
        "s_always [2:5] a",
        "s_nexttime [2] a and s_nexttime [3] a and s_nexttime [4] a and s_nexttime [5] a",
        &names,
        7,
    );
    equivalent("", "always [3:3] a", "nexttime [3] a", &names, 6);
    equivalent("", "s_always [3:3] a", "s_nexttime [3] a", &names, 6);
    equivalent("", "always [2:$] a", "nexttime [2] always a", &names, 7);
    equivalent(
        "",
        "always a",
        // (`always` has the lowest precedence of all (Table 16-3).)
        "(always [0:3] a) and nexttime [4] always a",
        &names,
        7,
    );
    // A property operand, with every start tick of its own.
    let two = ["a", "b"];
    equivalent(
        "",
        "always [1:2] (a |-> ##1 b)",
        "nexttime (a |-> ##1 b) and nexttime [2] (a |-> ##1 b)",
        &two,
        5,
    );
    // A single tick is a single tick.
    let single = all_verdicts("", "always [2:2] a", &names, 5);
    assert_eq!(single, all_verdicts("", "nexttime [2] a", &names, 5));
}

/// 16.12.11: `always p` over `p` at every start tick: the explicit form of the
/// implicit always of 16.5. `p` is false at a start tick iff `always p` fails from
/// any earlier one, and a pending `p` keeps `always p` pending.
#[test]
fn t23_always_is_every_start_tick() {
    let names = ["a", "b"];
    let prop = "a |-> ##1 b";
    let always = format!("always ({prop})");
    for len in 1..=5usize {
        for table in all_traces(&names, len) {
            let sig: Vec<(&str, String)> = names
                .iter()
                .map(|n| {
                    (
                        *n,
                        table[*n]
                            .iter()
                            .map(|v| char::from_digit(*v as u32, 10).unwrap())
                            .collect(),
                    )
                })
                .collect();
            let sig: Vec<(&str, &str)> = sig.iter().map(|(n, s)| (*n, s.as_str())).collect();
            // At the tail tick `p` is vacuous on both tails (no antecedent match
            // on a `⊥` letter, `|->`), so only the real ticks decide.
            let each: Vec<Verdict> = (0..len as u32)
                .map(|t| verdict("", prop, &sig, t, false))
                .collect();
            let want = if each.contains(&Verdict::Fails) {
                Verdict::Fails
            } else if each.iter().all(|v| *v == Verdict::HoldsStrongly) {
                Verdict::HoldsStrongly
            } else {
                Verdict::Holds
            };
            assert_eq!(
                verdict("", &always, &sig, 0, false),
                want,
                "{always} on {sig:?} (per start tick: {each:?})"
            );
        }
    }
}

/// 16.12.11's examples.
#[test]
fn t23_lrm_always_examples() {
    // p1: `a ##1 b |=> always c`: after a at the start and b at the second tick, c
    // at every tick that follows the second.
    let p1 = "a ##1 b |=> always c";
    let sig = |a, b, c| assert_verdict("", p1, &[("a", a), ("b", b), ("c", c)]);
    assert_eq!(sig("1000", "0100", "0011"), Verdict::Holds);
    assert_eq!(sig("1000", "0100", "0010"), Verdict::Fails);
    assert_eq!(sig("1000", "0100", "0001"), Verdict::Fails);
    // c is not required at the antecedent's own ticks, nor without a match.
    assert_eq!(sig("1000", "0100", "1111"), Verdict::Holds);
    assert_eq!(sig("0000", "0100", "0000"), Verdict::HoldsStrongly);
    assert_eq!(sig("1000", "0000", "0000"), Verdict::HoldsStrongly);
    // a1: `reset[*5] #=# always !reset` -- reset for the first 5 ticks, then low.
    let a1 = "reset[*5] #=# always !reset";
    let sig = |r| assert_verdict("", a1, &[("reset", r)]);
    assert_eq!(sig("11111000"), Verdict::Holds);
    assert_eq!(sig("111110"), Verdict::Holds);
    assert_eq!(sig("11111010"), Verdict::Fails);
    assert_eq!(sig("11110000"), Verdict::Fails);
    assert_eq!(sig("01111100"), Verdict::Fails);
    // 16.12.9 p1/p2: `##[0:5] done #-# always !rst` and the nonoverlapped form;
    // `done` is `d`, `rst` is `reset`.
    let overlapped = "##[0:5] d #-# always !reset";
    let nonoverlapped = "##[0:5] d #=# always !reset";
    let sig = |p, d, r| assert_verdict("", p, &[("d", d), ("reset", r)]);
    // done at tick 2, rst low from tick 2 (overlapped) / tick 3 (nonoverlapped) on.
    assert_eq!(sig(overlapped, "0010000", "1100000"), Verdict::Holds);
    assert_eq!(sig(nonoverlapped, "0010000", "1100000"), Verdict::Holds);
    // rst high exactly at the done tick: the overlapped form fails, the other not.
    assert_eq!(sig(overlapped, "0010000", "0010000"), Verdict::Fails);
    assert_eq!(sig(nonoverlapped, "0010000", "0010000"), Verdict::Holds);
    // One of the done ticks is enough ("starting from one of the clock ticks").
    assert_eq!(sig(overlapped, "0010100", "0010000"), Verdict::Holds);
    assert_eq!(sig(overlapped, "0010100", "0000100"), Verdict::Fails);
    // done must come within the first 6 ticks.
    assert_eq!(sig(overlapped, "0000001", "0000000"), Verdict::Fails);
    assert_eq!(sig(nonoverlapped, "0000001", "0000000"), Verdict::Fails);
}

/// Local variables reach the operand of `nexttime`/`always` from the antecedent
/// that is in scope, and nothing comes out of the operator (F.5.4).
#[test]
fn t23_variables_and_nexttime_always() {
    // In: `v` holds the sample of `n` on the tick `a` held.
    let decls = "property p; int v; (a, v = n) |-> nexttime (n == v); endproperty";
    assert_eq!(
        assert_verdict(decls, "p", &[("a", "10"), ("n", "55")]),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        assert_verdict(decls, "p", &[("a", "10"), ("n", "56")]),
        Verdict::Fails
    );
    let decls = "property p; int v; (a, v = n) |=> always (n == v); endproperty";
    assert_eq!(
        assert_verdict(decls, "p", &[("a", "100"), ("n", "555")]),
        Verdict::Holds
    );
    assert_eq!(
        assert_verdict(decls, "p", &[("a", "100"), ("n", "565")]),
        Verdict::Fails
    );
    let decls = "property p; int v; (a, v = n) |-> nexttime [2] always (n >= v); endproperty";
    builds(decls, "p");
    // Out: not from under a `nexttime`/`always`.
    for body in [
        "(nexttime ((a, v = n) |-> b)) and (c |-> (n == v))",
        "(always ((a, v = n) |-> b)) and (c |-> (n == v))",
        "(s_always [1:2] ((a, v = n) |-> b)) and (c |-> (n == v))",
        "(s_nexttime [2] ((a, v = n) |-> b)) and (c |-> (n == v))",
    ] {
        let msg = rejected_lenient(&format!("property p; int v; {body}; endproperty"), "p");
        assert!(msg.contains("does not flow"), "{body}: {msg}");
    }
}

/// 16.12.10/16.12.11 legality: the index of `nexttime` is one constant, `always`
/// takes a range, `s_always` a bounded one, minimum at most maximum.
#[test]
fn t23_illegal_forms_are_rejected() {
    // 16.12.11 p5.
    let msg = rejected_lenient("", "s_always [2:$] a");
    assert!(
        msg.contains("16.12.11") && msg.contains("bounded"),
        "s_always [2:$]: {msg}"
    );
    let msg = rejected_lenient("", "always [3:2] a");
    assert!(
        msg.contains("minimum") && msg.contains("maximum"),
        "always [3:2]: {msg}"
    );
    let msg = rejected_lenient("", "s_always [5:1] a");
    assert!(msg.contains("minimum"), "s_always [5:1]: {msg}");
    let msg = rejected_lenient("", "nexttime [1:2] a");
    assert!(msg.contains("16.12.10"), "nexttime [1:2]: {msg}");
    let msg = rejected_lenient("", "s_nexttime [1:$] a");
    assert!(msg.contains("16.12.10"), "s_nexttime [1:$]: {msg}");
    let msg = rejected_lenient("", "always [3] a");
    assert!(
        msg.contains("16.12.11") && msg.contains("range"),
        "always [3]: {msg}"
    );
    let msg = rejected_lenient("", "s_always [3] a");
    assert!(msg.contains("16.12.11"), "s_always [3]: {msg}");
}

// -- T24: eventually / until (16.12.12, 16.12.13) ----------------------------

/// [`nexttimes`] for `eventually`/`s_eventually`: `(lo, hi, strong)`.
fn eventually_nodes(decls: &str, prop: &str) -> Vec<(u32, Option<u32>, bool)> {
    with_property(decls, &ap(prop), false, |r, _| {
        let (ir, _) = r.unwrap_or_else(|e| panic!("`{prop}` failed to build: {e}"));
        ir.props
            .iter()
            .filter_map(|p| match p {
                Prop::Eventually { lo, hi, strong, .. } => Some((*lo, *hi, *strong)),
                _ => None,
            })
            .collect()
    })
}

/// The `strong` flag of every `until` node of the built property, in build order.
fn until_flags(decls: &str, prop: &str) -> Vec<bool> {
    with_property(decls, &ap(prop), false, |r, _| {
        let (ir, _) = r.unwrap_or_else(|e| panic!("`{prop}` failed to build: {e}"));
        ir.props
            .iter()
            .filter_map(|p| match p {
                Prop::Until { strong, .. } => Some(*strong),
                _ => None,
            })
            .collect()
    })
}

/// 16.12.12 p1/p2: `a until b` holds `a` at every tick up to, but not including,
/// one where `b` holds (`a` need not hold at a tick where `b` does); the weak form
/// does not need `b` ever to come, the strong form does. A verdict cannot tell the
/// two apart (they differ in how a still pending attempt is finally judged), so
/// the flag is pinned on the IR.
#[test]
fn t24_until_and_s_until() {
    for prop in ["a until b", "a s_until b"] {
        for (a, b, want) in [
            // `b` never came yet, `a` held throughout: pending.
            ("111", "000", Verdict::Holds),
            ("1", "0", Verdict::Holds),
            // `a` drops before `b` came.
            ("110", "000", Verdict::Fails),
            ("011", "000", Verdict::Fails),
            ("0", "0", Verdict::Fails),
            ("1101", "0001", Verdict::Fails),
            // `b` holds: `a` is not needed there or later.
            ("110", "001", Verdict::HoldsStrongly),
            ("100", "010", Verdict::HoldsStrongly),
            ("000", "100", Verdict::HoldsStrongly),
            ("0", "1", Verdict::HoldsStrongly),
            ("111", "111", Verdict::HoldsStrongly),
            // Only the FIRST tick where `b` holds ends the obligation.
            ("100", "011", Verdict::HoldsStrongly),
        ] {
            assert_eq!(
                assert_verdict("", prop, &[("a", a), ("b", b)]),
                want,
                "{prop} on a={a} b={b}"
            );
        }
    }
    assert_eq!(until_flags("", "a until b"), [false]);
    assert_eq!(until_flags("", "a s_until b"), [true]);
    // The start tick is the evaluation attempt's.
    assert_eq!(
        verdict("", "a until b", &[("a", "0110"), ("b", "0000")], 1, false),
        Verdict::Fails
    );
    assert_eq!(
        verdict("", "a until b", &[("a", "0110"), ("b", "0010")], 1, false),
        Verdict::HoldsStrongly
    );
}

/// 16.12.12 p3/p4: `a until_with b` also needs `a` at the tick where `b` holds.
#[test]
fn t24_until_with_and_s_until_with() {
    for prop in ["a until_with b", "a s_until_with b"] {
        for (a, b, want) in [
            ("111", "000", Verdict::Holds),
            ("1", "0", Verdict::Holds),
            ("110", "000", Verdict::Fails),
            // `a` is needed at the tick `b` holds.
            ("110", "001", Verdict::Fails),
            ("100", "010", Verdict::Fails),
            ("0", "1", Verdict::Fails),
            ("111", "001", Verdict::HoldsStrongly),
            ("110", "010", Verdict::HoldsStrongly),
            ("1", "1", Verdict::HoldsStrongly),
            // `a` after the first `b` tick does not matter.
            ("1100", "0100", Verdict::HoldsStrongly),
        ] {
            assert_eq!(
                assert_verdict("", prop, &[("a", a), ("b", b)]),
                want,
                "{prop} on a={a} b={b}"
            );
        }
    }
    assert_eq!(until_flags("", "a until_with b"), [false]);
    assert_eq!(until_flags("", "a s_until_with b"), [true]);
}

/// F.3.4.3.8: the derived unbounded operators, and 16.12.12's note that
/// `a s_until_with b` is `strong(a[*1:$] ##0 b)`.
#[test]
fn t24_until_equivalences() {
    let ab = ["a", "b"];
    equivalent("", "always a", "a until 1'b0", &["a"], 7);
    equivalent("", "a s_until b", "(a until b) and s_eventually b", &ab, 5);
    equivalent("", "a until_with b", "a until (a and b)", &ab, 5);
    equivalent("", "a s_until_with b", "a s_until (a and b)", &ab, 5);
    equivalent("", "a s_until_with b", "strong(a[*1:$] ##0 b)", &ab, 5);
    // Over property operands, too.
    equivalent(
        "",
        "(a |-> ##1 b) until_with c",
        "(a |-> ##1 b) until ((a |-> ##1 b) and c)",
        &["a", "b", "c"],
        4,
    );
    equivalent(
        "",
        "(a ##1 b) s_until c",
        "((a ##1 b) until c) and s_eventually c",
        &["a", "b", "c"],
        4,
    );
    // `until` and `until_with` are different, and so are weak and strong ones
    // only through the end of the trace.
    let weak = all_verdicts("", "a until b", &ab, 4);
    assert_ne!(weak, all_verdicts("", "a until_with b", &ab, 4));
    // Right associative (Table 16-3): `a until b until c` is `a until (b until c)`.
    let abc = ["a", "b", "c"];
    let right = equivalent("", "a until b until c", "a until (b until c)", &abc, 4);
    assert_ne!(right, all_verdicts("", "(a until b) until c", &abc, 4));
}

/// The operands of an until are properties, each with every start tick of its
/// own.
#[test]
fn t24_until_over_properties() {
    // `(a |-> ##1 b)` at every tick before `c`.
    let prop = "(a |-> ##1 b) until c";
    let sig = |a, b, c| assert_verdict("", prop, &[("a", a), ("b", b), ("c", c)]);
    // Every attempt holds (the last ones vacuously) and `c` never comes: a weak
    // until holds on.
    assert_eq!(sig("0100", "0010", "0000"), Verdict::HoldsStrongly);
    assert_eq!(sig("0100", "0000", "0000"), Verdict::Fails);
    // The failing attempt is at a tick after `c` came: not required.
    assert_eq!(sig("0001", "0000", "0100"), Verdict::HoldsStrongly);
    // The failing attempt is AT the tick `c` holds: not required either.
    assert_eq!(sig("0100", "0000", "0100"), Verdict::HoldsStrongly);
    // A sequence operand is a weak sequence property: the attempt at the last tick
    // is cut off by the end of the trace and pending, not failed.
    let seq = |a, b, c| assert_verdict("", "(a ##1 b) until c", &[("a", a), ("b", b), ("c", c)]);
    assert_eq!(seq("11", "01", "00"), Verdict::Holds);
    assert_eq!(seq("10", "01", "00"), Verdict::Fails);
}

/// 16.12.13 p1: `s_eventually a` needs a tick (the current one included) where
/// `a` holds, and so can never fail on a trace that may still be extended.
#[test]
fn t24_s_eventually() {
    for (a, want) in [
        ("000", Verdict::Holds),
        ("0", Verdict::Holds),
        ("010", Verdict::HoldsStrongly),
        ("1", Verdict::HoldsStrongly),
        ("0001", Verdict::HoldsStrongly),
    ] {
        assert_eq!(
            assert_verdict("", "s_eventually a", &[("a", a)]),
            want,
            "s_eventually a on a={a}"
        );
    }
    // From a later start tick only the ticks from it on count.
    assert_eq!(
        verdict("", "s_eventually a", &[("a", "1001")], 1, false),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        verdict("", "s_eventually a", &[("a", "1000")], 1, false),
        Verdict::Holds
    );
    assert_eq!(eventually_nodes("", "s_eventually a"), [(0, None, true)]);
    // p2: `s_eventually always a` -- from some tick on, `a` forever: no finite
    // trace proves or refutes it.
    for a in ["0111", "1111", "0110", "0"] {
        assert_eq!(
            assert_verdict("", "s_eventually always a", &[("a", a)]),
            Verdict::Holds,
            "s_eventually always a on a={a}"
        );
    }
    // p3: `always s_eventually a` neither: `a` may yet come.
    for a in ["0100", "1110", "0111"] {
        assert_eq!(
            assert_verdict("", "always s_eventually a", &[("a", a)]),
            Verdict::Holds,
            "always s_eventually a on a={a}"
        );
    }
}

/// 16.12.13 p4/p5/p7: the ranged forms. `eventually [2:5] a` needs `a` at one
/// of the second through fifth ticks unless they do not all exist;
/// `s_eventually [2:5] a` needs the tick; the strong range may be unbounded.
#[test]
fn t24_ranged_eventually() {
    for prop in ["eventually [2:5] a", "s_eventually [2:5] a"] {
        for (a, want) in [
            // `a` inside the range.
            ("0010000", Verdict::HoldsStrongly),
            ("0001000", Verdict::HoldsStrongly),
            ("0000010", Verdict::HoldsStrongly),
            ("001", Verdict::HoldsStrongly),
            // The whole range exists and `a` is never true in it.
            ("1100001", Verdict::Fails),
            ("1100000", Verdict::Fails),
            ("0100001", Verdict::Fails),
            // The range has not all been seen yet: pending.
            ("11000", Verdict::Holds),
            ("1100", Verdict::Holds),
            ("0", Verdict::Holds),
            ("10", Verdict::Holds),
        ] {
            assert_eq!(
                assert_verdict("", prop, &[("a", a)]),
                want,
                "{prop} on a={a}"
            );
        }
    }
    assert_eq!(
        eventually_nodes("", "eventually [2:5] a"),
        [(2, Some(5), false)]
    );
    assert_eq!(
        eventually_nodes("", "s_eventually [2:5] a"),
        [(2, Some(5), true)]
    );
    // p7: `s_eventually [2:$] a` -- from the second tick on, unbounded.
    for (a, want) in [
        ("0010", Verdict::HoldsStrongly),
        ("0000001", Verdict::HoldsStrongly),
        ("1100000", Verdict::Holds),
        ("11", Verdict::Holds),
    ] {
        assert_eq!(
            assert_verdict("", "s_eventually [2:$] a", &[("a", a)]),
            want,
            "s_eventually [2:$] a on a={a}"
        );
    }
    assert_eq!(
        eventually_nodes("", "s_eventually [2:$] a"),
        [(2, None, true)]
    );
    // The bounds are constant expressions, formals included.
    assert_eq!(
        eventually_nodes("", "eventually [my_delay:my_delay + 3] a"),
        [(2, Some(5), false)]
    );
    assert_eq!(
        eventually_nodes(
            "property p(int lo, int hi); s_eventually [lo:hi] a; endproperty",
            "p(1, 4)"
        ),
        [(1, Some(4), true)]
    );
}

/// 16.12.13 and F.3.4.3.8/9: the equivalences the clause states.
#[test]
fn t24_eventually_equivalences() {
    let a = ["a"];
    // p1: `strong(##[0:$] a)`.
    equivalent("", "s_eventually a", "strong(##[0:$] a)", &a, 7);
    equivalent("", "s_eventually a", "s_eventually [0:$] a", &a, 7);
    equivalent("", "s_eventually a", "not always not a", &a, 7);
    // p4, p5.
    equivalent("", "eventually [2:5] a", "weak(##[2:5] a)", &a, 8);
    equivalent("", "s_eventually [2:5] a", "strong(##[2:5] a)", &a, 8);
    // F.3.4.3.9.
    equivalent("", "eventually [3:3] a", "nexttime [3] a", &a, 7);
    equivalent("", "s_eventually [3:3] a", "s_nexttime [3] a", &a, 7);
    equivalent(
        "",
        "eventually [2:5] a",
        // (`eventually` has the lowest precedence of all (Table 16-3).)
        "(eventually [2:4] a) or nexttime [5] a",
        &a,
        8,
    );
    equivalent("", "s_eventually [2:5] a", "not always [2:5] not a", &a, 8);
    equivalent("", "s_always [2:5] a", "not eventually [2:5] not a", &a, 8);
    equivalent(
        "",
        "s_eventually [2:$] a",
        "s_nexttime [2] s_eventually a",
        &a,
        7,
    );
    // A property operand, with every start tick of its own.
    let two = ["a", "b"];
    equivalent(
        "",
        "s_eventually [1:3] (a |-> ##1 b)",
        "not always [1:3] not (a |-> ##1 b)",
        &two,
        5,
    );
    // `nexttime s_eventually a` (16.12.10 p5) and `s_nexttime s_eventually a` (p6):
    // the first one in the strict future, the second needing that future tick.
    for prop in ["nexttime s_eventually a", "s_nexttime s_eventually a"] {
        for (a, want) in [
            ("1000", Verdict::Holds),
            ("1010", Verdict::HoldsStrongly),
            ("0001", Verdict::HoldsStrongly),
            ("1", Verdict::Holds),
        ] {
            assert_eq!(
                assert_verdict("", prop, &[("a", a)]),
                want,
                "{prop} on a={a}"
            );
        }
    }
    equivalent("", "nexttime s_eventually a", "s_eventually [1:$] a", &a, 6);
    // A weak eventually is not its strong form: they differ in how an attempt
    // pending at the end of the trace is finally judged, which a verdict cannot
    // show, so the flag is pinned on the IR.
    assert_eq!(
        eventually_nodes("", "eventually [1:3] a"),
        [(1, Some(3), false)]
    );
    assert_eq!(
        eventually_nodes("", "s_eventually [1:3] a"),
        [(1, Some(3), true)]
    );
}

/// No local variable flows into or out of the operands of `until` and
/// `eventually` except the entry ones (F.5.4): an antecedent's variable is read
/// by the operands, a variable assigned inside an operand does not come out.
#[test]
fn t24_variables_and_until_eventually() {
    // In: `v` holds the sample of `n` on the tick `a` held.
    let decls = "property p; int v; (a, v = n) |-> (n == v) until b; endproperty";
    let sig = |a, n, b| assert_verdict(decls, "p", &[("a", a), ("n", n), ("b", b)]);
    assert_eq!(sig("10000", "55555", "00001"), Verdict::HoldsStrongly);
    assert_eq!(sig("10000", "55655", "00001"), Verdict::Fails);
    assert_eq!(sig("10000", "55555", "00000"), Verdict::Holds);
    let decls = "property p; int v; (a, v = n) |=> s_eventually (n == v + 1); endproperty";
    let sig = |a, n| assert_verdict(decls, "p", &[("a", a), ("n", n)]);
    assert_eq!(sig("1000", "5557"), Verdict::Holds);
    assert_eq!(sig("1000", "5566"), Verdict::HoldsStrongly);
    let decls = "property p; int v; (a, v = n) |-> eventually [1:3] (n == v); endproperty";
    assert_eq!(
        assert_verdict(decls, "p", &[("a", "10000"), ("n", "56665")]),
        Verdict::Fails
    );
    assert_eq!(
        assert_verdict(decls, "p", &[("a", "10000"), ("n", "56655")]),
        Verdict::HoldsStrongly
    );
    // Out: from neither operand of an `until`, nor from under an `eventually`.
    for body in [
        "(((a, v = n) |-> b) until c) and (d |-> (n == v))",
        "(c until ((a, v = n) |-> b)) and (d |-> (n == v))",
        "(((a, v = n) |-> b) s_until_with c) and (d |-> (n == v))",
        "(s_eventually ((a, v = n) |-> b)) and (d |-> (n == v))",
        "(eventually [1:2] ((a, v = n) |-> b)) and (d |-> (n == v))",
    ] {
        let msg = rejected_lenient(&format!("property p; int v; {body}; endproperty"), "p");
        assert!(msg.contains("does not flow"), "{body}: {msg}");
    }
}

/// 16.12.13 legality: a weak eventually has a bounded range and no bare form, a
/// range is a range, minimum at most maximum.
#[test]
fn t24_illegal_forms_are_rejected() {
    // p6.
    let msg = rejected_lenient("", "eventually [2:$] a");
    assert!(
        msg.contains("16.12.13") && msg.contains("bounded"),
        "eventually [2:$]: {msg}"
    );
    let msg = rejected_lenient("", "eventually a");
    assert!(
        msg.contains("16.12.13") && msg.contains("range"),
        "eventually a: {msg}"
    );
    let msg = rejected_lenient("", "eventually [3] a");
    assert!(
        msg.contains("16.12.13") && msg.contains("range"),
        "eventually [3]: {msg}"
    );
    let msg = rejected_lenient("", "s_eventually [3] a");
    assert!(msg.contains("16.12.13"), "s_eventually [3]: {msg}");
    let msg = rejected_lenient("", "eventually [5:2] a");
    assert!(
        msg.contains("minimum") && msg.contains("maximum"),
        "eventually [5:2]: {msg}"
    );
    let msg = rejected_lenient("", "s_eventually [4:1] a");
    assert!(msg.contains("minimum"), "s_eventually [4:1]: {msg}");
}

// -- T25: abort properties (16.12.14) ----------------------------------------

/// The mode and the abort condition's source text of every abort node of the
/// built property, in build order.
fn aborts(decls: &str, prop: &str) -> Vec<(AbortMode, String)> {
    with_property(decls, &ap(prop), false, |r, tree| {
        let (ir, leaves) = r.unwrap_or_else(|e| panic!("`{prop}` failed to build: {e}"));
        let texts = leaf_texts(&leaves, tree);
        ir.props
            .iter()
            .filter_map(|p| match p {
                Prop::Abort { cond, mode, .. } => Some((*mode, texts[cond.0 as usize].clone())),
                _ => None,
            })
            .collect()
    })
}

/// [`verdict`] with the abort conditions' samples strictly BETWEEN ticks (sample
/// `t` of a `between` row lies between tick `t` and tick `t + 1`), the part of the
/// trace only an asynchronous abort sees.
fn verdict_between(
    prop: &str,
    signals: &[(&str, &str)],
    between: &[(&str, &str)],
    start: u32,
) -> Verdict {
    let table = rows(signals);
    let len = table.values().next().expect("a signal").len() as u32;
    with_property("", &ap(prop), false, |r, _| {
        let (ir, leaves) = r.unwrap_or_else(|e| panic!("`{prop}` failed to build: {e}"));
        let mut env = Sigs::new(&leaves, &table);
        env.between = rows(between);
        Evaluator::new(&ir, &env, false)
            .verdict(len, start)
            .unwrap_or_else(|e| panic!("`{prop}` failed to evaluate: {e}"))
    })
}

/// 16.12.14 p1: the four keywords make the four modes, and the abort condition is
/// the leaf in parentheses (a whole expression, not just a name).
#[test]
fn t25_each_keyword_has_its_own_mode() {
    assert_eq!(
        aborts("", "accept_on(a) b"),
        [(AbortMode::Accept, "a".to_string())]
    );
    assert_eq!(
        aborts("", "reject_on(a) b"),
        [(AbortMode::Reject, "a".to_string())]
    );
    assert_eq!(
        aborts("", "sync_accept_on(a) b"),
        [(AbortMode::SyncAccept, "a".to_string())]
    );
    assert_eq!(
        aborts("", "sync_reject_on(a) b"),
        [(AbortMode::SyncReject, "a".to_string())]
    );
    assert_eq!(
        aborts("", "sync_reject_on(a && !b || c) d"),
        [(AbortMode::SyncReject, "a&&!b||c".to_string())]
    );
    // Any nesting is allowed (p14), lexically outermost first in the build order
    // of an operator before its operand.
    assert_eq!(
        aborts(
            "",
            "accept_on(a) sync_reject_on(b) reject_on(c) sync_accept_on(d) e"
        ),
        [
            (AbortMode::SyncAccept, "d".to_string()),
            (AbortMode::Reject, "c".to_string()),
            (AbortMode::SyncReject, "b".to_string()),
            (AbortMode::Accept, "a".to_string()),
        ]
    );
}

/// 16.12.14 p2: if the abort condition becomes true during the evaluation of the
/// underlying property, the overall evaluation is true; otherwise it is the
/// underlying property's. `strong(c ##1 d)` is still being evaluated through tick 1.
#[test]
fn t25_accept_on_makes_the_evaluation_true() {
    for prop in [
        "accept_on(a) strong(c ##1 d)",
        "sync_accept_on(a) strong(c ##1 d)",
    ] {
        for (a, c, d, want) in [
            // Never aborted: the property's own verdict.
            ("000", "100", "010", Verdict::HoldsStrongly),
            ("000", "100", "000", Verdict::Fails),
            // The abort at tick 1 comes while `d` is awaited: true although `d` is low.
            ("010", "100", "000", Verdict::HoldsStrongly),
            // The abort at tick 0: the evaluation is cut before it starts.
            ("100", "000", "000", Verdict::HoldsStrongly),
            // `d` fails at tick 1; an abort at tick 2 is after the evaluation ended.
            ("001", "100", "000", Verdict::Fails),
            // The attempt is cut off by the end of the trace: pending, and an abort
            // on its last tick makes it true.
            ("0", "1", "0", Verdict::Holds),
            ("1", "1", "0", Verdict::HoldsStrongly),
        ] {
            assert_eq!(
                assert_verdict("", prop, &[("a", a), ("c", c), ("d", d)]),
                want,
                "{prop} on a={a} c={c} d={d}"
            );
        }
    }
    // The condition is read from the attempt's start tick on, not before it.
    assert_eq!(
        verdict(
            "",
            "sync_accept_on(a) strong(c ##1 d)",
            &[("a", "1000"), ("c", "0100"), ("d", "0000")],
            1,
            false
        ),
        Verdict::Fails
    );
    // A constant true condition aborts at once.
    assert_eq!(
        assert_verdict("", "accept_on(1'b1) a", &[("a", "000")]),
        Verdict::HoldsStrongly
    );
}

/// 16.12.14 p3: a true abort condition makes the evaluation of `reject_on` false.
#[test]
fn t25_reject_on_makes_the_evaluation_false() {
    for prop in [
        "reject_on(a) strong(c ##1 d)",
        "sync_reject_on(a) strong(c ##1 d)",
    ] {
        for (a, c, d, want) in [
            ("000", "100", "010", Verdict::HoldsStrongly),
            ("000", "100", "000", Verdict::Fails),
            // The abort at tick 1, while `d` is awaited (and even though it comes).
            ("010", "100", "010", Verdict::Fails),
            ("010", "100", "000", Verdict::Fails),
            ("100", "100", "010", Verdict::Fails),
            // The abort at tick 2 is after the property was decided true.
            ("001", "100", "010", Verdict::HoldsStrongly),
        ] {
            assert_eq!(
                assert_verdict("", prop, &[("a", a), ("c", c), ("d", d)]),
                want,
                "{prop} on a={a} c={c} d={d}"
            );
        }
    }
    assert_eq!(
        assert_verdict("", "reject_on(1'b1) a", &[("a", "111")]),
        Verdict::Fails
    );
    // From a later start tick the earlier abort ticks do not count.
    assert_eq!(
        verdict(
            "",
            "sync_reject_on(b) a",
            &[("a", "11"), ("b", "10")],
            1,
            false
        ),
        Verdict::HoldsStrongly
    );
}

/// 16.12.14 p11: the abort condition takes precedence when it comes at the time
/// step where the evaluation of the underlying property ends.
#[test]
fn t25_abort_takes_precedence_at_the_end_of_the_evaluation() {
    // `a` is decided at tick 0, where `b` is true too.
    for (a, b, accept, reject) in [
        // true property, abort at the same tick: accept true, reject false.
        ("1", "1", Verdict::HoldsStrongly, Verdict::Fails),
        // false property, abort at the same tick: accept true, reject false.
        ("0", "1", Verdict::HoldsStrongly, Verdict::Fails),
        ("1", "0", Verdict::HoldsStrongly, Verdict::HoldsStrongly),
        ("0", "0", Verdict::Fails, Verdict::Fails),
    ] {
        for (kw, want) in [
            ("accept_on", accept),
            ("sync_accept_on", accept),
            ("reject_on", reject),
            ("sync_reject_on", reject),
        ] {
            assert_eq!(
                assert_verdict("", &format!("{kw}(b) a"), &[("a", a), ("b", b)]),
                want,
                "{kw}(b) a on a={a} b={b}"
            );
        }
    }
    // Once the evaluation is over, a later abort is not "during" it.
    assert_eq!(
        assert_verdict("", "sync_accept_on(b) a", &[("a", "00"), ("b", "01")]),
        Verdict::Fails
    );
    assert_eq!(
        assert_verdict("", "sync_reject_on(b) a", &[("a", "10"), ("b", "01")]),
        Verdict::HoldsStrongly
    );
}

/// 16.12.14 p5, p9: `reject_on(b) P` is `not (accept_on(b) not (P))` and
/// `sync_reject_on` is `not (sync_accept_on(b) not (P))`, over every trace.
#[test]
fn t25_reject_on_is_not_accept_on_not() {
    let names = ["a", "b", "c"];
    // Over a sequence, a Boolean and a property operand.
    for p in ["strong(b ##1 c)", "b", "(b |-> ##1 c)", "(b until c)"] {
        for (rej, acc) in [
            ("reject_on", "accept_on"),
            ("sync_reject_on", "sync_accept_on"),
        ] {
            equivalent(
                "",
                &format!("{rej}(a) {p}"),
                &format!("not ({acc}(a) (not {p}))"),
                &names,
                4,
            );
        }
    }
    // The four are four different operators: not all verdicts agree.
    let rej = all_verdicts("", "sync_reject_on(a) strong(b ##1 c)", &names, 4);
    let acc = all_verdicts("", "sync_accept_on(a) strong(b ##1 c)", &names, 4);
    let plain = all_verdicts("", "strong(b ##1 c)", &names, 4);
    assert_ne!(rej, acc);
    assert_ne!(rej, plain);
    assert_ne!(acc, plain);
    // With no tick between the clock ticks to look at, the asynchronous operators are
    // the synchronous ones.
    equivalent(
        "",
        "accept_on(a) strong(b ##1 c)",
        "sync_accept_on(a) strong(b ##1 c)",
        &names,
        4,
    );
    equivalent(
        "",
        "reject_on(a) strong(b ##1 c)",
        "sync_reject_on(a) strong(b ##1 c)",
        &names,
        4,
    );
}

/// 16.12.14 p4, p6: `accept_on`/`reject_on` look at every time step, so a pulse of
/// the condition between two ticks aborts; `sync_accept_on`/`sync_reject_on` look at
/// the ticks only and never see it.
#[test]
fn t25_asynchronous_aborts_see_the_time_steps_between_ticks() {
    // `c ##1 d` with `d` never true: fails at tick 1 unless the pulse between
    // tick 0 and tick 1 aborts it first.
    let sigs = [("c", "10"), ("d", "00"), ("a", "00")];
    let pulse = [("a", "10")];
    let quiet = [("a", "00")];
    for (prop, with_pulse, without) in [
        (
            "accept_on(a) strong(c ##1 d)",
            Verdict::HoldsStrongly,
            Verdict::Fails,
        ),
        // The sync version never samples the pulse.
        (
            "sync_accept_on(a) strong(c ##1 d)",
            Verdict::Fails,
            Verdict::Fails,
        ),
    ] {
        assert_eq!(
            verdict_between(prop, &sigs, &pulse, 0),
            with_pulse,
            "{prop}"
        );
        assert_eq!(verdict_between(prop, &sigs, &quiet, 0), without, "{prop}");
    }
    // A true property is rejected by the same pulse, asynchronously only.
    let sigs = [("c", "10"), ("d", "01"), ("a", "00")];
    assert_eq!(
        verdict_between("reject_on(a) strong(c ##1 d)", &sigs, &pulse, 0),
        Verdict::Fails
    );
    assert_eq!(
        verdict_between("sync_reject_on(a) strong(c ##1 d)", &sigs, &pulse, 0),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        verdict_between("reject_on(a) strong(c ##1 d)", &sigs, &quiet, 0),
        Verdict::HoldsStrongly
    );
    // A pulse after the evaluation ended (between ticks 1 and 2 here) does not count.
    let sigs = [("c", "100"), ("d", "010"), ("a", "000")];
    assert_eq!(
        verdict_between("reject_on(a) strong(c ##1 d)", &sigs, &[("a", "010")], 0),
        Verdict::HoldsStrongly
    );
    // A pulse before the attempt's start tick does not count either.
    let sigs = [("c", "010"), ("d", "000"), ("a", "000")];
    assert_eq!(
        verdict_between("accept_on(a) strong(c ##1 d)", &sigs, &[("a", "100")], 1),
        Verdict::Fails
    );
}

/// 16.12.14 p15..p17: the LRM's example, three formulations. The asynchronous
/// `reject_on` and the synchronous one agree when the condition has no pulse
/// between ticks, and the synchronous one is `!stop throughout put[->2]`.
#[test]
fn t25_the_stop_example_three_ways() {
    // The fixture module's signals stand in for the example's: go = x, get = y,
    // stop = z, put = e.
    let async_ = "x ##1 y[*2] |-> reject_on(z) e[->2]";
    let sync = "x ##1 y[*2] |-> sync_reject_on(z) e[->2]";
    let throughout = "x ##1 y[*2] |-> !z throughout e[->2]";
    // The three formulations over every trace: the synchronous abort is the
    // `throughout`, and with no pulse between ticks the asynchronous form is the
    // synchronous one. (The full example's 4-signal traces are too many to
    // enumerate, so the exhaustive comparison drops the `go ##1 get[*2]` prefix; the
    // example itself is checked on directed traces below.)
    equivalent(
        "",
        "sync_reject_on(z) e[->2]",
        "!z throughout e[->2]",
        &["z", "e"],
        4,
    );
    equivalent(
        "",
        "reject_on(z) e[->2]",
        "sync_reject_on(z) e[->2]",
        &["z", "e"],
        4,
    );
    // What each of them says, on a trace (go, get, get, then `put` twice).
    let sig = |stop| {
        assert_verdict(
            "",
            sync,
            &[
                ("x", "1000000"),
                ("y", "0110000"),
                ("z", stop),
                ("e", "0001010"),
            ],
        )
    };
    assert_eq!(sig("0000000"), Verdict::HoldsStrongly);
    // `stop` while the puts are awaited (tick 4).
    assert_eq!(sig("0000100"), Verdict::Fails);
    // `stop` at the tick the second `put` comes (tick 5): the abort wins.
    assert_eq!(sig("0000010"), Verdict::Fails);
    // `stop` after it (tick 6) is none of the property's business.
    assert_eq!(sig("0000001"), Verdict::HoldsStrongly);
    // With a pulse of `stop` between ticks only the asynchronous form fails.
    let sigs = [
        ("x", "1000000"),
        ("y", "0110000"),
        ("z", "0000000"),
        ("e", "0001010"),
    ];
    let pulse = [("z", "0000100")];
    assert_eq!(verdict_between(async_, &sigs, &pulse, 0), Verdict::Fails);
    assert_eq!(
        verdict_between(sync, &sigs, &pulse, 0),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        verdict_between(throughout, &sigs, &pulse, 0),
        Verdict::HoldsStrongly
    );
}

/// 16.9.2 on the property side, over weak and strong tails: goto repetition is its
/// own definition (`!b[*0:$] ##1 b` per count) and the nonconsecutive form is the
/// goto form plus the trailing `!b` ticks. The `stop` example needs this exactly:
/// a hit that is not yet awaited must not count.
#[test]
fn t25_goto_and_nonconsecutive_repetition_over_every_tail() {
    for (lhs, rhs) in [
        (
            "strong(b[->2])",
            "strong(!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b)",
        ),
        ("b[->2]", "!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b"),
        (
            "strong(b[=2])",
            "strong(!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b ##1 !b[*0:$])",
        ),
        ("b[=2]", "!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b ##1 !b[*0:$]"),
        ("c ##1 b[->2] ##1 d", "c ##1 (!b[*0:$] ##1 b)[*2] ##1 d"),
    ] {
        let names: &[&str] = if lhs.starts_with("c ") {
            &["b", "c", "d"]
        } else {
            &["b"]
        };
        equivalent("", lhs, rhs, names, if names.len() == 1 { 6 } else { 4 });
    }
    // Directed readings. One hit is not two: with the second hit the goto is
    // matched, with only one it is pending (`Holds` is the weak-tail-only pass).
    let sig = |p: &str, b, strong| verdict("", p, &[("b", b)], 0, strong);
    assert_eq!(sig("strong(b[->2])", "0101", false), Verdict::HoldsStrongly);
    assert_eq!(sig("strong(b[->2])", "0100", false), Verdict::Holds);
    // The goto match ends at the second hit, so `##1 b` then looks at the tick right
    // after it; the nonconsecutive match may extend over the trailing `!b` ticks.
    assert_eq!(sig("b[->2] ##1 b", "01101", false), Verdict::Fails);
    assert_eq!(sig("b[=2] ##1 b", "01101", false), Verdict::HoldsStrongly);
}

/// 16.9.2 over 4-state traces: `b[->n]` is `(!b[*0:$] ##1 b)[*n]`, and `!x` is
/// `x` (11.4.7), which a Boolean context makes false, so the gap `!b` is NOT true
/// on a tick where `b` is `x`. Every spelling must agree on traces holding `x`
/// samples (the gap guard once was `!(b as a Boolean)`, which is true there).
#[test]
fn goto_and_nonconsecutive_repetition_agree_with_their_definitions_on_x_samples() {
    for (lhs, rhs) in [
        ("strong(b[->1])", "strong(!b[*0:$] ##1 b)"),
        ("b[->1]", "!b[*0:$] ##1 b"),
        (
            "strong(b[->2])",
            "strong(!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b)",
        ),
        ("b[->1:2]", "(!b[*0:$] ##1 b)[*1:2]"),
        ("strong(b[=1])", "strong(!b[*0:$] ##1 b ##1 !b[*0:$])"),
        ("b[=2]", "!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b ##1 !b[*0:$]"),
    ] {
        let l = all_verdicts_over("", lhs, &["b"], 5, &[0, 1, X]);
        let r = all_verdicts_over("", rhs, &["b"], 5, &[0, 1, X]);
        assert_eq!(l.len(), r.len());
        if let Some(i) = (0..l.len()).find(|&i| l[i] != r[i]) {
            panic!(
                "`{lhs}` and `{rhs}` differ at case #{i}: {:?} vs {:?}",
                l[i], r[i]
            );
        }
        assert!(l.iter().any(|v| *v != l[0]), "`{lhs}` is vacuous");
    }
    // Directed: the `x` tick is neither a hit nor a gap, so it blocks the goto
    // match (here `Holds` is the weak tail, nothing matched or failed yet).
    let sig = |p: &str, b: &str| verdict("", p, &[("b", b)], 0, false);
    assert_eq!(sig("strong(b[->1])", "0x1"), Verdict::Fails);
    assert_eq!(sig("strong(b[->1])", "001"), Verdict::HoldsStrongly);
    assert_eq!(
        sig("strong(b[->1])", "0x1"),
        sig("strong(!b[*0:$] ##1 b)", "0x1")
    );
}

/// 16.12.14 p12..p14: abort operators among the other operators.
#[test]
fn t25_aborts_under_and_or_not() {
    // (accept_on(a) p1) and (reject_on(b) p2): `a` during p1 makes the first term
    // true (ignored), `b` during p2 makes the whole property false.
    let and = "(sync_accept_on(a) strong(c ##1 d)) and (sync_reject_on(b) strong(c ##1 e))";
    let sig = |a, b, d, e| {
        assert_verdict(
            "",
            and,
            &[("a", a), ("b", b), ("c", "100"), ("d", d), ("e", e)],
        )
    };
    assert_eq!(sig("000", "000", "010", "010"), Verdict::HoldsStrongly);
    assert_eq!(sig("000", "000", "000", "010"), Verdict::Fails);
    // `a` during p1: p1 is ignored although `d` never comes.
    assert_eq!(sig("010", "000", "000", "010"), Verdict::HoldsStrongly);
    // `a` makes the first term true but the second still has to hold.
    assert_eq!(sig("010", "000", "000", "000"), Verdict::Fails);
    // `b` during p2: false, although p2 itself holds.
    assert_eq!(sig("000", "010", "010", "010"), Verdict::Fails);
    assert_eq!(sig("010", "010", "000", "010"), Verdict::Fails);
    // (accept_on(a) p1) or (reject_on(b) p2): `a` during p1 makes the whole thing
    // true; `b` during p2 makes the second term false, ignored in the `or`.
    let or = "(sync_accept_on(a) strong(c ##1 d)) or (sync_reject_on(b) strong(c ##1 e))";
    let sig = |a, b, d, e| {
        assert_verdict(
            "",
            or,
            &[("a", a), ("b", b), ("c", "100"), ("d", d), ("e", e)],
        )
    };
    assert_eq!(sig("010", "000", "000", "000"), Verdict::HoldsStrongly);
    assert_eq!(sig("000", "000", "000", "000"), Verdict::Fails);
    // `b` rejects the second term only: p1 decides.
    assert_eq!(sig("000", "010", "010", "010"), Verdict::HoldsStrongly);
    assert_eq!(sig("000", "010", "000", "010"), Verdict::Fails);
    // not (accept_on(a) p1): `not` inverts the effect of the abort operator.
    let not = "not (sync_accept_on(a) strong(c ##1 d))";
    let sig = |a, d| assert_verdict("", not, &[("a", a), ("c", "100"), ("d", d)]);
    assert_eq!(sig("010", "000"), Verdict::Fails);
    assert_eq!(sig("010", "010"), Verdict::Fails);
    assert_eq!(sig("000", "000"), Verdict::HoldsStrongly);
    assert_eq!(sig("000", "010"), Verdict::Fails);
    // ... so it is `reject_on` of the negation, over every trace.
    equivalent(
        "",
        "not (accept_on(a) strong(b ##1 c))",
        "reject_on(a) not strong(b ##1 c)",
        &["a", "b", "c"],
        4,
    );
    // An abort operator has the lowest precedence (Table 16-3): it takes the whole of
    // the rest, `and` included.
    equivalent(
        "",
        "accept_on(a) b and c",
        "accept_on(a) (b and c)",
        &["a", "b", "c"],
        4,
    );
    let outer = all_verdicts("", "(accept_on(a) b) and c", &["a", "b", "c"], 4);
    assert_ne!(
        outer,
        all_verdicts("", "accept_on(a) b and c", &["a", "b", "c"], 4)
    );
}

/// 16.12.14 p18..p19: nested abort operators are evaluated left to right; if two
/// conditions become true in the same time step the outermost wins, if the inner
/// one comes first it applies.
#[test]
fn t25_nested_aborts_the_outermost_wins() {
    // `strong(x ##5 x)` is still being evaluated through all three ticks.
    let sig = |prop: &str, a, b| assert_verdict("", prop, &[("x", "111"), ("a", a), ("b", b)]);
    for (outer, inner) in [
        ("accept_on", "reject_on"),
        ("sync_accept_on", "sync_reject_on"),
    ] {
        let p = format!("{outer}(a) {inner}(b) strong(x ##5 x)");
        // Same tick: the outer accept wins.
        assert_eq!(sig(&p, "001", "001"), Verdict::HoldsStrongly, "{p}");
        // `b` before `a`: the inner reject has already failed it.
        assert_eq!(sig(&p, "001", "010"), Verdict::Fails, "{p}");
        // `a` before `b`: accepted before `b` matters.
        assert_eq!(sig(&p, "010", "001"), Verdict::HoldsStrongly, "{p}");
        assert_eq!(sig(&p, "000", "000"), Verdict::Holds, "{p}");
        // And the other way round: the outer reject wins a tie.
        let q = format!("{inner}(b) {outer}(a) strong(x ##5 x)");
        assert_eq!(sig(&q, "001", "001"), Verdict::Fails, "{q}");
        assert_eq!(sig(&q, "010", "001"), Verdict::HoldsStrongly, "{q}");
        assert_eq!(sig(&q, "001", "010"), Verdict::Fails, "{q}");
        assert_eq!(sig(&q, "000", "000"), Verdict::Holds, "{q}");
    }
    // Mixed strength: the synchronous one in the middle ignores a pulse.
    let sigs = [("x", "111"), ("a", "000"), ("b", "000")];
    assert_eq!(
        verdict_between(
            "accept_on(a) sync_reject_on(b) strong(x ##5 x)",
            &sigs,
            &[("a", "001")],
            0
        ),
        Verdict::HoldsStrongly
    );
}

/// 16.12.14 p20: the abort condition is a sampled value expression: sampled value
/// functions are fine, local variables and the sequence methods are not.
#[test]
fn t25_abort_conditions_are_sampled_expressions() {
    builds("", "accept_on($rose(a, @(posedge clk))) b");
    builds(
        "",
        "reject_on($sampled(a) || $past(b, 1, , @(posedge clk))) c",
    );
    let decls = "property p; int v; (a, v = n) |=> sync_accept_on(v == 1) b; endproperty";
    let msg = rejected_lenient(decls, "p");
    assert!(
        msg.contains("16.12.14") && msg.contains("local variable `v`"),
        "{msg}"
    );
    let decls = "sequence s; a ##1 b; endsequence";
    for method in ["triggered", "matched"] {
        let msg = rejected_lenient(decls, &format!("accept_on(s.{method}) c"));
        assert!(
            msg.contains("16.12.14") && msg.contains(method),
            "s.{method}: {msg}"
        );
    }
}

/// F.5.4 for the abort: the antecedent's local variables are visible in its body
/// (the body is just the consequent), and nothing assigned inside it comes out.
#[test]
fn t25_variables_and_abort() {
    // In: `v` holds `n` as sampled when `a` held.
    let decls = "property p; int v; (a, v = n) |=> sync_accept_on(b) (n == v); endproperty";
    let sig = |a, n, b| assert_verdict(decls, "p", &[("a", a), ("n", n), ("b", b)]);
    assert_eq!(sig("100", "551", "000"), Verdict::HoldsStrongly);
    assert_eq!(sig("100", "561", "000"), Verdict::Fails);
    // The abort at the tick the consequent would fail makes it true.
    assert_eq!(sig("100", "561", "010"), Verdict::HoldsStrongly);
    let decls = "property p; int v; (a, v = n) |=> sync_reject_on(b) (n == v); endproperty";
    let sig = |a, n, b| assert_verdict(decls, "p", &[("a", a), ("n", n), ("b", b)]);
    assert_eq!(sig("100", "551", "000"), Verdict::HoldsStrongly);
    assert_eq!(sig("100", "551", "010"), Verdict::Fails);
    // Out: a variable assigned in the body is not visible after it.
    for body in [
        "(sync_accept_on(b) ((a, v = n) |-> c)) and (d |-> (n == v))",
        "(reject_on(b) ((a, v = n) |-> c)) and (d |-> (n == v))",
    ] {
        let msg = rejected_lenient(&format!("property p; int v; {body}; endproperty"), "p");
        assert!(msg.contains("does not flow"), "{body}: {msg}");
    }
}

// -- T26: recursive properties (16.12.17, F.7) ----------------------------------

const PROP_ALWAYS: &str = "property prop_always(p); p and (1'b1 |=> prop_always(p)); endproperty";
const PROP_WEAK_UNTIL: &str =
    "property prop_weak_until(p, q); q or (p and (1'b1 |=> prop_weak_until(p, q))); endproperty";

/// `(declarations, call nodes)` of the built IR of `prop`.
fn recursion_shape(decls: &str, prop: &str) -> (usize, usize) {
    with_property(decls, &ap(prop), false, |r, _| {
        let (ir, _) = r.unwrap_or_else(|e| panic!("`{prop}` failed to build: {e}"));
        let calls = ir
            .props
            .iter()
            .filter(|p| matches!(p, Prop::Call { .. }))
            .count();
        assert_eq!(ir.is_recursive(), calls > 0);
        (ir.decls.len(), calls)
    })
}

/// The declarations `level(0)`, ..., `level(depth)`: the `k`-fold approximations
/// of a recursive property written out by hand (F.7: `level(0)` is the `1'b1`
/// declaration, `level(k)` instantiates `level(k - 1)` where the recursive
/// property instantiates itself). The oracle for the recursive builder, which
/// has to agree with the unfolding on every trace the unfolding is deep enough
/// for.
fn k_fold(depth: usize, level: impl Fn(usize) -> String) -> String {
    (0..=depth).map(level).collect::<Vec<_>>().join("\n")
}

/// Every explicit trace in `traces` (a list of signal rows) gives `rec` and
/// `unfolded` the same verdict, and the verdicts are not all the same.
fn agree_with_unfolding(decls: &str, rec: &str, unfolded: &str, traces: &[Vec<(&str, &str)>]) {
    let mut seen = Vec::new();
    for t in traces {
        for (start, strong) in [(0, false), (0, true), (1, false)] {
            let r = verdict(decls, rec, t, start, strong);
            let u = verdict(decls, unfolded, t, start, strong);
            assert_eq!(
                r, u,
                "`{rec}` vs `{unfolded}` on {t:?} (start {start}, strong {strong})"
            );
            if !seen.contains(&r) {
                seen.push(r);
            }
        }
    }
    assert!(
        seen.len() > 1,
        "every trace gives {seen:?}: the comparison is vacuous"
    );
}

/// 16.12.17: `prop_always(p)` "is required to hold at every cycle" -- the
/// recursive property and `always p` agree on whether they fail on every trace,
/// from every start tick, under both readings of a bare sequence (see
/// [`weakly_equivalent`] for the one way they differ).
#[test]
fn t26_prop_always_is_always() {
    weakly_equivalent(PROP_ALWAYS, "prop_always(a)", "always a", &["a"], 7);
    // The difference is exactly the strength: a trace on which `a` always holds
    // is HOLDS for `always a` (its tail owes `a` on every `⊥` letter) and HOLDS
    // STRONGLY for the recursion (the last `|=>` is vacuous).
    let a = [("a", "111")];
    assert_eq!(
        assert_verdict(PROP_ALWAYS, "prop_always(a)", &a),
        Verdict::HoldsStrongly
    );
    assert_eq!(assert_verdict(PROP_ALWAYS, "always a", &a), Verdict::Holds);
    assert_eq!(
        assert_verdict(PROP_ALWAYS, "prop_always(a)", &[("a", "101")]),
        Verdict::Fails
    );
    // The recursion is one declaration and one instance of it: the instance
    // slang unfolds past the written one is the call.
    assert_eq!(recursion_shape(PROP_ALWAYS, "prop_always(a)"), (1, 1));
    // Not just a Boolean: a property actual.
    weakly_equivalent(
        PROP_ALWAYS,
        "prop_always(b |-> c)",
        "always (b |-> c)",
        &["b", "c"],
        5,
    );
}

/// 16.12.17: `prop_weak_until(p, q)` holds `p` at every cycle up to, but not
/// including, the first cycle at which `q` holds, and `q` is never required to
/// hold -- the weak `until` of 16.12.12.
#[test]
fn t26_prop_weak_until_is_until() {
    weakly_equivalent(
        PROP_WEAK_UNTIL,
        "prop_weak_until(a, b)",
        "a until b",
        &["a", "b"],
        5,
    );
    assert_eq!(
        recursion_shape(PROP_WEAK_UNTIL, "prop_weak_until(a, b)"),
        (1, 1)
    );
}

/// 16.12.17: the properties that use them, `s |=> prop_always(p)` and `s |=>
/// prop_weak_until(p, q)`, with the sequence and property formals of the wrapper
/// passed on.
#[test]
fn t26_properties_built_on_recursive_properties() {
    let decls = format!(
        "{PROP_ALWAYS} {PROP_WEAK_UNTIL}
         property p1(s, p); s |=> prop_always(p); endproperty
         property p2(s, p, q); s |=> prop_weak_until(p, q); endproperty"
    );
    weakly_equivalent(&decls, "p1(a, b)", "a |=> always b", &["a", "b"], 5);
    weakly_equivalent(
        &decls,
        "p2(a, b, c)",
        "a |=> (b until c)",
        &["a", "b", "c"],
        4,
    );
    // The wrapper is not itself recursive but its expansion contains the call.
    assert_eq!(recursion_shape(&decls, "p1(a, b)"), (1, 1));
}

/// 16.12.17: mutually recursive properties. `check_phase1` and `check_phase2`
/// take turns; a phase whose trigger does not hold ends the obligation.
#[test]
fn t26_mutually_recursive_properties() {
    let decls = "logic s1, s2, ph1, ph2;
         property check_phase1; s1 |-> (ph1 and (1'b1 |=> check_phase2)); endproperty
         property check_phase2; s2 |-> (ph2 and (1'b1 |=> check_phase1)); endproperty";
    let run = |s1, s2, ph1, ph2| {
        assert_verdict(
            decls,
            "check_phase1",
            &[("s1", s1), ("s2", s2), ("ph1", ph1), ("ph2", ph2)],
        )
    };
    // Phase 1 at tick 0, phase 2 at tick 1, phase 1 again at tick 2, ...
    assert_eq!(run("1010", "0101", "1010", "0101"), Verdict::HoldsStrongly);
    // ... each obligation is checked: phase 1 at tick 0, phase 2 at tick 1,
    // phase 1 at tick 2 (ph1 is low there).
    assert_eq!(run("1010", "0101", "1000", "0101"), Verdict::Fails);
    assert_eq!(run("1010", "0101", "1010", "0001"), Verdict::Fails);
    // A phase whose trigger is low ends the chain: tick 1 has no s2, so tick 2's
    // low ph1 is never looked at.
    assert_eq!(run("1010", "0001", "1000", "0000"), Verdict::HoldsStrongly);
    assert_eq!(run("0000", "0000", "0000", "0000"), Verdict::HoldsStrongly);
    // One declaration is the target of the call: the other is expanded inline in
    // its body.
    assert_eq!(recursion_shape(decls, "check_phase1"), (1, 1));
}

/// 16.12.17: `accept_on` and `reject_on` may be used inside a recursive
/// property (`p3` and `p4` are mutually recursive and legal: the cycle advances
/// time once, in `p3`, although the edge `p4 -> p3` does not).
#[test]
fn t26_aborts_in_recursive_properties() {
    let decls = "property p3(p, bit b, abort); (p and (1'b1 |=> p4(p, b, abort))); endproperty
         property p4(p, bit b, abort); accept_on(b) reject_on(abort) p3(p, b, abort); endproperty";
    let run = |a, c, d| assert_verdict(decls, "p3(a, c, d)", &[("a", a), ("c", c), ("d", d)]);
    assert_eq!(run("1111", "0000", "0000"), Verdict::HoldsStrongly);
    // `a` fails at tick 2.
    assert_eq!(run("1101", "0000", "0000"), Verdict::Fails);
    // The abort that holds at tick 1 (the first tick of p4) accepts, so tick 2's
    // failure is never reached; one that comes after the failure is too late.
    assert_eq!(run("1101", "0100", "0000"), Verdict::HoldsStrongly);
    assert_eq!(run("1101", "0010", "0000"), Verdict::HoldsStrongly);
    assert_eq!(run("1101", "0001", "0000"), Verdict::Fails);
    // `abort` rejects at the first tick of p4 ...
    assert_eq!(run("1111", "0000", "0100"), Verdict::Fails);
    // ... but not before p4 starts (tick 0 is p3's).
    assert_eq!(run("1111", "0000", "1000"), Verdict::HoldsStrongly);
    // The p4 of tick 1 wraps every later one, and `reject_on(b) P` is `P on the
    // word, or b somewhere` and `P on each prefix before a b tick, completed with
    // ⊥` (F.5.6). A later abort therefore only asks for the prefix before it,
    // where `1 |=> p4` is vacuous on `⊥`: the verdict is the weak one.
    assert_eq!(run("1111", "0000", "0010"), Verdict::Holds);
    assert_eq!(run("1111", "0000", "0001"), Verdict::Holds);
    assert_eq!(recursion_shape(decls, "p3(a, c, d)"), (1, 1));
    // The recursion is the limit of its unfoldings.
    let all = format!(
        "{decls}\n{}",
        k_fold(8, |k| match k {
            0 => "property v0(p, bit b, abort); 1'b1; endproperty".to_string(),
            _ => format!(
                "property v{k}(p, bit b, abort); p and (1'b1 |=> accept_on(b) \
                 reject_on(abort) v{}(p, b, abort)); endproperty",
                k - 1
            ),
        })
    );
    let traces: Vec<Vec<(&str, &str)>> = [
        ("1111", "0000", "0000"),
        ("1101", "0000", "0000"),
        ("1101", "0100", "0000"),
        ("1101", "0010", "0000"),
        ("1101", "0001", "0000"),
        ("1111", "0000", "0100"),
        ("1111", "0000", "0001"),
        ("1111", "0000", "1000"),
        ("1011", "0001", "0010"),
    ]
    .iter()
    .map(|&(a, c, d)| vec![("a", a), ("c", c), ("d", d)])
    .collect();
    agree_with_unfolding(&all, "p3(a, c, d)", "v8(a, c, d)", &traces);
}

/// 16.12.17's `fibonacci1`: the local variable formals are rebound by each
/// recursive instance (`a`, `b`, `n` are `local input`, the actuals are
/// expressions over the caller's own copies of them) and the non-local formal
/// `fib_sig` is passed on unchanged.
#[test]
fn t26_fibonacci_with_local_variable_formals() {
    let decls = "property fibonacci1 (local input int a, b, n, int fib_sig);
           (n > 0) |-> ((fib_sig == a) and (1'b1 |=> fibonacci1(b, a + b, n - 1, fib_sig)));
         endproperty";
    let run = |count, sig| {
        assert_verdict(
            decls,
            &format!("fibonacci1(0, 1, {count}, n)"),
            &[("n", sig)],
        )
    };
    // 0, 1, 1, 2, 3, 5, 8: the first five are checked.
    assert_eq!(run(5, "01123"), Verdict::HoldsStrongly);
    assert_eq!(run(5, "0112358"), Verdict::HoldsStrongly);
    assert_eq!(run(5, "01124"), Verdict::Fails);
    assert_eq!(run(5, "11123"), Verdict::Fails);
    // `n` counts down: three ticks are checked, the fourth is free.
    assert_eq!(run(3, "0119"), Verdict::HoldsStrongly);
    assert_eq!(run(3, "0129"), Verdict::Fails);
    // One declaration, one call, three rebound slots (the call passes the three
    // local variable formals and nothing else).
    with_property(decls, &ap("fibonacci1(0, 1, 5, n)"), false, |r, _| {
        let (ir, _) = r.unwrap();
        let args: Vec<usize> = ir
            .props
            .iter()
            .filter_map(|p| match p {
                Prop::Call { args, .. } => Some(args.len()),
                _ => None,
            })
            .collect();
        assert_eq!(args, vec![3]);
        assert_eq!(ir.decls.len(), 1);
        assert_eq!(ir.decls[0].name, "fibonacci1");
    });
}

/// A declared local variable of a recursive property is initialised again by
/// every recursive instance, from the NEW values of the formals.
#[test]
fn t26_declared_local_is_reinitialised_by_each_instance() {
    let decls = "property q(local input int k);
           int w = k + 1;
           (n == w) and (1'b1 |=> q(k + 1));
         endproperty";
    let run = |sig| assert_verdict(decls, "q(0)", &[("n", sig)]);
    assert_eq!(run("1234"), Verdict::HoldsStrongly);
    assert_eq!(run("1224"), Verdict::Fails);
    assert_eq!(run("1233"), Verdict::Fails);
    // ... which is what the hand-unfolded property says.
    let all = format!(
        "{decls}\n{}",
        k_fold(8, |k| match k {
            0 => "property u0(local input int k); 1'b1; endproperty".to_string(),
            _ => format!(
                "property u{k}(local input int k); int w = k + 1; \
                 (n == w) and (1'b1 |=> u{}(k + 1)); endproperty",
                k - 1
            ),
        })
    );
    let traces: Vec<Vec<(&str, &str)>> = ["1234", "1224", "1233", "0234", "12", "1", "1234567"]
        .iter()
        .map(|n| vec![("n", *n)])
        .collect();
    agree_with_unfolding(&all, "q(0)", "u8(0)", &traces);
    // The initialisers are the instance's own, rebuilt at the call: the entry
    // writes the formal and the declared local, the call both again.
    with_property(decls, &ap("q(0)"), false, |r, _| {
        let (ir, _) = r.unwrap();
        let calls: Vec<(usize, usize)> = ir
            .props
            .iter()
            .filter_map(|p| match p {
                Prop::Call { args, inits, .. } => Some((args.len(), inits.len())),
                _ => None,
            })
            .collect();
        assert_eq!(calls, vec![(1, 1)]);
    });
    // A declared local reads the declared locals before it: those are the slots
    // of the instance being entered, not the caller's.
    let decls = "property q2(local input int k);
           int w = k + 1, v = w + w;
           (n == v) and (1'b1 |=> q2(k + 1));
         endproperty";
    let run = |sig| assert_verdict(decls, "q2(0)", &[("n", sig)]);
    // `v` is 2, 4, 6, 8, ...
    assert_eq!(run("2468"), Verdict::HoldsStrongly);
    assert_eq!(run("2478"), Verdict::Fails);
    assert_eq!(run("2268"), Verdict::Fails);
    let all = format!(
        "{decls}\n{}",
        k_fold(8, |k| match k {
            0 => "property z0(local input int k); 1'b1; endproperty".to_string(),
            _ => format!(
                "property z{k}(local input int k); int w = k + 1, v = w + w; \
                 (n == v) and (1'b1 |=> z{}(k + 1)); endproperty",
                k - 1
            ),
        })
    );
    let traces: Vec<Vec<(&str, &str)>> = ["2468", "2478", "2268", "4", "2", "24681"]
        .iter()
        .map(|n| vec![("n", *n)])
        .collect();
    agree_with_unfolding(&all, "q2(0)", "z8(0)", &traces);
}

/// The data-beat check of 16.12.17, minus the `disable iff` (sva T27) and the 128
/// bit model (the test evaluator does not slice): tags distinguish transactions,
/// a retry restarts the beat count at zero, a data beat after the last one is a
/// retry only if it comes one cycle after.
#[test]
fn t26_check_write_data_beat() {
    let decls = "logic wreq, wack, dv, rt, last; int model, wtag, dtag, rtag, data;
         property check_write;
           int expected_data; int tag;
           (wreq && wack, expected_data = model, tag = wtag)
           |=>
           check_write_data_beat(expected_data, tag, 0);
         endproperty
         property check_write_data_beat(local input int expected_data, tag, i);
           ((dv && (dtag == tag)) || (rt && (rtag == tag)))[->1]
           |->
           (
             ((dv && (dtag == tag)) |-> (data == expected_data + i))
             and
             (
               if (rt && (rtag == tag))
                 (1'b1 |=> check_write_data_beat(expected_data, tag, 0))
               else if (!last)
                 (1'b1 |=> check_write_data_beat(expected_data, tag, i + 1))
               else
                 (##1 (rt && (rtag == tag)) |=> check_write_data_beat(expected_data, tag, 0))
             )
           );
         endproperty";
    let run = |dv, dtag, data, rt, rtag, last| {
        assert_verdict(
            decls,
            "check_write",
            &[
                ("wreq", "1000000"),
                ("wack", "1000000"),
                ("model", "5000000"),
                ("wtag", "2000000"),
                ("dv", dv),
                ("dtag", dtag),
                ("data", data),
                ("rt", rt),
                ("rtag", rtag),
                ("last", last),
            ],
        )
    };
    // Two beats, the second the last: data 5 then 6.
    assert_eq!(
        run(
            "0110000", "0220000", "0560000", "0000000", "0000000", "0010000"
        ),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        run(
            "0110000", "0220000", "0570000", "0000000", "0000000", "0010000"
        ),
        Verdict::Fails
    );
    // A beat of another transaction is ignored.
    assert_eq!(
        run(
            "0110000", "0320000", "0950000", "0000000", "0000000", "0000000"
        ),
        Verdict::HoldsStrongly
    );
    // A retry (tick 2) restarts the count: the next beat is beat 0 again.
    assert_eq!(
        run(
            "0100100", "0200000", "0500500", "0010000", "0020000", "0000000"
        ),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        run(
            "0100100", "0200200", "0500700", "0010000", "0020000", "0000000"
        ),
        Verdict::Fails
    );
    // A retry one cycle after the last beat restarts it too.
    assert_eq!(
        run(
            "0100100", "0200200", "0500500", "0010000", "0020000", "0100000"
        ),
        Verdict::HoldsStrongly
    );
    assert_eq!(
        run(
            "0100100", "0200200", "0500600", "0010000", "0020000", "0100000"
        ),
        Verdict::Fails
    );
    // The three recursive instances are calls of the one declaration.
    assert_eq!(recursion_shape(decls, "check_write"), (1, 3));
}

/// Recursion through a swap of the actuals: the instance passes its formals on in
/// the other order, so it is a different binding than the instance it unfolds and
/// the recursion closes after two expansions (a recursive instance may pass a
/// formal or an expression over none, restriction 4).
#[test]
fn t26_recursion_through_permuted_formals() {
    let decls = "property alt(x, y); x and (1'b1 |=> alt(y, x)); endproperty";
    let run = |a, b| assert_verdict(decls, "alt(a, b)", &[("a", a), ("b", b)]);
    // `a` at the even ticks, `b` at the odd ones.
    assert_eq!(run("1010", "0101"), Verdict::HoldsStrongly);
    assert_eq!(run("1001", "0101"), Verdict::Fails);
    assert_eq!(run("1010", "0001"), Verdict::Fails);
    assert_eq!(recursion_shape(decls, "alt(a, b)"), (1, 1));
    // The two expansions are the declaration and its swap.
    with_property(decls, &ap("alt(a, b)"), false, |r, _| {
        let (ir, _) = r.unwrap();
        assert_eq!(
            ir.props
                .iter()
                .filter(|p| matches!(p, Prop::And(..)))
                .count(),
            2
        );
    });
}

/// Recursion with a binding that is not one of the formals: an expression over no
/// formal is a legal actual of a recursive instance (restriction 4).
#[test]
fn t26_recursive_instance_with_a_formal_free_actual() {
    let decls = "property fx(x, y); (x and y) and (1'b1 |=> fx(c, d)); endproperty";
    // The first instance is fx(a, b) at tick 0; every later one is fx(c, d), which
    // is its own unfolding.
    let run =
        |a, b, c, d| assert_verdict(decls, "fx(a, b)", &[("a", a), ("b", b), ("c", c), ("d", d)]);
    assert_eq!(run("1000", "1000", "0111", "0111"), Verdict::HoldsStrongly);
    // `c` and `d` are checked from tick 1 on, `a` and `b` only at tick 0.
    assert_eq!(run("1000", "1000", "0101", "0111"), Verdict::Fails);
    assert_eq!(run("1000", "1000", "0111", "0110"), Verdict::Fails);
    assert_eq!(run("0111", "1000", "0111", "0111"), Verdict::Fails);
    assert_eq!(run("1111", "1000", "0111", "0111"), Verdict::HoldsStrongly);
    assert_eq!(recursion_shape(decls, "fx(a, b)"), (1, 1));
}

/// slang unfolds a recursive instance one level past the first repeat of its
/// declaration and no further, so a chain of distinct bindings longer than that
/// (`sw(a, b)`, `sw(b, c)`, `sw(c, c)`, ...) reaches an instance with no body.
/// That is a named error, not a verdict from the wrong binding.
#[test]
fn t26_a_binding_chain_longer_than_slang_unfolds_is_a_named_error() {
    let msg = rejected(
        "property sw(x, y); x and (1'b1 |=> sw(y, c)); endproperty",
        "sw(a, b)",
    );
    assert!(
        msg.contains("16.12.17") && msg.contains("no body"),
        "sw: {msg}"
    );
    // The same when a `local` formal's actual would be needed from the instance
    // that has no body: a permutation of the non-local actuals closes the
    // recursion only there.
    let msg = rejected(
        "property alt2(x, y, local input int k); (x and (n == k)) and (1'b1 |=> alt2(y, x, k + 1)); endproperty",
        "alt2(a, b, 0)",
    );
    assert!(
        msg.contains("16.12.17") && msg.contains("local"),
        "alt2: {msg}"
    );
}

/// Restriction 1 (16.12.17, F.7): `not` and the strong operators cannot be
/// applied to a property expression that instantiates a recursive property, or
/// one from which a recursive property is reachable.
#[test]
fn t26_restriction_1_negation_of_a_recursive_property() {
    // slang diagnoses the restrictions of every declaration of the module, used
    // or not (and the builder's own check is the defence behind it), so each
    // illegal declaration is its own fixture and the legal forms a clean one.
    let wrapper = "property wrapper(p); prop_always(p); endproperty";
    for (extra, prop, why) in [
        (
            "property illegal_recursion_1(p); not prop_always(not p); endproperty",
            "illegal_recursion_1(a)",
            "the LRM's first example",
        ),
        (
            "property illegal_recursion_2(p); p and (1'b1 |=> not illegal_recursion_2(p)); endproperty",
            "illegal_recursion_2(a)",
            "the LRM's second example",
        ),
        ("", "not prop_always(a)", "the negation asserted"),
        (
            wrapper,
            "not wrapper(a)",
            "a property that depends on a recursive one (F.7)",
        ),
        (
            "",
            "prop_always(a) implies b",
            "implies negates its left operand",
        ),
        ("", "prop_always(a) iff b", "iff is two implies"),
        ("", "b iff prop_always(a)", "iff is two implies"),
        (
            "",
            "a #-# prop_always(b)",
            "a followed-by is a negated implication",
        ),
        ("", "s_nexttime prop_always(a)", "strong operator"),
        ("", "s_always [1:2] prop_always(a)", "strong operator"),
        ("", "s_eventually prop_always(a)", "strong operator"),
        ("", "prop_always(a) s_until b", "strong operator"),
        ("", "b s_until_with prop_always(a)", "strong operator"),
        (
            "property upto(p, q); q s_until prop_always(p); endproperty",
            "upto(a, b)",
            "a strong operator inside a wrapper",
        ),
    ] {
        let msg = rejected_lenient(&format!("{PROP_ALWAYS} {extra}"), prop);
        assert!(
            msg.contains("16.12.17") && msg.contains("restriction 1"),
            "{prop} ({why}): {msg}"
        );
    }
    // What stays legal: the weak operators, the abort operators, `not` on a
    // property with no recursion in it, and a recursive property on the side of
    // `implies` that is not negated.
    let ok = format!("{PROP_ALWAYS} {wrapper} property plain(p); p |=> b; endproperty");
    for prop in [
        "nexttime prop_always(a)",
        "always prop_always(a)",
        "eventually [1:2] prop_always(a)",
        "prop_always(a) until b",
        "prop_always(a) or prop_always(b)",
        "prop_always(a) and prop_always(b)",
        "a implies prop_always(b)",
        "a |-> prop_always(b)",
        "reject_on(b) prop_always(a)",
        "not plain(a)",
        "not (a ##1 b)",
        "wrapper(a)",
    ] {
        builds(&ok, prop);
    }
}

/// Restriction 2: `disable iff` cannot be used in the declaration of a recursive
/// property, but the legal form (a non-recursive property that wraps it) is a
/// `disable iff` like any other (sva T27's).
#[test]
fn t26_restriction_2_disable_iff_in_a_recursive_property() {
    let decls = format!(
        "{PROP_ALWAYS}
         property illegal_recursion_3(p); disable iff (b) p and (1'b1 |=> illegal_recursion_3(p)); endproperty
         property legal_3(p); disable iff (b) prop_always(p); endproperty
         property pa; disable iff (b) pb; endproperty
         property pb; a |=> pa; endproperty"
    );
    // slang diagnoses the first itself; the builder names the restriction.
    for prop in ["illegal_recursion_3(a)", "pa"] {
        let msg = rejected_lenient(&decls, prop);
        assert!(
            msg.contains("16.12.17") && msg.contains("restriction 2"),
            "{prop}: {msg}"
        );
    }
    // The legal form is a `disable iff` like any other.
    with_property(&decls, &ap("legal_3(a)"), true, |r, _| {
        let (ir, _) = r.expect("legal_3 builds");
        assert!(ir.disable.is_some(), "legal_3 lost its `disable iff`");
    });
}

/// Restriction 3: every recursive instance occurs after a positive advance in
/// time -- the sum over a cycle of the dependency digraph, not each edge.
#[test]
fn t26_restriction_3_positive_advance_in_time() {
    // Every illegal declaration is its own fixture: slang diagnoses all of the
    // declarations of a module (and the builder's check is the defence behind it).
    for (decl, prop) in [
        (
            "property illegal_recursion_4(p); p and (1'b1 |-> illegal_recursion_4(p)); endproperty",
            "illegal_recursion_4(a)",
        ),
        (
            "property ma; a |-> mb; endproperty property mb; b |-> ma; endproperty",
            "ma",
        ),
        (
            "property same(p); p and nexttime [0] same(p); endproperty",
            "same(a)",
        ),
        (
            "property wait0(p); p and (c ##[0:2] d |-> wait0(p)); endproperty",
            "wait0(a)",
        ),
        (
            "property ev(p); p and eventually [0:2] ev(p); endproperty",
            "ev(a)",
        ),
        (
            "property alw0(p); p and always [0:2] alw0(p); endproperty",
            "alw0(a)",
        ),
        (
            "property orbranch(p); (1'b1 |-> orbranch(p)) or (1'b1 |=> orbranch(p)); endproperty",
            "orbranch(a)",
        ),
    ] {
        let msg = rejected_lenient(decl, prop);
        assert!(
            msg.contains("16.12.17") && msg.contains("restriction 3"),
            "{prop}: {msg}"
        );
    }
    // A cycle whose edges sum to a positive weight is legal although one edge
    // has weight zero: `mc -> md` advances a tick, `md -> mc` none.
    let decls = "
         property mc; a |=> md; endproperty
         property md; b |-> mc; endproperty
         property nx(p); p and nexttime ev2(p); endproperty
         property ev2(p); p and (1'b1 |=> nx(p)); endproperty
         property alw(p); p and always [1:2] alw(p); endproperty";
    builds(decls, "mc");
    builds(decls, "md");
    builds(decls, "nx(a)");
    builds(decls, "alw(a)");
    // A delay inside the antecedent counts: the instance is after at least a tick.
    // (slang itself is more conservative than the LRM here and diagnoses the
    // declaration, so the fixture allows its errors.)
    let wait = "property wait1(p); p and (c ##[1:2] d |-> wait1(p)); endproperty";
    // `wait1(p)` needs `p` now and again one to two ticks after every match of the
    // antecedent `c ##[1:2] d`: here c at tick 0 matches at ticks 1 and 2 (d), so
    // `a` is owed at 0, 1 and 2.
    let run = |a| {
        verdict_in(
            wait,
            "wait1(a)",
            &[("a", a), ("c", "1000"), ("d", "0110")],
            0,
            false,
            true,
        )
    };
    assert_eq!(run("1110"), Verdict::HoldsStrongly);
    assert_eq!(run("1101"), Verdict::Fails);
    assert_eq!(run("1011"), Verdict::Fails);
    assert_eq!(run("0111"), Verdict::Fails);
}

/// Restriction 4: an actual of a recursive instance is a formal of the enclosing
/// declaration, or has none of them in it, or is bound to a local variable formal
/// (`fibonacci1` is legal, `fibonacci2` has `a + b` for a non-local formal).
#[test]
fn t26_restriction_4_actuals_of_a_recursive_instance() {
    // slang diagnoses the violation itself ("cannot refer to argument ... in an
    // argument to a recursive property") and leaves the actual unbound, which the
    // builder refuses loudly rather than build a property from nothing.
    for (decl, prop) in [
        (
            "property fibonacci2 (int a, b, n, fib_sig);
               (n > 0) |-> ((fib_sig == a) and (1'b1 |=> fibonacci2(b, a + b, n - 1, fib_sig)));
             endproperty",
            "fibonacci2(0, 1, 5, n)",
        ),
        (
            "property grow(p, int k); p and (1'b1 |=> grow(p, k + 1)); endproperty",
            "grow(a, 1)",
        ),
    ] {
        let msg = rejected_lenient(decl, prop);
        assert!(msg.contains("slang could not bind"), "{prop}: {msg}");
    }
    // One slang does not diagnose -- a `local` formal's value passed to a
    // non-local formal -- the builder names.
    let msg = rejected_lenient(
        "property mixed2(local input int k, int m); (n == k + m) and (1'b1 |=> mixed2(k, k)); endproperty",
        "mixed2(0, 2)",
    );
    assert!(
        msg.contains("16.12.17") && msg.contains("restriction 4") && msg.contains("`m`"),
        "mixed2: {msg}"
    );
    // The legal forms: a formal passed on, an expression over no formal, and an
    // expression over formals bound to a `local` formal (`fibonacci1`).
    let decls = "property fine(p, int k); p and (1'b1 |=> fine(p, 3)); endproperty
         property mixed(local input int k, int m); (n == k + m) and (1'b1 |=> mixed(k + 1, m)); endproperty";
    builds(decls, "fine(a, 1)");
    builds(decls, "mixed(0, 2)");
}

/// An instance of a recursive property outside any recursion is an ordinary
/// instance: expanded in place, a Boolean or sequence formal stays a formal, and
/// two instances in one property are two expansions.
#[test]
fn t26_several_instances_of_a_recursive_property() {
    weakly_equivalent(
        PROP_ALWAYS,
        "prop_always(a) and prop_always(b)",
        "always (a && b)",
        &["a", "b"],
        4,
    );
    weakly_equivalent(
        PROP_ALWAYS,
        "prop_always(a) or prop_always(b)",
        "(always a) or (always b)",
        &["a", "b"],
        4,
    );
    assert_eq!(
        recursion_shape(PROP_ALWAYS, "prop_always(a) and prop_always(b)"),
        (2, 2)
    );
}

/// `disable iff` (16.12, 16.15; sva T27).
mod disable;
/// Multiclocked sequences and properties (16.13, 16.16.1; sva T28).
mod multiclock;