learning.rs 7.98 KB
Newer Older
Bharat Garhewal's avatar
Bharat Garhewal committed
1
2
3
4
5
use crate::automatadefs::mealy::shortest_separating_sequence;
use crate::learner::l_sharp::{Rule2, Rule3};
use crate::oracles::equivalence::{
    EquivalenceOracle, ExternalEquivalenceOracle, InternalEquivalenceOracle,
};
6
7
use crate::{
    automatadefs::{
8
        mealy::{InputSymbol, Mealy, OutputSymbol},
Bharat Garhewal's avatar
Bharat Garhewal committed
9
        FiniteStateMachine,
10
    },
Bharat Garhewal's avatar
Bharat Garhewal committed
11
    learner::{l_sharp::Lsharp, obs_tree::map_tree::ObsTree as ObsMapTree},
12
13
14
    oracles::{
        equivalence::{
            hads_tree::HadsTree,
Bharat's avatar
Bharat committed
15
            incomplete::iads::IadsEO,
16
            sep_seq::SequenceOracle,
Bharat Garhewal's avatar
Bharat Garhewal committed
17
            soucha::{ConfigBuilder as SouchaConfigBuilder, Oracle as SouchaOracle},
18
19
20
        },
        membership::Oracle as OQOracle,
    },
Bharat Garhewal's avatar
Bharat Garhewal committed
21
    sul::simulator::Simulator,
22
    util::{
Bharat Garhewal's avatar
Bharat Garhewal committed
23
        learning_config::{EqOracle, LearnResult},
24
        writers::overall as MealyWriter,
25
26
    },
};
27
use fnv::{FnvHashMap, FnvHashSet};
28
use rand::{prelude::StdRng, Rng, SeedableRng};
Bharat Garhewal's avatar
Bharat Garhewal committed
29
use std::collections::HashMap;
30
use std::{cell::RefCell, hash::BuildHasherDefault, rc::Rc, sync::Arc};
31

32
33
34
35
36
37
#[derive(derive_builder::Builder)]
pub struct Options {
    pub rule2_mode: Rule2,
    pub rule3_mode: Rule3,
    pub oracle_choice: EqOracle,
    pub seed: u64,
38
    pub extra_states: usize,
39
    // pub expected_rnd_length: usize,
40
41
    pub use_ly_ads: bool,
}
42

43
/// Main function that learns the FSM.
Bharat Garhewal's avatar
Bharat Garhewal committed
44
#[allow(clippy::type_complexity)]
45
#[allow(clippy::too_many_lines)]
46
#[must_use]
Bharat Garhewal's avatar
Bharat Garhewal committed
47
pub fn learn_fsm<S: ::std::hash::BuildHasher>(
48
    sul: &Mealy,
Bharat Garhewal's avatar
Bharat Garhewal committed
49
50
    input_map: &HashMap<String, InputSymbol, S>,
    output_map: &HashMap<String, OutputSymbol, S>,
51
    options: &Options,
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
52
    logs: Option<Vec<(Box<[InputSymbol]>, Box<[OutputSymbol]>)>>,
Bharat's avatar
Bharat committed
53
) -> LearnResult {
54
    let mealy_machine = Arc::new(sul.clone());
55
56
    log::info!("Qsize : {}", mealy_machine.as_ref().states().len());
    log::info!("Isize : {}", mealy_machine.as_ref().input_alphabet().len());
57
58
    let mut trial = Simulator::new(Arc::clone(&mealy_machine));
    let oq_oracle: Rc<RefCell<OQOracle<'_, ObsMapTree<BuildHasherDefault<rustc_hash::FxHasher>>>>> =
Bharat's avatar
Bharat committed
59
60
61
62
63
        Rc::new(RefCell::new(OQOracle::new(
            &mut trial,
            options.rule2_mode.clone(),
            options.rule3_mode.clone(),
        )));
64
    let rev_input_map: FnvHashMap<_, _> = input_map.iter().map(|(x, y)| (*y, x.clone())).collect();
65

66
67
68
69
70
    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(
        Rc::clone(&oq_oracle),
71
        (),
72
        options.extra_states,
73
74
75
76
        rng.gen(),
        rev_input_map.clone(),
        rev_output_map.clone(),
    );
Bharat Garhewal's avatar
Bharat Garhewal committed
77

78
79
80
81
82
83
84
    let soucha_config = SouchaConfigBuilder::default()
        .exec_loc("/Users/bharat/research/FSMlib/fsm_lib")
        .lookahead(options.extra_states)
        .method(options.oracle_choice.clone().into())
        .build()
        .expect("Incorrect/Missing params from Soucha oracles.");
    let mut soucha_oracle = SouchaOracle::with_location(
85
        Rc::clone(&oq_oracle),
86
87
        soucha_config,
        "".to_string(),
88
        0,
89
90
91
92
        0,
        rev_input_map.clone(),
        rev_output_map.clone(),
    );
93
    let mut iads_oracle = IadsEO::new(Rc::clone(&oq_oracle), options.extra_states, rng.gen());
94
95
96
    let mut seq_oracle = SequenceOracle::new(Rc::clone(&oq_oracle), 10, rng.gen());
    let mut learner = Lsharp::new(
        oq_oracle,
97
98
99
100
        &mealy_machine
            .input_alphabet()
            .into_iter()
            .collect::<FnvHashSet<_>>(),
101
        options.use_ly_ads,
102
    );
103
    let mut idx = 1;
Bharat Garhewal's avatar
Bharat Garhewal committed
104
    let success: bool;
105
106
107
108
    let mut learn_inputs: usize = 0;
    let mut learn_resets: usize = 0;
    let mut test_inputs: usize = 0;
    let mut test_resets: usize = 0;
Bharat's avatar
Bharat committed
109
    let mut hyp_states;
110
    learner.init_obs_tree(logs);
111
112
113
    loop {
        println!("LOOP {}", idx);
        let hypothesis = learner.build_hypothesis();
114
115
116
117
118
        let (l_inputs, l_resets) = learner.get_counts();
        learn_inputs += l_inputs;
        learn_resets += l_resets;
        println!("Learning queries/symbols: {}/{}", l_resets, l_inputs,);
        hyp_states = hypothesis.states().len();
Bharat Garhewal's avatar
Bharat Garhewal committed
119
120
121
122
123
        println!(
            "Hypothesis size: {} and model size: {}",
            hyp_states,
            sul.states().len()
        );
124
125
126
127
128
129
        let writer_config = MealyWriter::WriteConfigBuilder::default()
            .file_name(Some(
                format!("./hypothesis/hypothesis_{}.dot", idx).to_string(),
            ))
            .format(MealyWriter::MealyEncoding::Dot)
            .build()
130
            .expect("Could not write Hypothesis file.");
Bharat Garhewal's avatar
Bharat Garhewal committed
131
132
        MealyWriter::write_machine(&writer_config, &hypothesis, &rev_input_map, &rev_output_map);
        let ideal_ce = shortest_separating_sequence(&sul.clone(), &hypothesis, None, None);
133
        if ideal_ce.is_none() {
Bharat Garhewal's avatar
Bharat Garhewal committed
134
            success = true;
Bharat Garhewal's avatar
Bharat Garhewal committed
135
            println!("Learning finished!");
136
137
138
139
            break;
        }
        println!("Searching for CEX...");
        let ce = match options.oracle_choice {
140
141
142
143
144
145
            EqOracle::SouchaH
            | EqOracle::SouchaHSI
            | EqOracle::SouchaSPY
            | EqOracle::SouchaSPYH => {
                let word = soucha_oracle.find_counterexample(&hypothesis);
                let (t_inputs, t_resets) = soucha_oracle.get_counts();
146
147
148
149
150
                test_inputs += t_inputs;
                test_resets += t_resets;
                println!("Testing queries/symbols: {}/{}", t_resets, t_inputs);
                word
            }
151
152
153
154
155
156
157
            EqOracle::SepSeq => {
                let word = seq_oracle.find_counterexample(&hypothesis);
                let (t_inputs, t_resets) = seq_oracle.get_counts();
                test_inputs += t_inputs;
                test_resets += t_resets;
                println!("Testing queries/symbols: {}/{}", t_resets, t_inputs);
                word
158
            }
Bharat Garhewal's avatar
Bharat Garhewal committed
159
            EqOracle::Internal => ideal_ce.clone(),
160
            EqOracle::HadsTree => {
161
                let word = hads_oracle_tree.find_counterexample(&hypothesis);
162
163
164
165
166
                let (t_inputs, t_resets) = hads_oracle_tree.get_counts();
                test_inputs += t_inputs;
                test_resets += t_resets;
                println!("Testing queries/symbols: {}/{}", t_resets, t_inputs);
                word
167
            }
Bharat's avatar
Bharat committed
168
            EqOracle::Iads => {
169
170
                let fs = learner.frontier_basis_map().clone();
                iads_oracle.load_frontier_states(fs);
Bharat's avatar
Bharat committed
171
172
173
174
175
176
177
                let word = iads_oracle.find_counterexample(&hypothesis);
                let (t_inputs, t_resets) = iads_oracle.get_counts();
                test_inputs += t_inputs;
                test_resets += t_resets;
                println!("Testing queries/symbols: {}/{}", t_resets, t_inputs);
                word
            }
178
        };
179
180
        let ce_len = ce.as_ref().map_or(0, |f| f.0.len());
        log::info!("EQStats:{{'Iter':{idx},'HypSize':{hyp_states},'CESize':{ce_len}}}");
181
182
183
184
185
        if ce.is_some() {
            println!("CE found, refining observation tree!");
            learner.process_cex(ce, &hypothesis);
        } else {
            println!("No CE found.");
Bharat Garhewal's avatar
Bharat Garhewal committed
186
            success = ideal_ce.is_none();
Bharat Garhewal's avatar
Bharat Garhewal committed
187
            println!("Model learned: {}", success);
188
            break;
189
190
191
        }
        idx += 1;
    }
Bharat's avatar
Bharat committed
192

193
194
195
196
197
198
199
200
201
202
203
204
205
206
    log::info!("MQ [Resets] : {learn_resets}");
    log::info!("MQ [Symbols] : {learn_inputs}");
    log::info!("EQ [Resets] : {test_resets}");
    log::info!("EQ [Symbols] : {test_inputs}");
    log::info!("Rounds : {idx}");
    log::info!("Searching for counterexample [ms] : {}", 0);
    log::info!("Learning [ms] : {}", 0);
    let equivalent = |learned| {
        if learned {
            "OK"
        } else {
            "NOK"
        }
    };
Bharat Garhewal's avatar
Bharat Garhewal committed
207
    log::info!("Equivalent : {}", equivalent(success));
Bharat's avatar
Bharat committed
208
    let ads_score = learner.get_ads_score();
209
    LearnResult {
210
211
212
        learn_inputs,
        learn_resets,
        eq_oracle: options.oracle_choice.clone(),
213
        rounds: idx,
Bharat Garhewal's avatar
Bharat Garhewal committed
214
        success,
215
216
        test_inputs,
        test_resets,
Bharat's avatar
Update    
Bharat committed
217
218
        num_inputs: rev_input_map.len(),
        num_states: hyp_states,
Bharat's avatar
Bharat committed
219
        ads_score,
220
    }
221
}