Commit 50ad8f76 authored by Bharat Garhewal's avatar Bharat Garhewal
Browse files

Removed redundant HADS file and cleaned up HADS tree

parent 3c25f3f4
Pipeline #60922 failed with stages
in 1 minute and 9 seconds
......@@ -30,6 +30,8 @@ shrinkwraprs = "0.3.0"
clap = "3.1.2"
log4rs = "1.0.0"
derive-alias = "0.1.0"
strum = "0.24.1"
strum_macros = "0.24"
num-format = "0.4.0"
priority-queue = "1.2.1"
libloading = "0.7"
......
......@@ -9,7 +9,7 @@ use crate::{
},
oracles::{
equivalence::{
hads_tree::HadsTree,
hads_tree::{HadsConfigBuilder, HadsTree, Mode, Prefix, Suffix},
incomplete::iads::IadsEO,
sep_seq::SequenceOracle,
soucha::{ConfigBuilder as SouchaConfigBuilder, Oracle as SouchaOracle},
......@@ -67,14 +67,23 @@ pub fn learn_fsm<S: ::std::hash::BuildHasher + Default>(
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 mut hads_oracle_tree = HadsTree::new(
let hads_config = HadsConfigBuilder::default()
.mode(Mode::Random)
.prefix(Prefix::Buggy)
.suffix(Suffix::Hads)
.extra_states(0)
.expected_rnd_length(options.extra_states)
.seed(options.seed)
.build()
.expect("Safe");
println!("HADS config : {:?}", hads_config);
let mut hads_oracle_tree = HadsTree::build(
Rc::clone(&oq_oracle),
(),
options.extra_states,
rng.gen(),
rev_input_map.clone(),
rev_output_map.clone(),
);
hads_config,
"./hybrid-ads/build/main",
)
.expect("Safe");
let soucha_config = SouchaConfigBuilder::default()
.exec_loc("/Users/bharat/research/FSMlib/fsm_lib")
......
use crate::sul::simulator::Simulator;
use crate::util::writers::overall as MealyWriter;
use crate::{
automatadefs::{
mealy::{InputSymbol, Mealy, OutputSymbol},
traits::FiniteStateMachine,
},
sul::system_under_learning::SystemUnderLearning,
};
use fnv::FnvHashMap;
use itertools::Itertools;
use rayon::iter::{IntoParallelRefIterator, ParallelIterator};
use std::{
io::{BufRead, BufReader, Write},
process::{Child, Command, Stdio},
time::Instant,
};
pub struct HADS<'a> {
sut: &'a mut Simulator,
lookahead: u32,
inputs_used: usize,
resets_used: usize,
seed: i32,
rev_input_map: FnvHashMap<InputSymbol, String>,
rev_output_map: FnvHashMap<OutputSymbol, String>,
}
impl<'a> HADS<'a> {
pub fn new(
sut: &'a mut Simulator,
lookahead: u32,
seed: i32,
rev_input_map: FnvHashMap<InputSymbol, String>,
rev_output_map: FnvHashMap<OutputSymbol, String>,
) -> Self {
Self {
sut,
lookahead,
rev_input_map,
rev_output_map,
seed,
inputs_used: 0,
resets_used: 0,
}
}
pub fn find_counterexample(
&mut self,
hypothesis: &Mealy,
) -> Option<(Vec<InputSymbol>, Vec<OutputSymbol>)> {
let mut child = self.hads_process();
{
let write_config = MealyWriter::WriteConfigBuilder::default()
.file_name(None)
.format(MealyWriter::MealyEncoding::Dot)
.build()
.expect("Building writer failed.");
let byte_hyp = MealyWriter::write_machine(
write_config,
hypothesis,
&self.rev_input_map,
&self.rev_output_map,
)
.expect("Writer did not return the byte-encoded mealy machine.");
// let byte_hyp =
// dot_fmt::write_dot_to_bytes(hypothesis, &self.rev_input_map, &self.rev_output_map);
let child_stdin = child.stdin.as_mut().unwrap();
child_stdin
.write_all(&byte_hyp)
.expect("Failed to write hypothesis model to h-ads program!");
child_stdin
.flush()
.expect("Failed to write hypothesis model to h-ads program!");
}
// Get a Pipestream, which implements the Reader trait.
let mut child_out = BufReader::new(child.stdout.as_mut().unwrap());
let start = Instant::now();
let input_map = self
.rev_input_map
.iter()
.map(|(x, y)| (y.clone(), *x))
.collect();
loop {
let buffer = read_into_buffer(&mut child_out, 100, &input_map);
for input_vec in buffer {
self.resets_used += 1;
let mut ce = Vec::<InputSymbol>::with_capacity(input_vec.len());
let mut hyp_dest = hypothesis.initial_state();
let mut sul_output = Vec::<OutputSymbol>::with_capacity(input_vec.len());
for input in input_vec {
ce.push(input);
let dest_output_pair = hypothesis.step_from(hyp_dest, input);
hyp_dest = dest_output_pair.0;
let hyp_output = dest_output_pair.1;
let sut_output = self.sut.step(&[input])[0];
sul_output.push(sut_output);
self.inputs_used += 1;
if hyp_output != sut_output {
child
.kill()
.expect("Could not manage to kill H-ADS process.");
self.sut.reset();
return Some((ce, sul_output));
}
}
self.sut.reset();
}
if start.elapsed().as_secs() >= 20 * 60 {
return None;
}
}
}
fn hads_process(&self) -> Child {
let h_ads_path = std::fs::canonicalize("./hybrid-ads/build/main").unwrap();
Command::new(h_ads_path)
.args(&[
"-p",
"buggy",
"-m",
"random",
"-k",
&self.lookahead.to_string(),
"-s",
"hads",
"-r",
"10",
"-x",
&self.seed.to_string(),
])
.stdin(Stdio::piped())
.stdout(Stdio::piped())
.stderr(Stdio::piped())
.spawn()
.unwrap()
}
pub fn get_counts(&mut self) -> (usize, usize) {
let ret = (self.inputs_used, self.resets_used);
self.inputs_used = 0;
self.resets_used = 0;
ret
}
}
fn read_into_buffer(
child_out: &mut BufReader<&mut std::process::ChildStdout>,
buffer_size: usize,
input_map_ref: &FnvHashMap<String, InputSymbol>,
) -> Vec<Vec<InputSymbol>> {
let mut string_vec = Vec::new();
let mut i = 0;
while i <= buffer_size {
let mut strline = String::new();
child_out.read_line(&mut strline).unwrap();
if strline.is_empty() {
continue;
}
string_vec.push(strline);
i += 1;
}
string_vec
.par_iter()
.map(|strline| {
strline
.trim()
.split_ascii_whitespace()
.map(|str_input| input_map_ref.get(str_input).expect("Safe"))
.copied()
.collect_vec()
})
.collect()
}
use crate::oracles::equivalence::{CounterExample, EquivalenceOracle, ExternalEquivalenceOracle};
use super::{CounterExample, EquivalenceOracle};
use crate::{
automatadefs::{
mealy::{InputSymbol, Mealy, OutputSymbol},
mealy::{InputSymbol, Mealy},
FiniteStateMachine,
},
learner::obs_tree::ObservationTree,
oracles::membership::Oracle as OQOracle,
util::writers::overall as MealyWriter,
};
use derive_builder::Builder;
use fnv::FnvHashMap;
use itertools::Itertools;
use std::{
......@@ -19,6 +20,18 @@ use std::{
time::{Duration, Instant},
};
#[derive(Default, Builder, Debug)]
pub struct HadsConfig {
mode: Mode,
prefix: Prefix,
suffix: Suffix,
#[builder(default = "3")]
extra_states: usize,
#[builder(default = "5")]
expected_rnd_length: usize,
seed: u64,
}
/**
Hybrid-ADS equivalence oracle.
......@@ -30,60 +43,15 @@ the repository.
*/
pub struct HadsTree<'a, T> {
oq_oracle: Rc<RefCell<OQOracle<'a, T>>>,
lookahead: usize,
config: HadsConfig,
location: String,
seed: u64,
rev_input_map: FnvHashMap<InputSymbol, String>,
rev_output_map: FnvHashMap<OutputSymbol, String>,
}
impl<'a, T> ExternalEquivalenceOracle<'a, T> for HadsTree<'a, T>
where
T: ObservationTree + Sync + Send,
{
fn new(
output_oracle: Rc<RefCell<OQOracle<'a, T>>>,
_config: (),
lookahead: usize,
random_seed: u64,
rev_input_map: FnvHashMap<InputSymbol, String>,
rev_output_map: FnvHashMap<OutputSymbol, String>,
) -> Self {
Self::with_location(
output_oracle,
(),
"./hybrid-ads/build/main".to_string(),
lookahead,
random_seed,
rev_input_map,
rev_output_map,
)
}
fn with_location(
output_oracle: Rc<RefCell<OQOracle<'a, T>>>,
_config: (),
location: String,
lookahead: usize,
random_seed: u64,
rev_input_map: FnvHashMap<InputSymbol, String>,
rev_output_map: FnvHashMap<OutputSymbol, String>,
) -> Self {
Self {
oq_oracle: output_oracle,
lookahead,
location,
seed: random_seed,
rev_input_map,
rev_output_map,
}
}
}
impl<'a, T> EquivalenceOracle<'a, T> for HadsTree<'a, T>
where
T: ObservationTree + Sync + Send,
{
type Options = HadsConfig;
fn get_counts(&mut self) -> (usize, usize) {
RefCell::borrow_mut(&self.oq_oracle).get_counts()
}
......@@ -93,68 +61,16 @@ where
let sleepy = Duration::from_millis(100);
thread::sleep(sleepy);
}
let mut child = self.hads_process(None);
{
let write_config = MealyWriter::WriteConfigBuilder::default()
.file_name(None)
.format(MealyWriter::MealyEncoding::Dot)
.build()
.unwrap();
let byte_hyp = MealyWriter::write_machine(
&write_config,
hypothesis,
&self.rev_input_map,
&self.rev_output_map,
)
.expect("Writer did not return the byte-encoded mealy machine.");
// let byte_hyp =
// dot_fmt::write_dot_to_bytes(hypothesis, &self.rev_input_map, &self.rev_output_map);
let child_stdin = child.stdin.as_mut().unwrap();
child_stdin
.write_all(&byte_hyp)
.expect("Failed to write hypothesis model to h-ads program!");
child_stdin
.flush()
.expect("Failed to write hypothesis model to h-ads program!");
}
// Get a Pipestream, which implements the Reader trait.
let mut child_out = BufReader::new(child.stdout.as_mut().unwrap());
let start = Instant::now();
let mut oracle_mut_borrow = RefCell::borrow_mut(&self.oq_oracle);
let mut buffer = Vec::new();
let input_map = self
.rev_input_map
.iter()
.map(|(k, v)| (v.clone(), *k))
.collect();
loop {
Self::read_into_buffer(&mut child_out, 10000, &input_map, &mut buffer);
for input_vec in &buffer {
let hyp_output = hypothesis.trace(input_vec).1.to_vec();
let sut_output = oracle_mut_borrow.output_query(input_vec);
if hyp_output != sut_output {
child
.kill()
.expect("Could not manage to kill H-ADS process.");
let ce_input = input_vec.clone();
let ce_output = sut_output;
let ret = Some((ce_input, ce_output));
return ret;
}
}
buffer.clear();
if start.elapsed().as_secs() >= 20 * 60 {
return None;
}
}
self.find_counterexample_with_lookahead(hypothesis, self.config.extra_states)
}
fn find_counterexample_with_lookahead(
&mut self,
hypothesis: &Mealy,
lookahead: usize,
) -> CounterExample {
let mut child = self.hads_process(Some(lookahead));
let mut child = self
.hads_process(Some(lookahead))
.expect("H-ADS process did not initialise.");
{
let write_config = MealyWriter::WriteConfigBuilder::default()
.file_name(None)
......@@ -164,12 +80,10 @@ where
let byte_hyp = MealyWriter::write_machine(
&write_config,
hypothesis,
&self.rev_input_map,
&self.rev_output_map,
&FnvHashMap::default(),
&FnvHashMap::default(),
)
.expect("Writer did not return the byte-encoded mealy machine.");
// let byte_hyp =
// dot_fmt::write_dot_to_bytes(hypothesis, &self.rev_input_map, &self.rev_output_map);
let child_stdin = child.stdin.as_mut().unwrap();
child_stdin
.write_all(&byte_hyp)
......@@ -183,13 +97,8 @@ where
let start = Instant::now();
let mut oracle_mut_borrow = RefCell::borrow_mut(&self.oq_oracle);
let mut buffer = Vec::new();
let input_map = self
.rev_input_map
.iter()
.map(|(k, v)| (v.clone(), *k))
.collect();
loop {
Self::read_into_buffer(&mut child_out, 10000, &input_map, &mut buffer);
Self::read_into_buffer(&mut child_out, 10000, &mut buffer);
for input_vec in &buffer {
let hyp_output = hypothesis.trace(input_vec).1.to_vec();
let sut_output = oracle_mut_borrow.output_query(input_vec);
......@@ -209,42 +118,62 @@ where
}
}
}
type Options = ();
}
impl<'a, T> HadsTree<'a, T>
where
T: ObservationTree + Sync,
{
fn hads_process(&self, lookahead_custom: Option<usize>) -> Child {
// let h_ads_path = std::fs::canonicalize("./hybrid-ads/build/main").unwrap();
let h_ads_path = std::fs::canonicalize(self.location.clone()).unwrap();
let random_infix_length = lookahead_custom.unwrap_or(self.lookahead);
Command::new(h_ads_path)
/// # Errors
/// Should not be any.
pub fn build(
output_oracle: Rc<RefCell<OQOracle<'a, T>>>,
config: HadsConfig,
location: &str,
) -> Result<Self, Box<dyn std::error::Error>> {
let hads_path = std::fs::canonicalize(location)?;
let ret = Self {
oq_oracle: output_oracle,
location: hads_path
.to_str()
.ok_or("Path is not valid UTF-8")?
.to_string(),
config,
};
Ok(ret)
}
fn hads_process(
&self,
lookahead_custom: Option<usize>,
) -> Result<Child, Box<dyn std::error::Error>> {
let h_ads_path = std::fs::canonicalize(self.location.clone())?;
let es = lookahead_custom.unwrap_or(self.config.extra_states);
let c = Command::new(h_ads_path)
.args(&[
"-p",
"buggy",
"-m",
"random",
self.config.mode.to_string().to_ascii_lowercase().as_str(),
"-p",
self.config.prefix.to_string().to_ascii_lowercase().as_str(),
"-k",
"0",
&es.to_string(),
"-s",
"hads",
self.config.suffix.to_string().to_ascii_lowercase().as_str(),
"-r",
&random_infix_length.to_string(),
&self.config.expected_rnd_length.to_string(),
"-x",
&self.seed.to_string(),
&self.config.seed.to_string(),
])
.stdin(Stdio::piped())
.stdout(Stdio::piped())
.stderr(Stdio::piped())
.spawn()
.unwrap()
.spawn()?;
Ok(c)
}
fn read_into_buffer(
child_out: &mut BufReader<&mut std::process::ChildStdout>,
buffer_size: usize,
input_map_ref: &FnvHashMap<String, InputSymbol>,
ret: &mut Vec<Vec<InputSymbol>>,
) {
let mut string_vec = Vec::with_capacity(buffer_size);
......@@ -264,10 +193,50 @@ where
strline
.trim()
.split_ascii_whitespace()
.map(|str_input| input_map_ref.get(str_input).expect("Safe"))
.copied()
.map(|str_input| InputSymbol::from(str_input.parse::<usize>().expect("Safe")))
.collect_vec()
})
.for_each(|x| ret.push(x));
}
}
use std::string::ToString;
#[derive(PartialEq, Eq, Clone, Copy, strum_macros::Display, Debug)]
pub enum Mode {
All,
Fixed,
Random,
}
impl Default for Mode {
fn default() -> Self {
Self::Random
}
}
#[derive(PartialEq, Eq, Clone, Copy, strum_macros::Display, Debug)]
pub enum Prefix {
Minimal,
Lexmin,
Buggy,
Longest,
}
impl Default for Prefix {
fn default() -> Self {
Self::Buggy
}
}
#[derive(PartialEq, Eq, Clone, Copy, strum_macros::Display, Debug)]
pub enum Suffix {
Hads,
Hsi,
None,
}
impl Default for Suffix {
fn default() -> Self {
Self::Hads
}
}
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