vj-sim 0.2.0

//! 16.11: the subroutine calls of an evaluation attempt (`Evaluator::scheduled_calls`,
//! `Evaluator::sequence_calls`). Leaf `i` is row `i` of `rows`; a call's by-value
//! argument is a leaf's value at the call's tick (0 or 1 here).
use super::*;
use crate::sva::ir::{CallArg, CallId};

fn ev(tick: u32, call: u32, args: &[Option<i64>]) -> CallEvent {
    CallEvent {
        tick,
        call: CallId(call),
        args: args.to_vec(),
    }
}

/// `(l0, call#0(l1, ref)) ##1 (l2, call#1(const))`: the antecedent shape every
/// test below uses, with the two calls the LRM's `s2` example has.
fn calling_sequence(b: &mut B) -> SeqRef {
    let entry = b.au.new_state();
    let s1 = b.au.new_state();
    let s2 = b.au.new_state();
    let s3 = b.au.new_state();
    let s4 = b.au.new_state();
    let s5 = b.au.new_state();
    let s6 = b.au.new_state();
    b.au.add_edge(entry, Some(LeafId(0)), Transition::Epsilon, s1);
    b.au.add_edge(
        s1,
        None,
        Transition::SubroutineCall {
            call: CallId(0),
            args: vec![CallArg::Value(LeafId(1)), CallArg::Ref],
        },
        s2,
    );
    b.au.add_edge(
        s2,
        None,
        Transition::Delay {
            min: 1,
            max: Some(1),
        },
        s3,
    );
    b.au.add_edge(s3, Some(LeafId(2)), Transition::Epsilon, s4);
    b.au.add_edge(
        s4,
        None,
        Transition::SubroutineCall {
            call: CallId(1),
            args: vec![CallArg::Const],
        },
        s5,
    );
    b.au.add_edge(
        s5,
        None,
        Transition::Match {
            actions: Vec::new(),
        },
        s6,
    );
    SeqRef::single(entry, false)
}

/// `calling_sequence |-> l3`.
fn implication(b: &mut B) -> PropertyIr {
    let ante = calling_sequence(b);
    let cons = b.b(3, None);
    let root = b.prop(Prop::Implication {
        ante,
        cons,
        overlapped: true,
    });
    std::mem::replace(b, B::new()).finish(root)
}

fn calls(ir: &PropertyIr, env: &Rows, len: u32, start: u32) -> Vec<CallEvent> {
    Evaluator::new(ir, env, false)
        .open_future()
        .scheduled_calls(len, start)
        .unwrap()
}

#[test]
fn a_pending_attempt_lists_the_calls_of_its_prefix_and_a_longer_trace_only_adds() {
    let mut b = B::new();
    let ir = implication(&mut b);
    // l0 at ticks 0 and 1, l1 high at tick 0, l2 at tick 1; l3 always.
    let env = rows(&["110", "100", "010", "111"]);
    assert_eq!(calls(&ir, &env, 1, 0), vec![ev(0, 0, &[Some(1), None])]);
    assert_eq!(
        calls(&ir, &env, 2, 0),
        vec![ev(0, 0, &[Some(1), None]), ev(1, 1, &[None])],
        "the second call joins at its own tick; the first stays"
    );
    assert_eq!(calls(&ir, &env, 3, 0), calls(&ir, &env, 2, 0));
}

#[test]
fn a_call_carries_the_sampled_value_of_its_by_value_argument_at_its_tick() {
    let mut b = B::new();
    let ir = implication(&mut b);
    let env = rows(&["100", "000", "010", "111"]);
    assert_eq!(calls(&ir, &env, 1, 0), vec![ev(0, 0, &[Some(0), None])]);
}

/// 16.11: the call fires whether or not the property then holds: the consequent
/// `l3` is false at the end point, the implication fails, both calls are listed.
#[test]
fn a_failing_attempt_still_lists_its_calls() {
    let mut b = B::new();
    let ir = implication(&mut b);
    let env = rows(&["110", "100", "010", "000"]);
    let ev_ = Evaluator::new(&ir, &env, false).open_future();
    assert_eq!(ev_.verdict(2, 0).unwrap(), Verdict::Fails);
    assert_eq!(
        ev_.scheduled_calls(2, 0).unwrap(),
        vec![ev(0, 0, &[Some(1), None]), ev(1, 1, &[None])]
    );
}

/// A thread that never matches still scheduled the calls it passed.
#[test]
fn a_thread_that_never_matches_keeps_the_calls_it_passed() {
    let mut b = B::new();
    let ir = implication(&mut b);
    // `l2` never holds: the sequence cannot match, call #0 still fired.
    let env = rows(&["100", "100", "000", "111"]);
    assert_eq!(calls(&ir, &env, 3, 0), vec![ev(0, 0, &[Some(1), None])]);
}

/// The first failing operand of `and` must not hide the other operand's calls.
#[test]
fn and_evaluates_both_operands_when_collecting_calls() {
    let mut b = B::new();
    let left = b.b(3, None);
    let ante = calling_sequence(&mut b);
    let right = b.prop(Prop::Seq {
        seq: ante,
        strength: None,
    });
    let root = b.prop(Prop::And(left, right));
    let ir = b.finish(root);
    // `l3` is false: the conjunction fails on its first operand.
    let env = rows(&["110", "100", "010", "000"]);
    let ev_ = Evaluator::new(&ir, &env, false).open_future();
    assert_eq!(ev_.verdict(2, 0).unwrap(), Verdict::Fails);
    assert_eq!(
        ev_.scheduled_calls(2, 0).unwrap(),
        vec![ev(0, 0, &[Some(1), None]), ev(1, 1, &[None])]
    );
}

/// ... and a true first operand of `or` must not hide the other operand's calls.
#[test]
fn or_evaluates_both_operands_when_collecting_calls() {
    let mut b = B::new();
    let left = b.b(3, None);
    let ante = calling_sequence(&mut b);
    let right = b.prop(Prop::Seq {
        seq: ante,
        strength: None,
    });
    let root = b.prop(Prop::Or(left, right));
    let ir = b.finish(root);
    let env = rows(&["110", "100", "010", "111"]);
    let ev_ = Evaluator::new(&ir, &env, false).open_future();
    assert_eq!(ev_.verdict(2, 0).unwrap(), Verdict::HoldsStrongly);
    assert_eq!(
        ev_.scheduled_calls(2, 0).unwrap(),
        vec![ev(0, 0, &[Some(1), None]), ev(1, 1, &[None])]
    );
}

/// An implication whose first end point already fails the consequent still lists
/// the calls of the antecedent's later end points: `(l0, call#0()) ##[1:2] l2`
/// matches at ticks 1 and 2 and the consequent is false at tick 1 only.
#[test]
fn implication_evaluates_every_end_point_when_collecting_calls() {
    let mut b = B::new();
    let entry = b.au.new_state();
    let s1 = b.au.new_state();
    let s2 = b.au.new_state();
    let s3 = b.au.new_state();
    let s4 = b.au.new_state();
    let s5 = b.au.new_state();
    b.au.add_edge(entry, Some(LeafId(0)), Transition::Epsilon, s1);
    b.au.add_edge(
        s1,
        None,
        Transition::Delay {
            min: 1,
            max: Some(2),
        },
        s2,
    );
    b.au.add_edge(s2, Some(LeafId(2)), Transition::Epsilon, s3);
    b.au.add_edge(
        s3,
        None,
        Transition::SubroutineCall {
            call: CallId(0),
            args: vec![],
        },
        s4,
    );
    b.au.add_edge(
        s4,
        None,
        Transition::Match {
            actions: Vec::new(),
        },
        s5,
    );
    let ante = SeqRef::single(entry, false);
    let cons = b.b(3, None);
    let root = b.prop(Prop::Implication {
        ante,
        cons,
        overlapped: true,
    });
    let ir = b.finish(root);
    // l2 holds at ticks 1 and 2; l3 (the consequent) is false at tick 1 only.
    let env = rows(&["1000", "0000", "0110", "0010"]);
    let ev_ = Evaluator::new(&ir, &env, false).open_future();
    assert_eq!(ev_.verdict(3, 0).unwrap(), Verdict::Fails);
    assert_eq!(
        ev_.scheduled_calls(3, 0).unwrap(),
        vec![ev(1, 0, &[]), ev(2, 0, &[])]
    );
}

/// 16.12: the attempt is judged on the letters before its `disable iff`: a call
/// at or after the disabling tick is not the attempt's.
#[test]
fn calls_at_or_after_the_disabling_tick_are_not_listed() {
    let mut b = B::new();
    let mut ir = implication(&mut b);
    ir.disable = Some(LeafId(4));
    // The disable condition (leaf 4) is first true at tick 1.
    let env = rows(&["110", "100", "010", "111", "010"]);
    assert_eq!(calls(&ir, &env, 3, 0), vec![ev(0, 0, &[Some(1), None])]);
    // A condition never true leaves both.
    let env = rows(&["110", "100", "010", "111", "000"]);
    assert_eq!(calls(&ir, &env, 3, 0).len(), 2);
}

/// An attempt starts at its own tick: only the threads it started there.
#[test]
fn a_later_start_lists_only_its_own_threads() {
    let mut b = B::new();
    let ir = implication(&mut b);
    let env = rows(&["110", "100", "010", "111"]);
    // Started at tick 1: l0 holds, call #0 fires at tick 1; l2 at tick 2 is false.
    assert_eq!(calls(&ir, &env, 3, 1), vec![ev(1, 0, &[Some(0), None])]);
}

/// A call scheduled by a thread of a letter tick (past the real samples) is
/// not a call of the simulation.
#[test]
fn a_call_on_a_top_or_bottom_letter_is_not_listed() {
    let mut b = B::new();
    let ir = implication(&mut b);
    // One real sample: `l2` at tick 1 would be satisfied by a letter, but no
    // sample exists there.
    let env = rows(&["110", "100", "010", "111"]);
    assert_eq!(calls(&ir, &env, 1, 0), vec![ev(0, 0, &[Some(1), None])]);
}

#[test]
fn sequence_calls_lists_the_calls_of_a_cover_sequence_root() {
    let mut b = B::new();
    let seq = calling_sequence(&mut b);
    let root = b.prop(Prop::Seq {
        seq,
        strength: None,
    });
    let ir = b.finish(root);
    let env = rows(&["110", "100", "010"]);
    let evaluator = Evaluator::new(&ir, &env, true);
    assert_eq!(
        evaluator.sequence_calls(2, 0).unwrap(),
        vec![ev(0, 0, &[Some(1), None]), ev(1, 1, &[None])]
    );
    assert_eq!(
        evaluator.sequence_calls(1, 0).unwrap(),
        vec![ev(0, 0, &[Some(1), None])]
    );
}

#[test]
fn sequence_calls_stop_at_the_disabling_tick() {
    let mut b = B::new();
    let seq = calling_sequence(&mut b);
    let root = b.prop(Prop::Seq {
        seq,
        strength: None,
    });
    let mut ir = b.finish(root);
    ir.disable = Some(LeafId(4));
    let env = rows(&["110", "100", "010", "111", "010"]);
    let evaluator = Evaluator::new(&ir, &env, true);
    assert_eq!(
        evaluator.sequence_calls(3, 0).unwrap(),
        vec![ev(0, 0, &[Some(1), None])]
    );
}

/// Collecting calls leaves no state behind: a verdict asked afterwards is the
/// same as on a fresh evaluator.
#[test]
fn collecting_calls_does_not_change_later_verdicts() {
    let mut b = B::new();
    let ir = implication(&mut b);
    let env = rows(&["110", "100", "010", "000"]);
    let ev_ = Evaluator::new(&ir, &env, false).open_future();
    let before = ev_.verdict(2, 0).unwrap();
    ev_.scheduled_calls(2, 0).unwrap();
    assert_eq!(ev_.verdict(2, 0).unwrap(), before);
    assert_eq!(ev_.attempt(2, 0).unwrap(), Disposition::Fails);
}