Struct WMethodEQ 

pub struct WMethodEQ {
    pub max_states: usize,
    /* private fields */
}

W-method equivalence-test strategy.

Fields

max_states: usize

Upper bound on the number of states in the target system.

Implementations

impl WMethodEQ

pub fn new( knowledge_base: Arc<Mutex<dyn KnowledgeBaseTrait>>, input_letters: Vec<Letter>, max_states: usize, ) -> Self

Create a new W-method equivalence tester.

Examples found in repository

examples/all_eqtests_custom_kb.rs (line 24)

fn main() -> Result<(), Box<dyn std::error::Error>> {
    println!("=== Custom KB: All Equivalence Tests ===");
    println!("System under learning: ATM protocol");

    let mut reports = Vec::new();

    let strategies: Vec<(&str, Box<EqBuilder>)> = vec![
        (
            "WMethodEQ",
            Box::new(|kb, input_letters, max_states| {
                Arc::new(WMethodEQ::new(kb, input_letters, max_states))
            }),
        ),
        (
            "RandomWalkMethod",
            Box::new(|kb, input_letters, _| {
                Arc::new(RandomWalkMethod::new(kb, input_letters, 10_000, 0.75))
            }),
        ),
        (
            "BDistMethod",
            Box::new(|kb, input_letters, _| Arc::new(BDistMethod::new(kb, input_letters, 2))),
        ),
        (
            "MultipleEqtests",
            Box::new(|kb, input_letters, max_states| {
                let eqtests: Vec<Arc<dyn EquivalenceTest>> = vec![
                    Arc::new(WMethodEQ::new(
                        kb.clone(),
                        input_letters.clone(),
                        max_states,
                    )),
                    Arc::new(RandomWalkMethod::new(
                        kb.clone(),
                        input_letters.clone(),
                        5_000,
                        0.65,
                    )),
                    Arc::new(BDistMethod::new(kb, input_letters, 2)),
                ];
                Arc::new(MultipleEqtests::new(eqtests))
            }),
        ),
    ];

    for (name, builder) in strategies {
        reports.push(run_strategy(name, builder.as_ref()));
    }

    print_summary(&reports);

    Ok(())
}

Trait Implementations

impl EquivalenceTest for WMethodEQ

fn find_counterexample( &self, hypothesis: &mut Automata, ) -> Option<Counterexample>

Find a counterexample for the given hypothesis Returns None if the automaton is equivalent to the system under learning