sep_seq.rs 6.79 KB
Newer Older
1
2
3
use super::equivalence_trait::{CounterExample, EquivalenceOracle, InternalEquivalenceOracle};
use crate::{
    automatadefs::{
4
        mealy::{InputSymbol, Mealy, State},
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
5
        traits::{FiniteStateMachine, ObservationTree},
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
    },
    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,
{
45
    type Options = ();
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
    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();
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
62
        let mut input_alphabet = toolbox::inputs_iterator(input_size).collect_vec();
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
        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();
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
150
        let mut input_alphabet = toolbox::inputs_iterator(input_size).collect_vec();
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
        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
Cleanup    
Bharat Garhewal committed
170
    fn run_test(&mut self, hyp: &Mealy, input_seq: &[InputSymbol]) -> CounterExample {
171
172
173
174
175
        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
Cleanup    
Bharat Garhewal committed
176
        Some((input_seq.to_vec(), sut_output))
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
    }

    /// 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()
    }
}