Commit 6d8bbf59 authored by Bharat Garhewal's avatar Bharat Garhewal
Browse files

Restore original IADS impl and CLI update

parent 19e3f838
Pipeline #60264 passed with stages
in 3 minutes and 7 seconds
......@@ -35,6 +35,7 @@ pub struct Options {
pub oracle_choice: EqOracle,
pub seed: u64,
pub extra_states: usize,
// pub expected_rnd_length: usize,
pub use_ly_ads: bool,
}
......
......@@ -61,6 +61,11 @@ fn main() -> Result<(), Box<dyn std::error::Error>> {
.expect("Extra states must be a valid unsigned integer.")
});
let _rnd_infix_len: usize = matches.value_of("expected_infix_length").map_or(0, |x| {
x.parse()
.expect("Expected infix length must be a valid unsigned integer.")
});
let seed: u64 = matches
.value_of("seed")
.map_or(0, |s| s.parse::<u64>().unwrap_or_default());
......
......@@ -84,11 +84,12 @@ where
}
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);
let access_map = self.access_map(hyp);
// let access_map = random_access_map(hyp, self.seed);
let rig = RandomInfixGenerator::new(self.seed, hyp.input_alphabet().len(), lookahead);
log::info!("Running AIC sequences.");
let splitting_tree = TreeCons::construct(hyp, &hyp_states.into_iter().collect_vec(), false);
let splitting_tree =
TreeCons::construct(hyp, &hyp_states.iter().copied().collect_vec(), false);
log::info!("Finished making ST-IADS.");
let mut rng = StdRng::seed_from_u64(self.seed);
let access_vec = access_map.into_values().collect_vec();
......@@ -99,7 +100,8 @@ 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);
// 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);
self.seed = rng.gen::<u64>();
......@@ -162,52 +164,28 @@ where
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();
let states_to_sep = self.must_sep_from(prefix, hyp);
log::debug!("States to separate: {:?}", &states_to_sep);
match &states_to_sep[..] {
[] => {
unreachable!("Cannot reach here");
unreachable!("A state cannot be distinguished from itself!");
}
// Already separated from everything, no need to run any test.
[_q] => None,
[_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
}
[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)
})
.expect("Safe")
.0;
let test_input = toolbox::concat_slices(&[prefix, &sep_word]);
self.run_test(hyp, &test_input)
......@@ -217,10 +195,9 @@ where
// 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, 0));
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);
......@@ -230,77 +207,175 @@ where
}
}
fn must_sep_from(
&mut self,
access: &[InputSymbol],
infix: &[InputSymbol],
hyp: &Mealy,
) -> Vec<State> {
/// 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> {
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();
}
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,
};
// Once we have the basis state, we have to walk along the infix until
// we reach a frontier state.
let num_inputs_till_frontier = self.num_inputs_for_frontier(access, infix, hyp);
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()
let are_not_sep = |s1: &State| !states_are_apart(tree, *s1, ts);
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 {
......@@ -334,21 +409,22 @@ where
Some((input_seq.to_vec(), sut_output.to_vec()))
}
#[allow(unused)]
fn num_inputs_for_frontier(
&self,
access: &[InputSymbol],
infix: &[InputSymbol],
hyp: &Mealy,
) -> usize {
) -> Option<usize> {
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)) {
return cnt;
return Some(cnt);
}
curr = hyp.step_from(curr, input).0;
}
0
None
// unreachable!("We should hit a frontier state from the basis states!");
}
......@@ -378,6 +454,7 @@ where
}
}
#[allow(unused)]
fn get_successors(fsm: &Mealy, input: InputSymbol, block: &FxHashSet<State>) -> FxHashSet<State> {
block
.par_iter()
......@@ -497,7 +574,7 @@ mod infix_generator {
fn next(&mut self) -> Option<Self::Item> {
let lookahead = self.geo.sample(&mut self.rng) as usize;
let lookahead = lookahead + self.k_min;
// let lookahead = lookahead + self.k_min;
let input_seq: Vec<_> = self
.inputs_dist
.map(InputSymbol::from)
......
......@@ -214,7 +214,7 @@ impl AdaptiveDistinguishingSequence for AdsTree {
}
fn reset_to_root(&mut self) {
self.curr_idx = 0;
self.curr_idx = self.initial_idx;
}
}
......
......@@ -56,15 +56,23 @@ pub fn parse() -> Result<clap::ArgMatches, Box<dyn std::error::Error>> {
)
.arg(
Arg::new("extra_states")
.short('l')
.short('k')
.long("extra_states")
.value_name("ES")
.takes_value(true)
.multiple_occurrences(false),
)
.arg(
Arg::new("expected_infix_length")
.short('l')
.long("expected_infix_length")
.takes_value(true)
.multiple_occurrences(false)
.multiple_values(false)
)
.arg(
Arg::new("seed")
.short('r')
.short('x')
.long("seed")
.value_name("seed")
.help("Random seed for the H-ADS oracle.")
......
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