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

More refactoring

parent 9ae7d681
Pipeline #60695 passed with stages
in 6 minutes and 16 seconds
use super::FiniteStateMachine;
use crate::oracles::equivalence::CounterExample;
use fnv::{FnvHashMap, FnvHashSet};
use rayon::prelude::*;
use serde::{Deserialize, Serialize};
use std::collections::VecDeque;
use std::fmt;
/// Newtype for an input symbol: wraps a u16.
......@@ -214,3 +216,60 @@ mod tests {
assert!(load_basic_fsm().is_complete());
}
}
/// Find the shortest separating sequence between `reference` and `other`.
///
/// If an initial state is `None`, we take the actual initial state of the machine.
/// If an initial state is `State(x)`, we use it as initial.
pub fn shortest_separating_sequence<M: FiniteStateMachine, St: Into<Option<State>>>(
reference: &M,
other: &M,
ref_initial: St,
other_initial: St,
) -> CounterExample {
let ref_initial_state = ref_initial
.into()
.unwrap_or_else(|| reference.initial_state());
let hyp_initial_state = other_initial
.into()
.unwrap_or_else(|| other.initial_state());
let initial_pair = (ref_initial_state, hyp_initial_state, Vec::new());
let input_alphabet = reference.input_alphabet();
let mut visited_pairs = FnvHashSet::default();
let mut work_list = VecDeque::from([initial_pair]);
while !work_list.is_empty() {
let (ref_state, hyp_state, access_seq) = work_list.pop_front().expect("Safe");
for i in input_alphabet.iter().copied() {
let (ref_dest, ref_out) = reference.step_from(ref_state, i);
let (hyp_dest, hyp_out) = other.step_from(hyp_state, i);
// If the outputs do not match, we have our CE.
// Return the current access seq + the input symbol
// Also the expected (i.e., reference) output.
if ref_out != hyp_out {
let mut input_seq = Vec::with_capacity(access_seq.len() + 1);
input_seq.extend_from_slice(&access_seq);
input_seq.push(i);
let (_, output_seq) = reference.trace(&input_seq);
return Some((input_seq, output_seq.to_vec()));
}
// If the outputs match, add the destination pairs,
// unless we've seen the destination pairs already or
// the dest. pair is the current pair (aka a loop).
if !visited_pairs.contains(&(ref_dest, hyp_dest))
&& (ref_dest, hyp_dest) != (ref_state, hyp_state)
{
let mut new_access_seq = Vec::with_capacity(access_seq.len() + 1);
new_access_seq.extend_from_slice(&access_seq);
new_access_seq.push(i);
work_list.push_back((ref_dest, hyp_dest, new_access_seq));
}
visited_pairs.insert((ref_state, hyp_state));
}
}
None
}
use super::obs_tree::ObservationTree;
use crate::oracles::equivalence::CounterExample;
use crate::{
ads::{
lee_yannakakis::adaptive_distinguishing_seq::AdsTree as LyAds,
......@@ -9,7 +10,7 @@ use crate::{
FiniteStateMachine,
},
learner::apartness::{compute_witness, states_are_apart},
oracles::{equivalence::equivalence_trait::CounterExample, membership::Oracle as OutputOracle},
oracles::membership::Oracle as OutputOracle,
util::{parsers::logs::Logs, toolbox},
};
use itertools::Itertools;
......@@ -440,3 +441,23 @@ fn get_ce_prefix_idx(ce_output: &[OutputSymbol], hyp_output: &[OutputSymbol]) ->
}
unreachable!();
}
/// Options for application of rule 2 of the L# algorithm.
#[derive(PartialEq, Eq, Clone, Debug)]
pub enum Rule2 {
/// Identify the new frontier state using an ADS (*default*).
Ads,
/// Basic version, do not attempt to identify the new frontier state.
Nothing,
/// Identify the new frontier state using a (randomly selected) witness for two basis states.
SepSeq,
}
/// Options for application of rule 3 of the L# algorithm.
#[derive(PartialEq, Eq, Clone, Debug)]
pub enum Rule3 {
/// Identify frontier states using an ADS (*default*).
Ads,
/// Identify frontier states using a (randomly selected) witness for two basis states.
SepSeq,
}
use crate::automatadefs::mealy::shortest_separating_sequence;
use crate::learner::l_sharp::{Rule2, Rule3};
use crate::oracles::equivalence::{
EquivalenceOracle, ExternalEquivalenceOracle, InternalEquivalenceOracle,
};
use crate::{
automatadefs::{
mealy::{InputSymbol, Mealy, OutputSymbol},
......@@ -6,10 +11,6 @@ use crate::{
learner::{l_sharp::Lsharp, obs_tree::map_tree::ObsTree as ObsMapTree},
oracles::{
equivalence::{
bfs::Bfs,
equivalence_trait::{
EquivalenceOracle, ExternalEquivalenceOracle, InternalEquivalenceOracle,
},
hads_tree::HadsTree,
incomplete::iads::IadsEO,
sep_seq::SequenceOracle,
......@@ -19,7 +20,7 @@ use crate::{
},
sul::simulator::Simulator,
util::{
learning_config::{EqOracle, LearnResult, Rule2, Rule3},
learning_config::{EqOracle, LearnResult},
writers::overall as MealyWriter,
},
};
......@@ -64,7 +65,6 @@ pub fn learn_fsm(
let rev_output_map: FnvHashMap<_, _> =
output_map.iter().map(|(x, y)| (*y, x.clone())).collect();
let mut rng = StdRng::seed_from_u64(options.seed);
let perfect_oracle = Bfs::new(sul);
let mut hads_oracle_tree = HadsTree::new(
Rc::clone(&oq_oracle),
(),
......@@ -73,17 +73,7 @@ pub fn learn_fsm(
rev_input_map.clone(),
rev_output_map.clone(),
);
// let mut hads_sut = Simulator::new(Arc::clone(&mealy_machine));
// let mut hads_oracle = HADS::new(
// &mut hads_sut,
// options
// .extra_states
// .try_into()
// .expect("Extra states cannot be larger than u32!"),
// rng.gen(),
// rev_input_map.clone(),
// rev_output_map.clone(),
// );
let soucha_config = SouchaConfigBuilder::default()
.exec_loc("/Users/bharat/research/FSMlib/fsm_lib")
.lookahead(options.extra_states)
......@@ -137,8 +127,8 @@ pub fn learn_fsm(
.format(MealyWriter::MealyEncoding::Dot)
.build()
.expect("Could not write Hypothesis file.");
MealyWriter::write_machine(writer_config, &hypothesis, &rev_input_map, &rev_output_map);
let ideal_ce = perfect_oracle.find_counterexample(&hypothesis);
MealyWriter::write_machine(&writer_config, &hypothesis, &rev_input_map, &rev_output_map);
let ideal_ce = shortest_separating_sequence(&sul.clone(), &hypothesis, None, None);
if ideal_ce.is_none() {
success = true;
println!("Learning finished!");
......@@ -165,7 +155,7 @@ pub fn learn_fsm(
println!("Testing queries/symbols: {}/{}", t_resets, t_inputs);
word
}
EqOracle::Internal => ideal_ce,
EqOracle::Internal => ideal_ce.clone(),
EqOracle::HadsTree => {
let word = hads_oracle_tree.find_counterexample(&hypothesis);
let (t_inputs, t_resets) = hads_oracle_tree.get_counts();
......@@ -192,8 +182,7 @@ pub fn learn_fsm(
learner.process_cex(ce, &hypothesis);
} else {
println!("No CE found.");
success = EqOracle::Internal == options.oracle_choice
|| None == perfect_oracle.find_counterexample(&hypothesis);
success = ideal_ce.is_none();
println!("Model learned: {}", success);
break;
}
......
......@@ -3,7 +3,7 @@ use crate::{
learner::learning::learn_fsm,
util::{
cli,
learning_config::{EqOracle, Rule2, Rule3},
learning_config::EqOracle,
parsers::{logs::read_logs, machine::read_mealy_from_file},
},
};
......@@ -14,6 +14,7 @@ use log4rs::{
config::{Appender, Config, Root},
encode::pattern::PatternEncoder,
};
use lsharp_ru::learner::l_sharp::{Rule2, Rule3};
use lsharp_ru::learner::learning::OptionsBuilder;
use lsharp_ru::{automatadefs, learner, util};
use rand::{prelude::StdRng, Rng, SeedableRng};
......
use super::equivalence_trait::CounterExample;
use crate::automatadefs::{mealy::State, FiniteStateMachine};
use fnv::FnvHashSet;
use std::collections::VecDeque;
/// Find the shortest separating sequence between `reference` and `other`.
///
/// If an initial state is `None`, we take the actual initial state of the machine.
/// If an initial state is `State(x)`, we use it as initial.
pub fn shortest_separating_sequence<M: FiniteStateMachine, St: Into<Option<State>>>(
reference: &M,
other: &M,
ref_initial: St,
other_initial: St,
) -> CounterExample {
let ref_initial_state = ref_initial
.into()
.unwrap_or_else(|| reference.initial_state());
let hyp_initial_state = other_initial
.into()
.unwrap_or_else(|| other.initial_state());
let initial_pair = (ref_initial_state, hyp_initial_state, Vec::new());
let input_alphabet = reference.input_alphabet();
let mut visited_pairs = FnvHashSet::default();
let mut work_list = VecDeque::from([initial_pair]);
while !work_list.is_empty() {
let (ref_state, hyp_state, access_seq) = work_list.pop_front().expect("Safe");
for i in input_alphabet.iter().copied() {
let (ref_dest, ref_out) = reference.step_from(ref_state, i);
let (hyp_dest, hyp_out) = other.step_from(hyp_state, i);
// If the outputs do not match, we have our CE.
// Return the current access seq + the input symbol
// Also the expected (i.e., reference) output.
if ref_out != hyp_out {
let mut input_seq = Vec::with_capacity(access_seq.len() + 1);
input_seq.extend_from_slice(&access_seq);
input_seq.push(i);
let (_, output_seq) = reference.trace(&input_seq);
return Some((input_seq, output_seq.to_vec()));
}
// If the outputs match, add the destination pairs,
// unless we've seen the destination pairs already or
// the dest. pair is the current pair (aka a loop).
if !visited_pairs.contains(&(ref_dest, hyp_dest))
&& (ref_dest, hyp_dest) != (ref_state, hyp_state)
{
let mut new_access_seq = Vec::with_capacity(access_seq.len() + 1);
new_access_seq.extend_from_slice(&access_seq);
new_access_seq.push(i);
work_list.push_back((ref_dest, hyp_dest, new_access_seq));
}
visited_pairs.insert((ref_state, hyp_state));
}
}
None
}
use super::{automata, equivalence_trait::CounterExample};
use crate::automatadefs::FiniteStateMachine;
/**
Breadth-First Search Equivalence Oracle
The BFS oracle is meant essentially for providing
the shortest separating sequence between the hypothesis and the SUL;
it requires the SUL model to be known.
*/
pub struct Bfs<'a, M> {
reference: &'a M,
}
impl<'a, M> Bfs<'a, M>
where
M: FiniteStateMachine,
{
#[must_use]
pub fn new(reference: &'a M) -> Self {
Self { reference }
}
#[must_use]
pub fn find_counterexample(&self, hypothesis: &M) -> CounterExample {
automata::shortest_separating_sequence(self.reference, hypothesis, None, None)
}
}
use crate::{
automatadefs::mealy::{InputSymbol, Mealy, OutputSymbol},
oracles::membership::Oracle as OQOracle,
};
use fnv::FnvHashMap;
use std::{cell::RefCell, rc::Rc};
/// Counterexample is `Some(...)` if found else `None`.
pub type CounterExample = Option<(Vec<InputSymbol>, Vec<OutputSymbol>)>;
/**
Trait for equivalence oracles.
`Tree` is the type for the Observation Tree, i.e., if a different type of
data structure is used to construct the observation tree, that will work
as well.
*/
pub trait EquivalenceOracle<'a, Tree> {
type Options;
/// Get the number of inputs and resets sent to the SUL, and reset the counters.
#[must_use]
fn get_counts(&mut self) -> (usize, usize);
/// Given a hypothesis, find a CE if possible.
#[must_use = "Do not forget to send the CE for processing."]
fn find_counterexample(&mut self, hypothesis: &Mealy) -> CounterExample;
/// Given a hypothesis, find a CE if possible.
#[must_use = "Do not forget to send the CE for processing."]
fn find_counterexample_with_lookahead(
&mut self,
hypothesis: &Mealy,
lookahead: usize,
) -> CounterExample;
}
/// Trait for "internal" equivalence oracles: must implement [`EquivalenceOracle`].
///
/// An internal equivalence oracle does not need to 'talk' to anything outside
/// the program, and hence lacks the input/output maps for conversion of the
/// alphabet.
pub trait InternalEquivalenceOracle<'a, Tree>: EquivalenceOracle<'a, Tree> {
fn new(
output_oracle: Rc<RefCell<OQOracle<'a, Tree>>>,
lookahead: usize,
random_seed: u64,
) -> Self;
}
/// Trait for "external" equivalence oracles: must implement [`EquivalenceOracle`].
///
/// An external equivalence oracle needs to 'talk' to anything outside
/// the program, and hence has input/output maps for conversion of the
/// alphabet.
pub trait ExternalEquivalenceOracle<'a, Tree>: EquivalenceOracle<'a, Tree> {
fn new(
output_oracle: Rc<RefCell<OQOracle<'a, Tree>>>,
config: <Self as EquivalenceOracle<'a, Tree>>::Options,
lookahead: usize,
random_seed: u64,
rev_input_map: FnvHashMap<InputSymbol, String>,
rev_output_map: FnvHashMap<OutputSymbol, String>,
) -> Self;
fn with_location(
output_oracle: Rc<RefCell<OQOracle<'a, Tree>>>,
config: <Self as EquivalenceOracle<'a, Tree>>::Options,
location: String,
lookahead: usize,
random_seed: u64,
rev_input_map: FnvHashMap<InputSymbol, String>,
rev_output_map: FnvHashMap<OutputSymbol, String>,
) -> Self;
}
use super::equivalence_trait::{CounterExample, EquivalenceOracle, ExternalEquivalenceOracle};
use crate::oracles::equivalence::{CounterExample, EquivalenceOracle, ExternalEquivalenceOracle};
use crate::{
automatadefs::{
mealy::{InputSymbol, Mealy, OutputSymbol},
......@@ -91,7 +91,7 @@ where
.build()
.unwrap();
let byte_hyp = MealyWriter::write_machine(
write_config,
&write_config,
hypothesis,
&self.rev_input_map,
&self.rev_output_map,
......@@ -152,7 +152,7 @@ where
.build()
.unwrap();
let byte_hyp = MealyWriter::write_machine(
write_config,
&write_config,
hypothesis,
&self.rev_input_map,
&self.rev_output_map,
......
use super::{impl_ads::AdsTree, tree::SplittingTree};
use crate::automatadefs::mealy::shortest_separating_sequence;
use crate::oracles::equivalence::{CounterExample, EquivalenceOracle, InternalEquivalenceOracle};
use crate::{
ads::traits::AdaptiveDistinguishingSequence,
automatadefs::{
......@@ -6,13 +8,7 @@ use crate::{
FiniteStateMachine,
},
learner::{apartness::states_are_apart, obs_tree::ObservationTree},
oracles::{
equivalence::{
automata::shortest_separating_sequence,
equivalence_trait::{CounterExample, EquivalenceOracle, InternalEquivalenceOracle},
},
membership::Oracle as OQOracle,
},
oracles::membership::Oracle as OQOracle,
util::{
sequences::{FixedInfixGenerator, Order, RandomInfixGenerator},
toolbox,
......
......@@ -5,14 +5,12 @@
//! 2. Hybrid-ADS, and
//! 3. Separating Sequence.
/// Shortest separating sequence with user-specified initial states.
pub mod automata;
/// Breadth-First Search oracle
pub mod bfs;
/// Trait for equivalence oracles.
pub mod equivalence_trait;
// /// Hybrid-ADS without tree.
// pub mod hads;
use crate::automatadefs::mealy::{InputSymbol, Mealy, OutputSymbol};
use crate::oracles::membership::Oracle as OQOracle;
use fnv::FnvHashMap;
use std::cell::RefCell;
use std::rc::Rc;
/// Hybrid-ADS oracle.
pub mod hads_tree;
/// Soucha IADS algorithm.
......@@ -23,3 +21,69 @@ pub mod sep_seq;
pub mod soucha;
/// Observation Tree ADS oracle.
pub mod tree_ads;
/// Counterexample is `Some(...)` if found else `None`.
pub type CounterExample = Option<(Vec<InputSymbol>, Vec<OutputSymbol>)>;
/// Trait for equivalence oracles.
///
/// `Tree` is the type for the Observation Tree, i.e., if a different type of
/// data structure is used to construct the observation tree, that will work
/// as well.
#[allow(clippy::module_name_repetitions)]
pub trait EquivalenceOracle<'a, Tree> {
type Options;
/// Get the number of inputs and resets sent to the SUL, and reset the counters.
#[must_use]
fn get_counts(&mut self) -> (usize, usize);
/// Given a hypothesis, find a CE if possible.
#[must_use = "Do not forget to send the CE for processing."]
fn find_counterexample(&mut self, hypothesis: &Mealy) -> CounterExample;
/// Given a hypothesis, find a CE if possible.
#[must_use = "Do not forget to send the CE for processing."]
fn find_counterexample_with_lookahead(
&mut self,
hypothesis: &Mealy,
lookahead: usize,
) -> CounterExample;
}
/// Trait for "internal" equivalence oracles: must implement [`EquivalenceOracle`].
///
/// An internal equivalence oracle does not need to 'talk' to anything outside
/// the program, and hence lacks the input/output maps for conversion of the
/// alphabet.
pub trait InternalEquivalenceOracle<'a, Tree>: EquivalenceOracle<'a, Tree> {
fn new(
output_oracle: Rc<RefCell<OQOracle<'a, Tree>>>,
lookahead: usize,
random_seed: u64,
) -> Self;
}
/// Trait for "external" equivalence oracles: must implement [`EquivalenceOracle`].
///
/// An external equivalence oracle needs to 'talk' to anything outside
/// the program, and hence has input/output maps for conversion of the
/// alphabet.
pub trait ExternalEquivalenceOracle<'a, Tree>: EquivalenceOracle<'a, Tree> {
fn new(
output_oracle: Rc<RefCell<OQOracle<'a, Tree>>>,
config: <Self as EquivalenceOracle<'a, Tree>>::Options,
lookahead: usize,
random_seed: u64,
rev_input_map: FnvHashMap<InputSymbol, String>,
rev_output_map: FnvHashMap<OutputSymbol, String>,
) -> Self;
fn with_location(
output_oracle: Rc<RefCell<OQOracle<'a, Tree>>>,
config: <Self as EquivalenceOracle<'a, Tree>>::Options,
location: String,
lookahead: usize,
random_seed: u64,
rev_input_map: FnvHashMap<InputSymbol, String>,
rev_output_map: FnvHashMap<OutputSymbol, String>,
) -> Self;
}
use super::equivalence_trait::{CounterExample, EquivalenceOracle, InternalEquivalenceOracle};
use crate::oracles::equivalence::{CounterExample, EquivalenceOracle, InternalEquivalenceOracle};
use crate::{
automatadefs::{
mealy::{InputSymbol, Mealy, State},
......
use super::equivalence_trait::{CounterExample, EquivalenceOracle, ExternalEquivalenceOracle};
use crate::oracles::equivalence::{CounterExample, EquivalenceOracle, ExternalEquivalenceOracle};
use crate::{
automatadefs::{
mealy::{InputSymbol, Mealy, OutputSymbol},
......@@ -230,7 +230,7 @@ where
.build()
.expect("Safe");
let byte_hyp = MealyWriter::write_machine(
write_config,
&write_config,
hypothesis,
&self.rev_input_map,
&self.rev_output_map,
......
use super::equivalence_trait::{CounterExample, EquivalenceOracle, InternalEquivalenceOracle};
use crate::oracles::equivalence::{CounterExample, EquivalenceOracle, InternalEquivalenceOracle};
use crate::{
automatadefs::{
mealy::{InputSymbol, Mealy, State},
......
use super::equivalence::equivalence_trait::CounterExample;
use crate::learner::l_sharp::{Rule2, Rule3};
use crate::oracles::equivalence::CounterExample;
use crate::{
ads::{
traits::{AdaptiveDistinguishingSequence, AdsStatus},
......@@ -13,10 +14,7 @@ use crate::{
obs_tree::{ObservationTree, TreeErr},
},
sul::SystemUnderLearning,
util::{
learning_config::{Rule2, Rule3},
toolbox,
},
util::toolbox,
};
use itertools::Itertools;
use rand::prelude::SliceRandom;
......
......@@ -13,7 +13,7 @@ use std::fmt;
pub enum EqOracle {
/// [`Hybrid-ADS with Tree`](crate::oracles::equivalence::hads_tree::HadsTree) (*default*).
HadsTree,
/// BFS oracle, see [`Bfs`](crate::oracles::equivalence::bfs::Bfs).
/// Simple shortest separating sequence (can be used iff the FSM is known.)
Internal,
/// Generates tests using Observation tree, see [`SequenceOracle`](crate::oracles::equivalence::sep_seq::SequenceOracle).
SepSeq,
......@@ -34,26 +34,6 @@ impl fmt::Display for EqOracle {
}
}
/// Options for application of rule 2 of the L# algorithm.
#[derive(PartialEq, Eq, Clone, Debug)]
pub enum Rule2 {
/// Identify the new frontier state using an ADS (*default*).
Ads,
/// Basic version, do not attempt to identify the new frontier state.
Nothing,
/// Identify the new frontier state using a (randomly selected) witness for two basis states.
SepSeq,
}
/// Options for application of rule 3 of the L# algorithm.
#[derive(PartialEq, Eq, Clone, Debug)]
pub enum Rule3 {
/// Identify frontier states using an ADS (*default*).
Ads,
/// Identify frontier states using a (randomly selected) witness for two basis states.
SepSeq,
}
/// Stores the metrics of the learning process.
pub struct LearnResult {
pub rounds: usize,
......
......@@ -35,7 +35,7 @@ impl WriteConfig {
}
pub fn write_machine<S: BuildHasher + Default, Machine: FiniteStateMachine>(
config: WriteConfig,
config: &WriteConfig,
fsm: &Machine,
input_rev_map: &HashMap<InputSymbol, String, S>,
output_rev_map: &HashMap<OutputSymbol, String, S>,
......