Skip to content
Snippets Groups Projects
sep_seq.rs 6.97 KiB
Newer Older
use super::equivalence_trait::{CounterExample, EquivalenceOracle, InternalEquivalenceOracle};
use crate::{
    automatadefs::{
        mealy::{InputSymbol, Mealy, State},
Bharat Garhewal's avatar
Bharat Garhewal committed
        traits::{FiniteStateMachine, ObservationTree},
    },
    learner::apartness::{compute_witness, states_are_apart},
    oracles::membership::Oracle as OQOracle,
    util::toolbox,
};
use fnv::FnvHashSet;
use itertools::Itertools;
use rand::prelude::{SeedableRng, SliceRandom, StdRng};
use rayon::iter::{IntoParallelRefIterator, ParallelIterator};
use std::{cell::RefCell, collections::HashMap, rc::Rc};

/// Separating Sequence Oracle (Observation Tree-based)
///
/// This is a new equivalence oracle, based on the observation
/// tree and the hypothesis, rather than just the hypothesis.
/// More explanation will be added as the oracle is developed.
pub struct SequenceOracle<'a, T> {
    oq_oracle: Rc<RefCell<OQOracle<'a, T>>>,
    lookahead: usize,
    rng: StdRng,
}

impl<'a, T> InternalEquivalenceOracle<'a, T> for SequenceOracle<'a, T>
where
    T: ObservationTree + Sync + Send,
{
    fn new(oq_oracle: Rc<RefCell<OQOracle<'a, T>>>, lookahead: usize, seed: u64) -> Self {
        Self {
            oq_oracle,
            lookahead,
            rng: StdRng::seed_from_u64(seed),
        }
    }
}

impl<'a, T> EquivalenceOracle<'a, T> for SequenceOracle<'a, T>
where
    T: ObservationTree + Sync + Send,
{
    type Options = ();
    fn get_counts(&mut self) -> (usize, usize) {
        RefCell::borrow_mut(&self.oq_oracle).get_counts()
    }

    #[must_use]
    fn find_counterexample_with_lookahead(
        &mut self,
        hypothesis: &Mealy,
        lookahead: usize,
    ) -> CounterExample {
        let hyp_states = hypothesis.states().into_iter().collect_vec();
        if hyp_states.len() == 1 {
            return self.find_counterexample_initial(hypothesis);
        }
        let access_map = self.construct_access_map(hyp_states.clone()); // S -> Access Seq.
        let input_size = hypothesis.input_alphabet().len();
        let mut input_alphabet: Vec<_> = (0..input_size)
            .into_iter()
            .map(|x| x as u16)
            .map(InputSymbol::from)
            .collect_vec();
        input_alphabet.shuffle(&mut self.rng);
        let lookahead_range = (1..=lookahead + 1).into_iter().collect_vec();
        let infix_closure = || {
            Iterator::flatten(lookahead_range.iter().map(|&n| {
                itertools::repeat_n(input_alphabet.iter().copied(), n as _)
                    .multi_cartesian_product()
            }))
        };

        log::info!("Running AIC sequences.");
        for infix in infix_closure() {
            for (&s, access_seq) in &access_map {
                let temp = RefCell::borrow(&self.oq_oracle);
                let tree = temp.borrow_tree();
                let tree_dest = tree.get_succ(s, &infix);
                let hyp_dest = hypothesis.trace_from(s, &infix).0;
                let sep_set = Self::separating_set(&hyp_states, hyp_dest, tree_dest, tree);
                drop(temp);
                for sep_seq in sep_set {
                    let input_seq = toolbox::concat_slices(&[access_seq, &infix, &sep_seq]);
                    if let Some(ce) = self.run_test(hypothesis, &input_seq) {
                        return Some(ce);
                    }
                }
            }
        }
        log::info!("Running AC sequences.");
        for (&s, access_seq) in &access_map {
            let temp = RefCell::borrow(&self.oq_oracle);
            let tree = temp.borrow_tree();
            let sep_set: FnvHashSet<_> = hyp_states
                .iter()
                .copied()
                .filter(|&q| q != s)
                .map(|q| compute_witness(tree, q, s).unwrap())
                .collect();
            drop(temp);
            assert!(!sep_set.is_empty());
            for seq in sep_set {
                let input_seq = toolbox::concat_slices(&[access_seq, &seq]);
                if let Some(x) = self.run_test(hypothesis, &input_seq) {
                    return Some(x);
                }
            }
        }

        None
    }

    fn find_counterexample(&mut self, hypothesis: &Mealy) -> CounterExample {
        self.find_counterexample_with_lookahead(hypothesis, self.lookahead)
    }
}

impl<'a, T> SequenceOracle<'a, T>
where
    T: ObservationTree + Sync + Send,
{
    #[inline]
    #[must_use]
    fn separating_set(
        hyp_states: &[State],
        hyp_dest: State,
        tree_dest: Option<State>,
        tree: &T,
    ) -> FnvHashSet<Vec<InputSymbol>> {
        hyp_states
            .par_iter()
            .copied()
            .filter(|&s| s != hyp_dest)
            .filter(|&s| {
                tree_dest.map_or_else(|| true, |tree_dest| !states_are_apart(tree, s, tree_dest))
            })
            .map(|s| compute_witness(tree, s, hyp_dest).unwrap())
            .collect()
    }

    /// Specialised case for when the hypothesis is a single-state FSM.
    #[must_use]
    fn find_counterexample_initial(&mut self, hyp: &Mealy) -> CounterExample {
        // When the hypothesis has size one, there's no point in testing A.C,
        // as we will have no characterising set.
        // A similar argument works for A.I.C, as C is empty.
        // A will contain only the empty sequence,
        // since we are already in the initial state;
        // Therefore, the only thing left is I<=(n+1)
        let input_size = hyp.input_alphabet().len();
        let mut input_alphabet: Vec<_> = (0..input_size)
            .into_iter()
            .map(|x| x as u16)
            .map(InputSymbol::from)
            .collect_vec();
        input_alphabet.shuffle(&mut self.rng);
        let lookahead_range = (0..=self.lookahead + 1).into_iter().collect_vec();
        let infix_closure = || {
            Iterator::flatten(lookahead_range.iter().map(|&n| {
                itertools::repeat_n(input_alphabet.iter().copied(), n as _)
                    .multi_cartesian_product()
            }))
        };
        for input_seq in infix_closure() {
            if let Some(x) = self.run_test(hyp, &input_seq) {
                return Some(x);
            }
        }
        None
    }

    /// Run a single test sequence and return whether it is a CE or not.
    #[inline]
    #[must_use]
Bharat Garhewal's avatar
Bharat Garhewal committed
    fn run_test(&mut self, hyp: &Mealy, input_seq: &[InputSymbol]) -> CounterExample {
        let hyp_output = hyp.trace(input_seq).1.to_vec();
        let sut_output = RefCell::borrow_mut(&self.oq_oracle).output_query(input_seq);
        if hyp_output == sut_output {
            return None;
        }
Bharat Garhewal's avatar
Bharat Garhewal committed
        Some((input_seq.to_vec(), sut_output))
    }

    /// Compute the access sequences for the states
    /// of the hypothesis.
    #[must_use]
    fn construct_access_map(
        &self,
        states: impl IntoIterator<Item = State>,
    ) -> HashMap<State, Vec<InputSymbol>> {
        let temp = RefCell::borrow(&self.oq_oracle);
        let tree = temp.borrow_tree();
        states
            .into_iter()
            .map(|s| (s, tree.get_access_seq(s)))
            .collect()
    }
}