Newer
Older
use super::equivalence_trait::{CounterExample, EquivalenceOracle, InternalEquivalenceOracle};
use crate::{
automatadefs::{
mealy::{InputSymbol, Mealy, State},
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,
{
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()
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
150
151
152
153
154
155
.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(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]
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;
}
}
/// 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()
}
}