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

Merge remote-tracking branch 'refs/remotes/origin/incomplete_ads' into incomplete_ads

parents 2649163c 5b7c08d1
Pipeline #60274 passed with stages
in 3 minutes and 6 seconds
......@@ -103,7 +103,6 @@ where
let access = access_vec.get(st_num).expect("Safe");
// let access = access_vec.choose(&mut rng).expect("Safe");
let prefix = toolbox::concat_slices(&[access, &infix]);
// let ce = self.run_ads_test(&prefix, hyp, &splitting_tree, access, rng.gen());
let ce = self.run_ads_test(&prefix, hyp, &splitting_tree, rng.gen());
if ce.is_some() {
let mut rng: StdRng = SeedableRng::seed_from_u64(self.seed);
......@@ -229,156 +228,6 @@ where
other_states.retain(are_not_sep);
other_states
}
// #[must_use]
// fn run_ads_test(
// &mut self,
// prefix: &[InputSymbol],
// hyp: &Mealy,
// splitting_tree: &SplittingTree,
// access: &[InputSymbol],
// seed: u64,
// ) -> CounterExample {
// let hyp_dest = hyp.trace(prefix).0;
// // State hyp_dest must be separated from the following states.
// let access_idx = {
// let ret = access.len();
// if ret == 0 {
// ret
// } else {
// ret - 1
// }
// };
// let states_to_sep = self
// .must_sep_from(access, &prefix[access_idx..], hyp)
// .into_iter()
// .chain(std::iter::once(hyp_dest))
// .dedup()
// .collect_vec();
// let states_to_sep = {
// let temp = RefCell::borrow(&self.oq_oracle);
// let o_tree = temp.borrow_tree();
// if let Some(tree_dest) = o_tree.get_succ(State::new(0), prefix) {
// states_to_sep
// .into_par_iter()
// .filter(|hs| !states_are_apart(o_tree, tree_dest, *hs))
// .collect()
// } else {
// states_to_sep
// }
// };
// let states_to_sep = states_to_sep.into_iter().dedup().collect_vec();
// log::debug!("States to separate: {:?}", &states_to_sep);
// match &states_to_sep[..] {
// [] => {
// unreachable!("Cannot reach here");
// }
// // Already separated from everything, no need to run any test.
// [_q] => None,
// [q, q_p] => {
// // We need to split "q" from "q'", so we just run an output query.
// // let q = hyp_dest;
// let sep_word = shortest_separating_sequence(hyp, hyp, *q, *q_p)
// .unwrap_or_else(|| {
// panic!("Could not separate {:?} and {:?} in the hypothesis", q, q_p)
// })
// .0;
// let test_input = toolbox::concat_slices(&[prefix, &sep_word]);
// self.run_test(hyp, &test_input)
// }
// _ => {
// // 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);
// log::debug!("IADS:{:?}", &st_ads);
// let ce = RefCell::borrow_mut(&self.oq_oracle).ads_equiv_test(st_ads, prefix, hyp);
// st_ads.reset_to_root();
// ce
// }
// }
// }
// fn must_sep_from(
// &mut self,
// access: &[InputSymbol],
// infix: &[InputSymbol],
// hyp: &Mealy,
// ) -> Vec<State> {
// let temp = RefCell::borrow(&self.oq_oracle);
// let o_tree = temp.borrow_tree();
// let prefix = toolbox::concat_slices(&[access, infix]);
// let hyp_final_dest = hyp.trace(&prefix).0;
// let mut must_sep_from: FxHashSet<_> = hyp
// .states()
// .into_par_iter()
// .filter(|&s| s != hyp_final_dest)
// .collect();
// // We essentially have no guarantee that the state reached by the
// // access sequence exists in the observation tree.
// let basis_state = match o_tree.get_succ(State::new(0), access) {
// Some(x) => x,
// None => {
// for input in infix.iter().copied() {
// must_sep_from = get_successors(hyp, input, &must_sep_from);
// }
// return must_sep_from.into_iter().collect();
// }
// };
// // Once we have the basis state, we have to walk along the infix until
// // we reach a frontier state.
// let num_inputs_till_frontier = match self.num_inputs_for_frontier(access, infix, hyp) {
// Some(x) => x,
// None => return vec![],
// };
// let mut infix_iter = infix.iter().copied();
// // We must then make that many steps from the infix and then one more, so that
// // we exit the frontier.
// let mut tree_curr = basis_state;
// for input in infix_iter.by_ref().take(num_inputs_till_frontier + 1) {
// if let Some(tree_dest) = o_tree.get_succ(tree_curr, &[input]) {
// tree_curr = tree_dest;
// must_sep_from = get_successors(hyp, input, &must_sep_from);
// } else {
// // If at any point the successor is undefined, we must return the full
// // set.
// return must_sep_from.into_iter().collect();
// }
// }
// // tree_curr is now outside the frontier, which means that we can start paring down the
// // set of states we need to separate from, assuming that the transitions are actually
// // defined in the observation tree.
// // We need not actually maintain the original set we need to separate from,
// // for even if the transition at a later point is undefined, the preceding
// // transitions ensured that we did not remove useful states, since the ones
// // removed were already separate.
// for input in infix_iter.by_ref() {
// // First, check if we can remove some states.
// let sep_here: FxHashSet<_> = must_sep_from
// .par_iter()
// .copied()
// .filter(|&hs| !tree_and_hyp_states_apart(o_tree, tree_curr, hs, hyp))
// .collect();
// must_sep_from.retain(|s| !sep_here.contains(s));
// if let Some(tree_dest) = o_tree.get_succ(tree_curr, &[input]) {
// tree_curr = tree_dest;
// must_sep_from = get_successors(hyp, input, &must_sep_from);
// } else {
// break;
// }
// }
// for input in infix_iter.by_ref() {
// must_sep_from = get_successors(hyp, input, &must_sep_from);
// }
// must_sep_from.into_iter().collect()
// }
/// Specialised case for when the hypothesis is a single-state FSM.
#[must_use]
fn find_counterexample_initial(&mut self, hyp: &Mealy) -> CounterExample {
......
......@@ -8,5 +8,6 @@ pub mod cli;
pub(crate) mod data_structs;
pub mod learning_config;
pub mod parsers;
pub mod sequences;
pub mod toolbox;
pub mod writers;
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