iads.rs 13.4 KB
Newer Older
1
use super::{impl_ads::AdsTree, tree::SplittingTree};
Bharat's avatar
Bharat committed
2
use crate::{
3
    ads::traits::AdaptiveDistinguishingSequence,
Bharat's avatar
Bharat committed
4
    automatadefs::{
Bharat's avatar
Bharat committed
5
6
        mealy::{InputSymbol, Mealy, State},
        traits::{FiniteStateMachine, ObservationTree},
Bharat's avatar
Bharat committed
7
    },
8
    learner::apartness::states_are_apart,
Bharat's avatar
Bharat committed
9
    oracles::{
10
11
12
        equivalence::{
            automata::shortest_separating_sequence,
            equivalence_trait::{CounterExample, EquivalenceOracle, InternalEquivalenceOracle},
13
            incomplete::tree::TreeCons,
Bharat's avatar
Bharat committed
14
15
16
        },
        membership::Oracle as OQOracle,
    },
17
18
19
20
    util::{
        sequences::{FixedInfixGenerator, Order, RandomInfixGenerator},
        toolbox,
    },
Bharat's avatar
Bharat committed
21
};
22
use fnv::{FnvHashMap, FnvHashSet};
Bharat's avatar
Bharat committed
23
use itertools::Itertools;
24
25
26
27
use rand::{
    prelude::{SliceRandom, StdRng},
    Rng, SeedableRng,
};
28
use rand_distr::{Distribution, Uniform};
29
30
use rayon::iter::{IntoParallelIterator, IntoParallelRefIterator, ParallelIterator};
use rustc_hash::{FxHashMap, FxHashSet};
31
32
33
34
use std::{
    cell::RefCell,
    collections::{BTreeSet, VecDeque},
    rc::Rc,
35
    time::Instant,
36
};
Bharat's avatar
Bharat committed
37

Bharat's avatar
Bharat committed
38
39
40
pub struct IadsEO<'a, T> {
    oq_oracle: Rc<RefCell<OQOracle<'a, T>>>,
    lookahead: usize,
41
    seed: u64,
42
    ads_map: FnvHashMap<BTreeSet<State>, AdsTree>,
43
44
45
    frontier_states: FnvHashMap<State, Vec<State>>, // frontier -> basis
    // transitions from the basis using an input that goes to the frontier
    frontier_trans: FnvHashSet<(State, InputSymbol)>,
Bharat's avatar
Bharat committed
46
47
}

Bharat's avatar
Bharat committed
48
49
50
51
52
impl<'a, T> InternalEquivalenceOracle<'a, T> for IadsEO<'a, T>
where
    T: ObservationTree + Sync + Send,
{
    fn new(oq_oracle: Rc<RefCell<OQOracle<'a, T>>>, lookahead: usize, seed: u64) -> Self {
Bharat Garhewal's avatar
Bharat Garhewal committed
53
        Self {
Bharat's avatar
Bharat committed
54
55
            oq_oracle,
            lookahead,
56
            seed,
57
            ads_map: Default::default(),
58
59
            frontier_states: Default::default(),
            frontier_trans: Default::default(),
Bharat Garhewal's avatar
Bharat Garhewal committed
60
61
        }
    }
Bharat's avatar
Bharat committed
62
}
Bharat Garhewal's avatar
Bharat Garhewal committed
63

Bharat's avatar
Bharat committed
64
65
66
67
68
69
70
71
impl<'a, T> EquivalenceOracle<'a, T> for IadsEO<'a, T>
where
    T: ObservationTree + Send + Sync,
{
    type Options = ();

    fn get_counts(&mut self) -> (usize, usize) {
        RefCell::borrow_mut(&self.oq_oracle).get_counts()
Bharat's avatar
Bharat committed
72
73
    }

Bharat's avatar
Bharat committed
74
75
76
    fn find_counterexample(&mut self, hypothesis: &Mealy) -> CounterExample {
        self.find_counterexample_with_lookahead(hypothesis, self.lookahead)
    }
Bharat's avatar
Bharat committed
77

Bharat's avatar
Bharat committed
78
79
    fn find_counterexample_with_lookahead(
        &mut self,
Bharat Garhewal's avatar
Bharat Garhewal committed
80
        hyp: &Mealy,
Bharat's avatar
Bharat committed
81
82
        lookahead: usize,
    ) -> CounterExample {
Bharat Garhewal's avatar
Bharat Garhewal committed
83
        let hyp_states = hyp.states();
84
        let num_states = hyp_states.len();
85
        if num_states == 1 {
Bharat Garhewal's avatar
Bharat Garhewal committed
86
            return self.find_counterexample_initial(hyp);
87
        }
88
        self.ads_map.clear();
89
        self.frontier_trans = self.frontier_transitions(hyp);
90
91
        let access_map = self.access_map(hyp);
        // let access_map = random_access_map(hyp, self.seed);
92
        let rig = RandomInfixGenerator::new(self.seed, hyp.input_alphabet().len(), 0, lookahead);
Bharat's avatar
Bharat committed
93
        log::info!("Running AIC sequences.");
94
95
        let splitting_tree =
            TreeCons::construct(hyp, &hyp_states.iter().copied().collect_vec(), false);
96
        log::info!("Finished making ST-IADS.");
97
98
        let mut rng = StdRng::seed_from_u64(self.seed);
        let access_vec = access_map.into_values().collect_vec();
99
100

        let mut time_now = Instant::now();
101
        for (cnt, infix) in rig.generate().enumerate() {
102
103
104
            let st_num = rng.gen_range(0..num_states);
            let access = access_vec.get(st_num).expect("Safe");
            // let access = access_vec.choose(&mut rng).expect("Safe");
105
            let prefix = toolbox::concat_slices(&[access, &infix]);
106
            let ce = self.run_ads_test(&prefix, hyp, &splitting_tree, rng.gen());
107
108
109
110
111
            if ce.is_some() {
                let mut rng: StdRng = SeedableRng::seed_from_u64(self.seed);
                self.seed = rng.gen::<u64>();
                return ce;
            }
112
113
114
115
            if cnt % 10000 == 0 {
                let time_spent = time_now.elapsed();
                time_now = Instant::now();
                println!("Spent : {} ms", time_spent.as_millis());
116
            }
Bharat's avatar
Bharat committed
117
        }
118
        unreachable!("This process never ends until a CE is found.");
Bharat's avatar
Bharat committed
119
    }
Bharat's avatar
Bharat committed
120
}
Bharat's avatar
Bharat committed
121

122
123
/// Checks whether the hypothesis and the observation tree agree after a given prefix.
#[must_use]
124
fn _check_consistency_from<T: ObservationTree + Sync>(
125
126
127
128
129
130
    prefix: &[InputSymbol],
    o_tree: &T,
    hypothesis: &Mealy,
) -> CounterExample {
    let tree_start = o_tree.get_succ(State::new(0), prefix).expect("Safe");
    let hyp_start = hypothesis.trace(prefix).0;
Bharat's avatar
Bharat committed
131
132
133
    let input_size = hypothesis.input_alphabet().len();
    // let tree_start = State::new(0);
    // let hyp_start = State::new(0);
134
135
    let mut queue = VecDeque::from([(tree_start, hyp_start)]);
    while let Some((q, r)) = queue.pop_front() {
Bharat's avatar
Bharat committed
136
137
138
139
140
        for i in toolbox::inputs_iterator(input_size) {
            let tree_hyp_next_pair = o_tree
                .get_out_succ(q, i)
                .zip(Some(hypothesis.step_from(r, i)));
            if let Some(((out_t, dest_t), (dest_h, out_h))) = tree_hyp_next_pair {
141
                if out_h == out_t {
Bharat's avatar
Bharat committed
142
                    queue.push_back((dest_t, dest_h));
143
                } else {
Bharat's avatar
Bharat committed
144
145
146
147
                    let mut inputs = o_tree.get_access_seq(q);
                    inputs.push(i);
                    let outputs = o_tree.get_observation(None, &inputs).expect("Safe");
                    return Some((inputs, outputs));
148
                }
Bharat's avatar
Bharat committed
149
            }
150
151
152
153
154
        }
    }
    None
}

Bharat's avatar
Bharat committed
155
156
157
158
impl<'a, T> IadsEO<'a, T>
where
    T: ObservationTree + Send + Sync,
{
159
160
161
162
    pub fn load_frontier_states(&mut self, frontier: FnvHashMap<State, Vec<State>>) {
        self.frontier_states = frontier;
    }

163
    #[must_use]
164
165
166
167
168
    fn run_ads_test(
        &mut self,
        prefix: &[InputSymbol],
        hyp: &Mealy,
        splitting_tree: &SplittingTree,
169
        seed: u64,
170
    ) -> CounterExample {
171
172
        let hyp_dest = hyp.trace(prefix).0;
        // State hyp_dest must be separated from the following states.
173
        let states_to_sep = self.must_sep_from(prefix, hyp);
174
175
176
        log::debug!("States to separate: {:?}", &states_to_sep);
        match &states_to_sep[..] {
            [] => {
177
                unreachable!("A state cannot be distinguished from itself!");
178
            }
179
            // Already separated from everything, no need to run any test.
180
181
182
183
184
185
            [_q_p] => {
                // let temp = RefCell::borrow(&self.oq_oracle);
                // let o_tree = temp.borrow_tree();
                // assert!(_check_consistency_from(&[], o_tree, hyp).is_none());
                None
            }
186
            [q, q_p] => {
187
                // We need to split "q" from "q'", so we just run an output query.
188
189
                // let q = hyp_dest;
                let sep_word = shortest_separating_sequence(hyp, hyp, *q, *q_p)
190
                    .expect("Safe")
191
192
                    .0;
                let test_input = toolbox::concat_slices(&[prefix, &sep_word]);
193
                self.run_test(hyp, &test_input)
194
195
196
197
            }
            _ => {
                // There are at least three states (in total) we need to split,
                // so it makes sense to use an IADS now.
198
                // states_to_sep.push(hyp_dest);
199
                let states = states_to_sep.iter().copied().collect();
200
201
202
                let st_ads = self.ads_map.entry(states).or_insert_with(|| {
                    AdsTree::construct(hyp, splitting_tree, &states_to_sep, seed)
                });
203
                st_ads.randomise_root(hyp_dest);
204
                log::debug!("IADS:{:?}", &st_ads);
205
206
207
                let ce = RefCell::borrow_mut(&self.oq_oracle).ads_equiv_test(st_ads, prefix, hyp);
                st_ads.reset_to_root();
                ce
208
209
210
211
            }
        }
    }

212
213
214
    /// Returns the states which `tree_state` is not separated from in the observation tree.
    #[must_use]
    fn must_sep_from(&self, prefix: &[InputSymbol], hyp: &Mealy) -> Vec<State> {
Bharat's avatar
Bharat committed
215
        let temp = RefCell::borrow(&self.oq_oracle);
216
217
218
219
220
221
222
223
224
225
        let tree = temp.borrow_tree();
        let tree_dest = tree.get_succ(State::new(0), prefix);
        // let hyp_dest = hyp.trace_from(State::new(0), prefix).0;
        let mut other_states = hyp.states().into_iter().collect();
        // .into_par_iter()
        // .filter(|&s| s != hyp_dest)
        // .collect();
        let ts = match tree_dest {
            Some(ts) => ts,
            None => return other_states,
226
        };
227
228
229
        let are_not_sep = |s1: &State| !states_are_apart(tree, *s1, ts);
        other_states.retain(are_not_sep);
        other_states
Bharat Garhewal's avatar
Bharat Garhewal committed
230
    }
Bharat's avatar
Bharat committed
231
232
233
234
235
236
237
238
239
    /// 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)
240
241
242
243
244
245
246
247
248
        let input_alphabet = hyp.input_alphabet().into_iter().sorted().collect_vec();
        let fig = FixedInfixGenerator::new(input_alphabet, self.lookahead + 1, Order::ASC);
        for seq in fig.generate() {
            let res = self.run_test(hyp, &seq);
            if res.is_some() {
                return res;
            }
        }
        None
Bharat's avatar
Bharat committed
249
    }
Bharat's avatar
Bharat committed
250

Bharat's avatar
Bharat committed
251
252
253
254
255
256
257
258
259
260
261
    /// Run a single test sequence and return whether it is a CE or not.
    #[inline]
    #[must_use]
    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;
        }
        Some((input_seq.to_vec(), sut_output.to_vec()))
    }
262

263
    #[allow(unused)]
264
    fn num_inputs_for_frontier(
Bharat's avatar
Bharat committed
265
        &self,
266
267
268
        access: &[InputSymbol],
        infix: &[InputSymbol],
        hyp: &Mealy,
269
    ) -> Option<usize> {
270
271
272
273
        let mut curr = hyp.trace(access).0;
        for (cnt, input) in infix.iter().copied().enumerate() {
            let cnt = cnt + 1;
            if self.frontier_trans.contains(&(curr, input)) {
274
                return Some(cnt);
275
276
277
            }
            curr = hyp.step_from(curr, input).0;
        }
278
        None
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
        // unreachable!("We should hit a frontier state from the basis states!");
    }

    /// Given a hypothesis and the frontier-basis map, we compute the transitions
    /// that would lead to a frontier state.
    fn frontier_transitions(&mut self, hyp: &Mealy) -> FnvHashSet<(State, InputSymbol)> {
        let temp = RefCell::borrow(&self.oq_oracle);
        let o_tree = temp.borrow_tree();
        hyp.states()
            .into_iter()
            .cartesian_product(hyp.input_alphabet().into_iter())
            .filter(|(s, i)| {
                let dest = o_tree.get_succ(*s, &[*i]).expect("Safe");
                self.frontier_states.contains_key(&dest)
            })
            .collect()
    }

    #[allow(unused)]
    pub(crate) fn access_map(&self, hyp: &Mealy) -> FxHashMap<State, Vec<InputSymbol>> {
Bharat's avatar
Bharat committed
299
        let temp = RefCell::borrow(&self.oq_oracle);
300
301
302
303
304
        let o_tree = temp.borrow_tree();
        hyp.states()
            .into_par_iter()
            .map(|s| (s, o_tree.get_access_seq(s)))
            .collect()
Bharat Garhewal's avatar
Bharat Garhewal committed
305
    }
306
}
307

308
#[allow(unused)]
309
310
311
312
313
314
315
316
fn get_successors(fsm: &Mealy, input: InputSymbol, block: &FxHashSet<State>) -> FxHashSet<State> {
    block
        .par_iter()
        .copied()
        .map(|s| fsm.step_from(s, input).0)
        .collect()
}

317
318
319
320
/// Randomly compute access sequencs for states in the hypothesis.
///
/// Equivalent to the ``buggy`` mode of H-ADS.
#[must_use]
321
#[allow(dead_code)]
322
323
324
325
326
327
328
329
330
331
332
333
fn random_access_map(fsm: &Mealy, seed: u64) -> FxHashMap<State, Vec<InputSymbol>> {
    let mut ret = FxHashMap::default();
    let mut rng: StdRng = SeedableRng::seed_from_u64(seed);
    let mut work_list = VecDeque::from([State::new(0)]);
    ret.insert(State::new(0), vec![]);
    let uni_dist = Uniform::new_inclusive(0.0, 1.0);
    while !work_list.is_empty() {
        let state = {
            let sample = uni_dist.sample(&mut rng);
            let scaled_sample = {
                let scaled = (work_list.len() as f64 * sample).floor() as usize;
                scaled.clamp(0, work_list.len() - 1)
334
            };
335
336
337
338
339
340
341
342
            work_list.remove(scaled_sample).expect("Safe")
        };
        let mut inputs = fsm.input_alphabet().into_iter().collect_vec();
        inputs.shuffle(&mut rng);
        for i in inputs {
            let dest = fsm.step_from(state, i).0;
            if ret.contains_key(&dest) {
                continue;
343
            }
344
345
346
347
348
349
350
            let dest_acc = {
                let mut x = ret.get(&state).expect("Safe").clone();
                x.push(i);
                x
            };
            work_list.push_back(dest);
            ret.insert(dest, dest_acc);
351
352
        }
    }
353
    ret
Bharat's avatar
Bharat committed
354
}
355

356
357
#[cfg(test)]
mod tests {
358
359
360
    use rstest::rstest;

    use super::random_access_map;
361
    use crate::{
362
        automatadefs::traits::FiniteStateMachine, util::parsers::machine::read_mealy_from_file,
363
    };
364
    use std::collections::HashSet;
365

366
367
368
369
370
371
372
    #[rstest]
    #[case("tests/hypothesis_23.dot")]
    /// Check if all the number of access sequences found is equal to
    /// the number of states of an FSM.
    fn all_states_found(#[case] file_name: &str) {
        let (fsm, _input_map, _) = read_mealy_from_file(file_name);
        let access_states: HashSet<_, _> = random_access_map(&fsm, 10).into_keys().collect();
373
374
375
        assert_eq!(fsm.states(), access_states)
    }
}