vj-sim 0.2.0

//! 16.14.8: one test per lettered nonvacuity rule (a)-(ag), each on a vacuous and
//! a nonvacuous run of the minimal property shape. A run is a set of leaf rows
//! (`rows`: leaf `i` is row `i`, tick `t` its `t`-th character); the attempt
//! starts at tick 0.
use super::*;

/// Whether the attempt at tick 0 of the `len`-tick trace is nonvacuous.
fn nv(ir: &PropertyIr, env: &Rows, len: u32) -> bool {
    Evaluator::new(ir, env, false).nonvacuous(len, 0).unwrap()
}

/// The leaf `l` as a bare (weak) sequence property.
fn seq(b: &mut B, l: u32) -> PropId {
    b.b(l, None)
}

/// `a |-> c` (or `a |=> c`) over the leaves `a` and `c`.
fn imp(b: &mut B, a: u32, c: u32, overlapped: bool) -> PropId {
    let ante = b.leaf(a);
    let cons = seq(b, c);
    b.prop(Prop::Implication {
        ante,
        cons,
        overlapped,
    })
}

/// `l0 |-> l1`, the canonical vacuous-success property.
fn a_implies_b(b: &mut B) -> PropId {
    imp(b, 0, 1, true)
}

/// `x |-> y` on the leaves 2 and 3, the second implication of the binary rules.
fn c_implies_d(b: &mut B) -> PropId {
    imp(b, 2, 3, true)
}

#[test]
fn the_canonical_example_a_implies_b_is_a_vacuous_success_when_a_is_false() {
    let mut b = B::new();
    let root = a_implies_b(&mut b);
    let ir = b.finish(root);
    let vacuous = rows(&["0", "0"]);
    assert_eq!(verdict(&ir, &vacuous, 1, 0, false), Verdict::HoldsStrongly);
    assert!(!nv(&ir, &vacuous, 1), "a false: the success is vacuous");
    let real = rows(&["1", "1"]);
    assert_eq!(verdict(&ir, &real, 1, 0, false), Verdict::HoldsStrongly);
    assert!(nv(&ir, &real, 1), "a true, b true: nonvacuous success");
    let fail = rows(&["1", "0"]);
    assert_eq!(verdict(&ir, &fail, 1, 0, false), Verdict::Fails);
    assert!(nv(&ir, &fail, 1), "a failure is a nonvacuous evaluation");
}

/// (a), (b), (c): a sequence, `strong(seq)` and `weak(seq)` are always
/// nonvacuous, whatever they evaluate to.
#[test]
fn rule_a_b_c_sequences_are_always_nonvacuous() {
    for strength in [None, Some(Strength::Strong), Some(Strength::Weak)] {
        let mut b = B::new();
        let root = b.b(0, strength);
        let ir = b.finish(root);
        assert!(nv(&ir, &rows(&["0"]), 1), "{strength:?} false");
        assert!(nv(&ir, &rows(&["1"]), 1), "{strength:?} true");
    }
}

/// (d): `not p` is nonvacuous iff `p` is.
#[test]
fn rule_d_not() {
    let mut b = B::new();
    let p = a_implies_b(&mut b);
    let root = b.not(p);
    let ir = b.finish(root);
    assert!(!nv(&ir, &rows(&["0", "0"]), 1));
    assert!(nv(&ir, &rows(&["1", "0"]), 1));
}

/// (e): `or` is nonvacuous iff either operand is; (f): so is `and`.
#[test]
fn rule_e_f_or_and_and() {
    for or in [true, false] {
        let mut b = B::new();
        let (p, q) = (a_implies_b(&mut b), c_implies_d(&mut b));
        let root = b.prop(if or { Prop::Or(p, q) } else { Prop::And(p, q) });
        let ir = b.finish(root);
        assert!(!nv(&ir, &rows(&["0", "0", "0", "0"]), 1), "or={or} neither");
        assert!(nv(&ir, &rows(&["1", "1", "0", "0"]), 1), "or={or} left");
        assert!(nv(&ir, &rows(&["0", "0", "1", "1"]), 1), "or={or} right");
    }
}

/// (g): `if (c) p` needs `c` true and `p` nonvacuous; with an `else`, either
/// branch taken nonvacuously.
#[test]
fn rule_g_if_and_if_else() {
    // leaves: 0 = a, 1 = b, 2 = c (condition), 3 = d, 4 = e
    let mut b = B::new();
    let then = a_implies_b(&mut b);
    let plain = b.prop(Prop::If {
        cond: LeafId(2),
        then,
        els: None,
    });
    let els = imp(&mut b, 3, 4, true);
    let full = b.prop(Prop::If {
        cond: LeafId(2),
        then,
        els: Some(els),
    });
    let mut ir = b.finish(plain);
    let cond_false = rows(&["1", "1", "0", "1", "1"]);
    let cond_true_vac = rows(&["0", "0", "1", "0", "0"]);
    let cond_true = rows(&["1", "1", "1", "0", "0"]);
    assert!(!nv(&ir, &cond_false, 1), "no else, condition false");
    assert!(!nv(&ir, &cond_true_vac, 1), "condition true, p vacuous");
    assert!(nv(&ir, &cond_true, 1), "condition true, p nonvacuous");
    ir.root = full;
    assert!(nv(&ir, &cond_false, 1), "else branch nonvacuous");
    assert!(
        !nv(&ir, &rows(&["1", "1", "0", "0", "0"]), 1),
        "else vacuous"
    );
    assert!(nv(&ir, &cond_true, 1), "then branch nonvacuous");
}

/// (h): `s |-> p` / `s |=> p`: an end point of `s` and a nonvacuous `p` from
/// there (the next clock event for `|=>`).
#[test]
fn rule_h_overlapped_and_nonoverlapped_implication() {
    let mut b = B::new();
    let over = a_implies_b(&mut b);
    let non = imp(&mut b, 0, 1, false);
    let mut ir = b.finish(over);
    assert!(!nv(&ir, &rows(&["0", "0"]), 1), "|-> antecedent false");
    assert!(nv(&ir, &rows(&["1", "1"]), 1), "|-> match");
    ir.root = non;
    assert!(!nv(&ir, &rows(&["00", "00"]), 2), "|=> antecedent false");
    assert!(
        nv(&ir, &rows(&["10", "01"]), 2),
        "|=> match, next tick exists"
    );
    assert!(
        !nv(&ir, &rows(&["1", "0"]), 1),
        "|=> match on the last tick: no clock event follows it"
    );
}

/// (i): an instance is nonvacuous iff the body with the actuals substituted is.
#[test]
fn rule_i_property_instance() {
    let mut b = B::new();
    let body = a_implies_b(&mut b);
    b.decls.push(PropDecl {
        name: "p".into(),
        body,
    });
    let call = b.prop(Prop::Call {
        decl: DeclId(0),
        args: Vec::new(),
        inits: Vec::new(),
    });
    let ir = b.finish(call);
    assert!(!nv(&ir, &rows(&["0", "0"]), 1));
    assert!(nv(&ir, &rows(&["1", "1"]), 1));
}

/// (j): `s #-# p` has an end point of `s` and a nonvacuous `p` there; (k):
/// `s #=# p` the next clock event after it. Both are `not (s |-> not p)`.
#[test]
fn rule_j_k_followed_by() {
    for overlapped in [true, false] {
        let mut b = B::new();
        let ante = b.leaf(0);
        let cons = seq(&mut b, 1);
        let ncons = b.not(cons);
        let imp = b.prop(Prop::Implication {
            ante,
            cons: ncons,
            overlapped,
        });
        let root = b.not(imp);
        let ir = b.finish(root);
        assert!(!nv(&ir, &rows(&["00", "00"]), 2), "overlapped={overlapped}");
        assert!(nv(&ir, &rows(&["10", "11"]), 2), "overlapped={overlapped}");
    }
}

/// (l)-(o): `nexttime`, `s_nexttime`, with and without a count: the clock event
/// must exist and `p` be nonvacuous on it.
#[test]
fn rule_l_m_n_o_nexttime() {
    for (n, strong) in [(1, false), (2, false), (1, true), (2, true)] {
        let mut b = B::new();
        let p = a_implies_b(&mut b);
        let root = b.prop(Prop::Nexttime { p, n, strong });
        let ir = b.finish(root);
        let len = n + 1;
        let (a, bb) = ("0".repeat(n as usize) + "1", "0".repeat(n as usize) + "1");
        assert!(nv(&ir, &rows(&[&a, &bb]), len), "n={n} strong={strong}");
        let vac = "0".repeat(len as usize);
        assert!(!nv(&ir, &rows(&[&vac, &vac]), len), "n={n} vacuous");
        assert!(
            !nv(&ir, &rows(&[&a, &bb]), n),
            "n={n} strong={strong}: only {n} tick(s), the n-th clock event does not exist"
        );
    }
}

/// (p), (q), (r): `always`, `always[m:n]`, `s_always[m:n]`: a clock event where
/// `p` is nonvacuous, `p` not having failed before it.
#[test]
fn rule_p_q_r_always() {
    for (lo, hi, strong) in [(0, None, false), (1, Some(2), false), (1, Some(2), true)] {
        let mut b = B::new();
        let p = a_implies_b(&mut b);
        let root = b.prop(Prop::Always { p, lo, hi, strong });
        let ir = b.finish(root);
        assert!(!nv(&ir, &rows(&["0000", "0000"]), 4), "{lo} {hi:?} vacuous");
        assert!(
            nv(&ir, &rows(&["0110", "0110"]), 4),
            "{lo} {hi:?} nonvacuous"
        );
        // The only nonvacuous event is outside the range [1:2].
        if lo == 1 {
            assert!(!nv(&ir, &rows(&["1000", "1000"]), 4), "{lo} outside");
        }
    }
    // Failed before the nonvacuous event: `not (a |-> b)` fails (vacuously) at
    // tick 0 and would be nonvacuous at tick 1.
    let mut b = B::new();
    let imp = a_implies_b(&mut b);
    let p = b.not(imp);
    let root = b.prop(Prop::Always {
        p,
        lo: 0,
        hi: None,
        strong: false,
    });
    let ir = b.finish(root);
    assert!(!nv(&ir, &rows(&["01", "00"]), 2), "failed in a prior event");
}

/// (s), (t), (u): `s_eventually`, `s_eventually[m:n]`, `eventually[m:n]`: a
/// clock event where `p` is nonvacuous, `p` not having held before it.
#[test]
fn rule_s_t_u_eventually() {
    for (lo, hi, strong) in [(0, None, true), (1, Some(2), true), (1, Some(2), false)] {
        let mut b = B::new();
        let p = a_implies_b(&mut b);
        let root = b.prop(Prop::Eventually { p, lo, hi, strong });
        let ir = b.finish(root);
        // `a` and `b` are both the row: `1` at index `k` is a nonvacuous event.
        let at = |k: usize| {
            let row: String = (0..4).map(|i| if i == k { '1' } else { '0' }).collect();
            rows(&[&row, &row])
        };
        let lo = lo as usize;
        assert!(!nv(&ir, &rows(&["0000", "0000"]), 4), "{lo} vacuous");
        assert!(nv(&ir, &at(lo), 4), "{lo}: nonvacuous at the first event");
        // `p` holds (vacuously) at the first event of the range, so a later
        // nonvacuous event does not count.
        assert!(!nv(&ir, &at(lo + 1), 4), "{lo}: p held at an earlier event");
    }
}

/// (v), (w) `until`/`s_until`: a clock event where either operand is
/// nonvacuous, `q` not having held and `p` having held at every one before it.
#[test]
fn rule_v_w_until() {
    for strong in [false, true] {
        let mut b = B::new();
        let (p, q) = (a_implies_b(&mut b), c_implies_d(&mut b));
        let root = b.prop(Prop::Until { p, q, strong });
        let ir = b.finish(root);
        let none = rows(&["000", "000", "000", "000"]);
        assert!(
            !nv(&ir, &none, 3),
            "strong={strong} both vacuous throughout"
        );
        // q's antecedent first holds at tick 1, but `q` held (vacuously) at tick
        // 0 already: the until is over before any nonvacuous event.
        let late = rows(&["000", "000", "010", "010"]);
        assert!(!nv(&ir, &late, 3), "strong={strong} q held before tick 1");
        let p_nv = rows(&["100", "100", "000", "000"]);
        assert!(nv(&ir, &p_nv, 3), "strong={strong} p nonvacuous at tick 0");
        let q_nv = rows(&["000", "000", "100", "100"]);
        assert!(nv(&ir, &q_nv, 3), "strong={strong} q nonvacuous at tick 0");
    }
}

/// (x), (y) `until_with`/`s_until_with`: only `p` counts, `q` being nonvacuous
/// alone does not. (`p until (p and q)`, so the derived node carries the rule.)
#[test]
fn rule_x_y_until_with() {
    for strong in [false, true] {
        let mut b = B::new();
        let (p, q) = (a_implies_b(&mut b), c_implies_d(&mut b));
        let both = b.prop(Prop::And(p, q));
        let root = b.prop(Prop::Until { p, q: both, strong });
        let mut ir = b.finish(root);
        // q's antecedent is true at tick 0 with d true; p's is false.
        let only_q = rows(&["000", "000", "100", "100"]);
        assert!(
            nv(&ir, &only_q, 3),
            "strong={strong}: without the rule the `and` makes q count"
        );
        ir.nv_rules.push((root, NvRule::UntilWith));
        assert!(
            !nv(&ir, &only_q, 3),
            "strong={strong}: with the rule p only"
        );
        let p_nv = rows(&["100", "100", "000", "000"]);
        assert!(nv(&ir, &p_nv, 3), "strong={strong}: p nonvacuous");
    }
}

/// (z) `p implies q`: `p` true and nonvacuous, and `q` nonvacuous.
#[test]
fn rule_z_implies() {
    let mut b = B::new();
    let p = seq(&mut b, 0);
    let q = c_implies_d(&mut b);
    let not_p = b.not(p);
    let root = b.prop(Prop::Or(not_p, q));
    let mut ir = b.finish(root);
    ir.nv_rules.push((root, NvRule::Implies));
    assert!(
        nv(&ir, &rows(&["1", "0", "1", "1"]), 1),
        "p true, q nonvacuous"
    );
    assert!(!nv(&ir, &rows(&["0", "0", "1", "1"]), 1), "p false");
    assert!(!nv(&ir, &rows(&["1", "0", "0", "0"]), 1), "q vacuous");
    // Without the rule (the plain `or`) the false `p` side counts.
    ir.nv_rules.clear();
    assert!(nv(&ir, &rows(&["0", "0", "1", "1"]), 1));
}

/// (aa) `p iff q`: either operand nonvacuous (two `implies` as plain `or`s).
#[test]
fn rule_aa_iff() {
    let mut b = B::new();
    let (p, q) = (a_implies_b(&mut b), c_implies_d(&mut b));
    let (np, nq) = (b.not(p), b.not(q));
    let (pq, qp) = (b.prop(Prop::Or(np, q)), b.prop(Prop::Or(nq, p)));
    let root = b.prop(Prop::And(pq, qp));
    let ir = b.finish(root);
    assert!(!nv(&ir, &rows(&["0", "0", "0", "0"]), 1));
    assert!(nv(&ir, &rows(&["1", "1", "0", "0"]), 1));
    assert!(nv(&ir, &rows(&["0", "0", "1", "1"]), 1));
}

/// (ab)-(ae): `accept_on`, `reject_on`, `sync_accept_on`, `sync_reject_on`: `p`
/// nonvacuous and the condition (leaf 4) true at no time step of the attempt.
#[test]
fn rule_ab_ac_ad_ae_abort() {
    for mode in AbortMode::ALL {
        let mut b = B::new();
        let p = a_implies_b(&mut b);
        let root = b.prop(Prop::Abort {
            cond: LeafId(4),
            p,
            mode,
        });
        let ir = b.finish(root);
        let quiet = rows(&["110", "110", "000", "000", "000"]);
        let aborted = rows(&["110", "110", "000", "000", "010"]);
        let vacuous = rows(&["000", "000", "000", "000", "000"]);
        assert!(nv(&ir, &quiet, 3), "{mode:?} nonvacuous, condition false");
        assert!(!nv(&ir, &aborted, 3), "{mode:?} condition true at tick 1");
        assert!(!nv(&ir, &vacuous, 3), "{mode:?} p vacuous");
    }
}

/// (af) `case`: the selected arm's statement nonvacuous, the `default`'s when
/// no label matches (and none at all when there is no default).
#[test]
fn rule_af_case() {
    // leaves: 0 selector, 1 label, 2/3 arm `x |-> y`, 4/5 default `x |-> y`
    let mut b = B::new();
    let arm = imp(&mut b, 2, 3, true);
    let default = imp(&mut b, 4, 5, true);
    let with_default = b.prop(Prop::Case {
        selector: LeafId(0),
        arms: vec![CaseArm {
            labels: vec![LeafId(1)],
            body: arm,
        }],
        default: Some(default),
    });
    let without = b.prop(Prop::Case {
        selector: LeafId(0),
        arms: vec![CaseArm {
            labels: vec![LeafId(1)],
            body: arm,
        }],
        default: None,
    });
    let mut ir = b.finish(with_default);
    let selected = rows(&["1", "1", "1", "1", "0", "0"]);
    let selected_vacuous = rows(&["1", "1", "0", "0", "1", "1"]);
    let defaulted = rows(&["1", "0", "0", "0", "1", "1"]);
    let defaulted_vacuous = rows(&["1", "0", "1", "1", "0", "0"]);
    assert!(nv(&ir, &selected, 1), "arm selected, nonvacuous");
    assert!(!nv(&ir, &selected_vacuous, 1), "arm selected, vacuous");
    assert!(nv(&ir, &defaulted, 1), "default taken, nonvacuous");
    assert!(!nv(&ir, &defaulted_vacuous, 1), "default taken, vacuous");
    ir.root = without;
    assert!(!nv(&ir, &defaulted, 1), "no arm, no default");
    assert!(nv(&ir, &selected, 1));
}

/// (ag) `disable iff (c) p`: `p` nonvacuous and `c` true at no time step of the
/// attempt. The attempt is `nexttime (a |-> b)` on a 3-tick trace; `c` (leaf 4)
/// true at tick 1 ends the attempt before the nonvacuous event at tick 1.
#[test]
fn rule_ag_disable_iff() {
    let mut b = B::new();
    let imp = a_implies_b(&mut b);
    let root = b.prop(Prop::Nexttime {
        p: imp,
        n: 1,
        strong: false,
    });
    let mut ir = b.finish(root);
    ir.disable = Some(LeafId(4));
    let free = rows(&["011", "011", "000", "000", "000"]);
    let disabled = rows(&["011", "011", "000", "000", "010"]);
    assert!(nv(&ir, &free, 3), "disable never true");
    assert!(!nv(&ir, &disabled, 3), "disable true at tick 1");
}