Commit 72575064 authored by Bharat Garhewal's avatar Bharat Garhewal
Browse files

IADS no longer cached, amount tried to optimise constr. alg. of IADS from ST-IADS

parent d6d8cd32
Pipeline #60280 passed with stages
in 3 minutes and 11 seconds
......@@ -28,18 +28,12 @@ use rand::{
use rand_distr::{Distribution, Uniform};
use rayon::iter::{IntoParallelIterator, IntoParallelRefIterator, ParallelIterator};
use rustc_hash::{FxHashMap, FxHashSet};
use std::{
cell::RefCell,
collections::{BTreeSet, VecDeque},
rc::Rc,
time::Instant,
};
use std::{cell::RefCell, collections::VecDeque, rc::Rc, time::Instant};
pub struct IadsEO<'a, T> {
oq_oracle: Rc<RefCell<OQOracle<'a, T>>>,
lookahead: usize,
seed: u64,
ads_map: FnvHashMap<BTreeSet<State>, AdsTree>,
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)>,
......@@ -54,7 +48,6 @@ where
oq_oracle,
lookahead,
seed,
ads_map: Default::default(),
frontier_states: Default::default(),
frontier_trans: Default::default(),
}
......@@ -85,7 +78,6 @@ where
if num_states == 1 {
return self.find_counterexample_initial(hyp);
}
self.ads_map.clear();
self.frontier_trans = self.frontier_transitions(hyp);
let access_map = self.access_map(hyp);
// let access_map = random_access_map(hyp, self.seed);
......@@ -129,8 +121,6 @@ fn _check_consistency_from<T: ObservationTree + Sync>(
let tree_start = o_tree.get_succ(State::new(0), prefix).expect("Safe");
let hyp_start = hypothesis.trace(prefix).0;
let input_size = hypothesis.input_alphabet().len();
// let tree_start = State::new(0);
// let hyp_start = State::new(0);
let mut queue = VecDeque::from([(tree_start, hyp_start)]);
while let Some((q, r)) = queue.pop_front() {
for i in toolbox::inputs_iterator(input_size) {
......@@ -195,14 +185,16 @@ where
_ => {
// There are at least three states (in total) we need to split,
// so it makes sense to use an IADS now.
// states_to_sep.push(hyp_dest);
let states = states_to_sep.iter().copied().collect();
let st_ads = self.ads_map.entry(states).or_insert_with(|| {
AdsTree::construct(hyp, splitting_tree, &states_to_sep, seed)
});
st_ads.randomise_root(hyp_dest);
let mut st_ads = AdsTree::construct(hyp, splitting_tree, &states_to_sep, seed);
let other_states = states_to_sep
.iter()
.copied()
.filter(|&x| x != hyp_dest)
.collect_vec();
st_ads.randomise_root(hyp_dest, &other_states);
log::debug!("IADS:{:?}", &st_ads);
let ce = RefCell::borrow_mut(&self.oq_oracle).ads_equiv_test(st_ads, prefix, hyp);
let ce =
RefCell::borrow_mut(&self.oq_oracle).ads_equiv_test(&mut st_ads, prefix, hyp);
st_ads.reset_to_root();
ce
}
......@@ -214,12 +206,12 @@ where
fn must_sep_from(&self, prefix: &[InputSymbol], hyp: &Mealy) -> Vec<State> {
let temp = RefCell::borrow(&self.oq_oracle);
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();
if tree_dest == Some(State::new(6000)) {
let _x = "";
}
let ts = match tree_dest {
Some(ts) => ts,
None => return other_states,
......@@ -228,6 +220,7 @@ where
other_states.retain(are_not_sep);
other_states
}
/// Specialised case for when the hypothesis is a single-state FSM.
#[must_use]
fn find_counterexample_initial(&mut self, hyp: &Mealy) -> CounterExample {
......@@ -237,7 +230,7 @@ where
// 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_alphabet = hyp.input_alphabet().into_iter().sorted().collect_vec();
let input_alphabet = hyp.input_alphabet();
let fig = FixedInfixGenerator::new(input_alphabet, self.lookahead + 1, Order::ASC);
for seq in fig.generate() {
let res = self.run_test(hyp, &seq);
......
......@@ -13,7 +13,7 @@ use rand::{
Rng, SeedableRng,
};
use rayon::iter::{IntoParallelIterator, ParallelIterator};
use rustc_hash::FxHashMap;
use rustc_hash::{FxHashMap, FxHashSet};
use std::collections::VecDeque;
#[derive(Debug, Default, Clone, PartialEq)]
......@@ -90,8 +90,8 @@ impl AdsTree {
}
fn _construct(&mut self, splitting_tree: &SplittingTree, fsm: &Mealy, initial_label: &[State]) {
let init_root = splitting_tree.get_lca(initial_label);
let all_states = splitting_tree.arena[init_root.to_index()].val.label.clone();
// let init_root = splitting_tree.get_lca(initial_label);
let all_states = initial_label.to_vec(); // splitting_tree.arena[init_root.to_index()].val.label.clone();
let mut undistinguished = VecDeque::from([all_states]);
while let Some(s_prime) = undistinguished.pop_front() {
let curr_root_idx = self.tree.node(AdsNode::from_block(s_prime.into_iter()));
......@@ -174,9 +174,17 @@ impl AdsTree {
&mut self.tree.arena[x].val
}
pub(crate) fn randomise_root(&mut self, must_have: State) {
pub(crate) fn randomise_root(&mut self, must_have: State, should_have: &[State]) {
let should_have: FxHashSet<_> = should_have.iter().copied().collect();
let roots: Vec<_> = rayon::iter::IntoParallelRefIterator::par_iter(&self.roots)
.filter(|&&idx| self.tree.ref_at(idx).initial.contains(&must_have))
.filter(|&&idx| {
self.tree
.ref_at(idx)
.initial
.iter()
.any(|x| should_have.contains(x))
})
.copied()
.collect();
let mut rng = StdRng::seed_from_u64(self.seed);
......
......@@ -265,8 +265,6 @@ where
match ads_res {
Ok((ads_inputs, ads_outputs)) => {
println!("Tree had a reply, duplicate query!");
// assert!(self.check_consistency(fsm).is_none());
// println!("ADS: {:#?}", ads);
let mut input_seq = Vec::from(prefix);
input_seq.extend(ads_inputs.iter());
let mut output_seq = tree_prefix_out;
......@@ -283,7 +281,6 @@ where
self.sul.reset();
let prefix_out = self.sul.step(prefix);
let (mut hyp_curr, hyp_out) = fsm.trace(prefix);
let hyp_prefix_state = hyp_curr;
if prefix_out != hyp_out {
log::info!("Found CE in the random prefix.");
return Some((prefix.to_vec(), prefix_out.to_vec()));
......@@ -310,14 +307,6 @@ where
}
Err(ads_err) => match ads_err {
AdsStatus::Done => {
// if !ads
// .tree
// .ref_at(ads.curr_idx)
// .initial
// .contains(&hyp_prefix_state)
// {
// panic!("Probably not the state we wanted!");
// }
self.add_observation(&inputs_sent, &outputs_received);
return None;
}
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment