Commit 77766eef authored by Bharat Garhewal's avatar Bharat Garhewal
Browse files

Removed non-tree HADS version

parent 8c6b3595
Pipeline #60647 canceled with stages
in 1 minute and 18 seconds
......@@ -10,7 +10,6 @@ use crate::{
equivalence_trait::{
EquivalenceOracle, ExternalEquivalenceOracle, InternalEquivalenceOracle,
},
hads::HADS,
hads_tree::HadsTree,
incomplete::iads::IadsEO,
sep_seq::SequenceOracle,
......@@ -41,6 +40,7 @@ pub struct Options {
/// Main function that learns the FSM.
#[allow(clippy::type_complexity)]
#[allow(clippy::too_many_lines)]
#[must_use]
pub fn learn_fsm(
sul: &Mealy,
......@@ -73,17 +73,17 @@ 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 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)
......@@ -130,14 +130,13 @@ pub fn learn_fsm(
hyp_states,
sul.states().len()
);
assert!(learner.check_consistency(&hypothesis).is_none());
let writer_config = MealyWriter::WriteConfigBuilder::default()
.file_name(Some(
format!("./hypothesis/hypothesis_{}.dot", idx).to_string(),
))
.format(MealyWriter::MealyEncoding::Dot)
.build()
.unwrap();
.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);
if ideal_ce.is_none() {
......@@ -158,14 +157,6 @@ pub fn learn_fsm(
println!("Testing queries/symbols: {}/{}", t_resets, t_inputs);
word
}
EqOracle::Hads => {
let word = hads_oracle.find_counterexample(&hypothesis);
let (t_inputs, t_resets) = hads_oracle.get_counts();
test_inputs += t_inputs;
test_resets += t_resets;
println!("Testing queries/symbols: {}/{}", t_resets, t_inputs);
word
}
EqOracle::SepSeq => {
let word = seq_oracle.find_counterexample(&hypothesis);
let (t_inputs, t_resets) = seq_oracle.get_counts();
......
......@@ -47,7 +47,6 @@ fn main() -> Result<(), Box<dyn std::error::Error>> {
let oracle_choice = match matches.value_of("eq_oracle").unwrap() {
"int" => EqOracle::Internal,
"hads_tree" => EqOracle::HadsTree,
"hads" => EqOracle::Hads,
"iads" => EqOracle::Iads,
"seq" => EqOracle::SepSeq,
"soucha_h" => EqOracle::SouchaH,
......
......@@ -11,8 +11,8 @@ pub mod automata;
pub mod bfs;
/// Trait for equivalence oracles.
pub mod equivalence_trait;
/// Hybrid-ADS without tree.
pub mod hads;
// /// Hybrid-ADS without tree.
// pub mod hads;
/// Hybrid-ADS oracle.
pub mod hads_tree;
/// Soucha IADS algorithm.
......
......@@ -51,7 +51,7 @@ pub fn parse() -> Result<clap::ArgMatches, Box<dyn std::error::Error>> {
.long("eq_oracle")
.value_name("EO")
.default_value("hads_tree")
.possible_values(&["int", "hads", "seq", "hads_tree", "iads", "soucha_h", "soucha_hsi", "soucha_spy", "soucha_spyh"])
.possible_values(&["int", "seq", "hads_tree", "iads", "soucha_h", "soucha_hsi", "soucha_spy", "soucha_spyh"])
.help("Equivalence Oracle")
.takes_value(true),
)
......
......@@ -11,8 +11,6 @@ use std::fmt;
/// Equivalence oracle.
#[derive(PartialEq, Eq, Clone, Debug)]
pub enum EqOracle {
/// [`Hybrid-ADS`](crate::oracles::equivalence::hads::HADS).
Hads,
/// [`Hybrid-ADS with Tree`](crate::oracles::equivalence::hads_tree::HadsTree) (*default*).
HadsTree,
/// BFS oracle, see [`Bfs`](crate::oracles::equivalence::bfs::Bfs).
......
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