l_sharp.rs 16.8 KB
Newer Older
1
2
3
use crate::{
    ads::{
        lee_yannakakis::adaptive_distinguishing_seq::AdsTree as LyAds,
Bharat Garhewal's avatar
Bharat Garhewal committed
4
        traits::AdaptiveDistinguishingSequence, tree::threaded::Ads as OtAds,
5
6
    },
    automatadefs::{
7
        mealy::{InputSymbol, Mealy, MealyBuilder, OutputSymbol, State},
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
8
        traits::{FiniteStateMachine, ObservationTree},
9
10
11
12
13
14
    },
    learner::apartness::{compute_witness, states_are_apart},
    oracles::{equivalence::equivalence_trait::CounterExample, membership::Oracle as OutputOracle},
    util::{parsers::logs::Logs, toolbox},
};
use itertools::Itertools;
Bharat Garhewal's avatar
Bharat Garhewal committed
15
use rayon::iter::{IntoParallelRefIterator, IntoParallelRefMutIterator, ParallelIterator};
16
17
18
19
use std::{
    cell::RefCell,
    collections::{HashMap, HashSet, VecDeque},
    fmt::Debug,
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
20
    hash::{BuildHasher, BuildHasherDefault},
21
22
23
24
25
26
27
28
29
    rc::Rc,
};

/// Struct for the learner.
pub struct Lsharp<'a, Tree, S> {
    /// OutputQuery Oracle, needed by the Learner.
    oq_oracle: Rc<RefCell<OutputOracle<'a, Tree>>>,
    /// Size of the input alphabet.
    input_size: usize,
30
    /// List of basis states.
31
    basis: Vec<State>,
32
    /// Frontier state &mapsto; set of basis candidate states.
33
    frontier_to_basis_map: HashMap<State, Vec<State>, S>,
34
35
36
37
    /// Use the Lee-Yannakakis optimisation.
    use_ly_ads: bool,
    /// Num of `consistency` CEs generated.
    consistency_ce_count: usize,
Bharat Garhewal's avatar
Bharat Garhewal committed
38
39
}

40
41
42
43
44
45
46
47
48
49
impl<'a, Tree, S> Lsharp<'a, Tree, S>
where
    Tree: ObservationTree + Sync + Debug + Send,
    S: BuildHasher + Default + Send + Sync,
{
    /// Constructor.
    ///
    /// We require an oracle for asking output queries, (wrapped in an `Rc<RefCell<>>`),
    /// the input alphabet of the FSM to be learned, and a flag for enabling the use of
    /// the Lee-Yannakakis optimisation.
Bharat Garhewal's avatar
Bharat Garhewal committed
50
    pub fn new(
51
52
53
        oracle: Rc<RefCell<OutputOracle<'a, Tree>>>,
        input_alphabet: &HashSet<InputSymbol, S>,
        use_ly_ads: bool,
Bharat Garhewal's avatar
Bharat Garhewal committed
54
    ) -> Self {
Bharat Garhewal's avatar
Bharat Garhewal committed
55
        Self {
56
57
58
            oq_oracle: oracle,
            input_size: input_alphabet.len(),
            basis: vec![State::new(0)],
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
59
            frontier_to_basis_map: HashMap::default(),
60
            use_ly_ads,
61
            consistency_ce_count: 0,
Bharat Garhewal's avatar
Bharat Garhewal committed
62
63
64
        }
    }

65
66
67
68
69
70
71
72
73
74
75
76
77
    /// Process the given counterexample in order to find the new state.
    ///
    /// We require the hypothesis in order to find the prefix of input sequence
    /// to the point that the hypothesis and observation tree agree
    /// (i.e., have the same outputs).
    pub fn process_cex(&mut self, counter_example: CounterExample, hypothesis: &Mealy) {
        let (ce_input, ce_output) = {
            let unwrapped_ce = counter_example.expect("Safe");
            (unwrapped_ce.0, unwrapped_ce.1)
        };
        let _ = RefCell::borrow_mut(&self.oq_oracle).add_observation(&ce_input, &ce_output);
        let (_, hyp_output) = hypothesis.trace(&ce_input);
        let prefix_idx = get_ce_prefix_idx(&ce_output, &hyp_output);
Bharat Garhewal's avatar
Bharat Garhewal committed
78
79
80
81
        self.process_bin_search(
            &ce_input[..prefix_idx],
            &ce_output[..prefix_idx],
            hypothesis,
Bharat Garhewal's avatar
Bharat Garhewal committed
82
        );
Bharat Garhewal's avatar
Bharat Garhewal committed
83
84
    }

85
86
87
88
    pub fn frontier_basis_map(&self) -> &HashMap<State, Vec<State>, S> {
        &self.frontier_to_basis_map
    }

Bharat Garhewal's avatar
Bharat Garhewal committed
89
    #[allow(clippy::many_single_char_names)]
90
    fn process_bin_search(
Bharat Garhewal's avatar
Bharat Garhewal committed
91
        &mut self,
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
92
93
        ce_input: &[InputSymbol],
        ce_output: &[OutputSymbol],
Bharat Garhewal's avatar
Bharat Garhewal committed
94
95
96
        hypothesis: &Mealy,
    ) {
        let q: State = hypothesis.trace(ce_input).0;
97
98
99
        let r: State = RefCell::borrow(&self.oq_oracle)
            .borrow_tree()
            .get_succ(State::new(0), ce_input)
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
100
            .expect("Safe");
101
102
        self.update_frontier_and_basis();
        if self.frontier_to_basis_map.contains_key(&r) || self.basis.contains(&r) {
103
104
            return;
        }
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
105
106
        let temp = RefCell::borrow(&self.oq_oracle);
        let o_tree = temp.borrow_tree();
107
        // Get the prefix of the CE input that is leading to a frontier state.
108
109
110
        let idx = {
            let mut src = State::new(0);
            let mut i = 0;
111
            for (idx, input) in ce_input.iter().enumerate() {
112
113
114
115
                let dest = o_tree
                    .get_succ(src, &[*input])
                    .expect("Obs-Tree should have CE included!");
                if self.frontier_to_basis_map.contains_key(&dest) {
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
116
                    i = idx;
117
                    break;
Bharat Garhewal's avatar
Bharat Garhewal committed
118
                }
119
                src = dest;
Bharat Garhewal's avatar
Bharat Garhewal committed
120
            }
121
            i + 1
122
        };
123

Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
124
125
126
        let eta = compute_witness(o_tree, q, r)
            .expect("Could not find witness when it should exist, during CE processing!");

127
        // We used idx inputs to get to the frontier.
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
128
        let rho = &ce_input[..idx];
129
130
        let x = rho.len();
        let y = ce_input.len();
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
131
132
133
        #[allow(clippy::cast_possible_truncation)]
        #[allow(clippy::cast_precision_loss)]
        #[allow(clippy::cast_sign_loss)]
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
134
        let h = ((x as f32 + y as f32) / 2_f32).floor() as usize;
135

Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
136
137
        let sigma_1 = &ce_input[..h];
        let sigma_2 = &ce_input[h..];
138
        let q_p = hypothesis.trace(sigma_1).0;
139
140
141
142
143
144
145
146
147
148
        let r_p = o_tree.get_succ(State::new(0), sigma_1).unwrap();
        let access_q_p = o_tree.get_access_seq(q_p);
        let output_query = toolbox::concat_slices(&[&access_q_p, sigma_2, &eta]);
        drop(temp);
        let sul_response = RefCell::borrow_mut(&self.oq_oracle).output_query(&output_query);
        let temp = RefCell::borrow(&self.oq_oracle);
        let o_tree = temp.borrow_tree();
        let wit = compute_witness(o_tree, q_p, r_p);
        drop(temp);
        if wit.is_some() {
Bharat Garhewal's avatar
Bharat Garhewal committed
149
            self.process_bin_search(sigma_1, &ce_output[..sigma_1.len()], hypothesis);
150
        } else {
151
            let new_inputs = toolbox::concat_slices(&[&access_q_p, sigma_2]);
Bharat Garhewal's avatar
Bharat Garhewal committed
152
            self.process_bin_search(&new_inputs, &sul_response[..new_inputs.len()], hypothesis);
Bharat Garhewal's avatar
Bharat Garhewal committed
153
154
155
        }
    }

156
157
158
159
160
161
    /**
    We loop through the following three rules until the observation tree is adequate:
    1. Explore the frontier (implemented [here](crate::oracles::membership::Oracle::explore_frontier)).
    2. Identify the frontier (implemented [here](crate::oracles::membership::Oracle::identify_frontier)).
    3. Promote a frontier state if possible (internal method of this struct).
    */
Bharat Garhewal's avatar
Bharat Garhewal committed
162
    fn make_obs_tree_adequate(&mut self) {
163
164
165
166
        log::info!(
            "Size of tree after EQ: {}",
            RefCell::borrow(&self.oq_oracle).borrow_tree().size()
        );
Bharat Garhewal's avatar
Bharat Garhewal committed
167
        loop {
Bharat's avatar
Bharat committed
168
            log::debug!("Applying rule 2");
169
170
171
172
173
            let new_frontier = RefCell::borrow_mut(&self.oq_oracle).explore_frontier(&self.basis);
            for (fs, cands) in new_frontier {
                log::debug!("Adding frontier {:?} with candidates {:?}", fs, cands);
                self.frontier_to_basis_map.insert(fs, cands);
            }
Bharat Garhewal's avatar
Bharat Garhewal committed
174

175
            // Identify the frontier states
Bharat's avatar
Bharat committed
176
            log::debug!("Applying rule 3");
177
178
179
180
181
182
183
184
            for (fs, candidates) in self
                .frontier_to_basis_map
                .iter_mut()
                .filter(|(_fs, c)| c.len() > 1)
            {
                log::debug!("Identifying {:?} amongst {:?}", fs, candidates);
                RefCell::borrow_mut(&self.oq_oracle).identify_frontier(*fs, candidates);
            }
Bharat Garhewal's avatar
Bharat Garhewal committed
185

186
187
            // Promote the frontier states if they're isolated.
            self.promote_frontier_state();
188

189
            if self.tree_is_adequate() {
Bharat Garhewal's avatar
Bharat Garhewal committed
190
191
192
193
194
                break;
            }
        }
    }

195
196
197
198
199
200
201
202
203
204
    fn promote_frontier_state(&mut self) {
        let new_bs = self
            .frontier_to_basis_map
            .iter()
            .find(|(_fs, bs_not_sep)| bs_not_sep.is_empty())
            .map(|(&fs, _)| fs);
        let bs = match new_bs {
            Some(bs) => bs,
            _ => return,
        };
Bharat's avatar
Bharat committed
205
206
        log::debug!("Applying rule 4");
        log::debug!("Promoting {:?}", bs);
207
208
209
210
211
212
213
214
215
216
        self.basis.push(bs);
        self.frontier_to_basis_map.remove(&bs);
        let temp = RefCell::borrow(&self.oq_oracle);
        let o_tree = temp.borrow_tree();
        // The new basis state is a candidate for the frontier
        // states it is not apart from.
        self.frontier_to_basis_map
            .par_iter_mut()
            .filter(|(&fs, _cands)| !states_are_apart(o_tree, fs, bs))
            .for_each(|(_fs, cands)| {
217
                cands.push(bs);
218
            });
219
220
    }

221
222
223
224
225
226
227
    /// If each frontier state is identified, a tree is adequate.
    ///
    /// *We assume that all basis states have been explored*.
    fn tree_is_adequate(&mut self) -> bool {
        self.check_frontier_consistency();
        log::debug!("Basis set: {:?}", self.basis);
        log::debug!("Frontier->Basis mapping: {:?}", self.frontier_to_basis_map);
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
228
229
230
        let is_singleton = |c: &Vec<State>| c.len() == 1;
        let all_frontier_identified = self.frontier_to_basis_map.values().all(is_singleton);
        let input_alphabet = toolbox::inputs_iterator(self.input_size).collect_vec();
231
232
233
234
235
236
        let temp = RefCell::borrow(&self.oq_oracle);
        let o_tree = temp.borrow_tree();
        let all_basis_extended = self
            .basis
            .iter()
            .copied()
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
237
            .cartesian_product(input_alphabet)
238
239
            .all(|(q, i)| o_tree.get_out(q, i).is_some());
        all_frontier_identified && all_basis_extended
Bharat Garhewal's avatar
Bharat Garhewal committed
240
241
    }

242
243
244
245
246
247
248
    fn update_frontier_and_basis(&mut self) {
        {
            let temp = RefCell::borrow(&self.oq_oracle);
            let o_tree = temp.borrow_tree();
            self.frontier_to_basis_map
                .par_iter_mut()
                .for_each(|(&fs, cands)| cands.retain(|&bs| !states_are_apart(o_tree, fs, bs)));
Bharat Garhewal's avatar
Bharat Garhewal committed
249
        }
250
251
252
253
254
255
256
257
        self.promote_frontier_state();
        self.check_frontier_consistency();
        {
            let temp = RefCell::borrow(&self.oq_oracle);
            let o_tree = temp.borrow_tree();
            self.frontier_to_basis_map
                .par_iter_mut()
                .for_each(|(&fs, cands)| cands.retain(|&bs| !states_are_apart(o_tree, fs, bs)));
Bharat Garhewal's avatar
Bharat Garhewal committed
258
        }
259
260
    }

261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
    /// Make the observation tree adequate and return the hypothesis.
    pub fn build_hypothesis(&mut self) -> Mealy {
        loop {
            self.make_obs_tree_adequate();
            let hyp = self.construct_hypothesis();
            if let Some(ce) = self.check_consistency(&hyp) {
                self.consistency_ce_count += 1;
                self.process_cex(Some(ce), &hyp);
            } else {
                if self.use_ly_ads {
                    let mut ly_ads = LyAds::new(&hyp);
                    let temp = RefCell::borrow(&self.oq_oracle);
                    let tree = temp.borrow_tree();
                    let hyp_states: Vec<_> = hyp.states().into_iter().collect();
                    let ot_ads = OtAds::new(tree, &hyp_states);
                    drop(temp);
                    if ly_ads.identification_power() > ot_ads.identification_power() * 10f32 {
                        self.run_ly_ads(&mut ly_ads);
                        continue;
                    }
Bharat Garhewal's avatar
Bharat Garhewal committed
281
                }
282
283
284
                println!(
                    "Size of the tree: {}",
                    RefCell::borrow(&self.oq_oracle).borrow_tree().size()
Bharat's avatar
Bharat committed
285
                );
286
                return hyp;
Bharat Garhewal's avatar
Bharat Garhewal committed
287
            }
288
        }
Bharat Garhewal's avatar
Bharat Garhewal committed
289
290
    }

291
292
293
294
    fn construct_hypothesis(&mut self) -> Mealy {
        let temp = RefCell::borrow(&self.oq_oracle);
        let o_tree = temp.borrow_tree();
        let basis = self.basis.iter().copied().collect::<HashSet<_, _>>();
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
295
        let hyp_input_alphabet = toolbox::inputs_iterator(self.input_size).collect_vec();
296
297
        let func_size = basis.len() * hyp_input_alphabet.len();
        let mut hyp_output_alphabet = HashSet::<_, _>::default();
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
298
299
300
301
        let mut hyp_trans_fn =
            HashMap::with_capacity_and_hasher(func_size, BuildHasherDefault::default());
        let mut hyp_output_fn =
            HashMap::with_capacity_and_hasher(func_size, BuildHasherDefault::default());
Bharat's avatar
Bharat committed
302
303
        log::debug!("Basis set: {:?}", self.basis);
        log::debug!("Frontier-Basis sep: {:?}", self.frontier_to_basis_map);
304
305
306
307

        for (q, i) in
            Itertools::cartesian_product(basis.iter().copied(), hyp_input_alphabet.iter().copied())
        {
308
309
310
            if o_tree.get_out(q, i).is_none() {
                println!("Something is wrong!");
            }
311
312
313
314
315
316
317
318
            let output = o_tree.get_out(q, i).expect("Safe");
            hyp_output_alphabet.insert(output);
            let succ = o_tree
                .get_succ(q, &[i])
                .expect("Frontier-Basis sep and observation tree are inconsistent.");
            let dest = {
                if basis.contains(&succ) {
                    succ
Bharat Garhewal's avatar
Bharat Garhewal committed
319
                } else {
320
321
322
323
324
325
326
327
                    // Destination is another basis state.
                    *self
                        .frontier_to_basis_map
                        .get(&succ)
                        .expect("Missing a frontier state")
                        .iter()
                        .exactly_one()
                        .expect("Multiple basis candidates for a single frontier state.")
Bharat Garhewal's avatar
Bharat Garhewal committed
328
329
                }
            };
330
331
            hyp_trans_fn.insert((q, i), dest);
            hyp_output_fn.insert((q, i), output);
Bharat Garhewal's avatar
Bharat Garhewal committed
332
        }
333
334
335
336
337
338
339
340
341
342
343
        log::info!("Size of the tree: {}", o_tree.size());

        MealyBuilder::default()
            .initial_state(State::new(0))
            .states(basis)
            .input_alphabet(hyp_input_alphabet)
            .output_alphabet(hyp_output_alphabet)
            .trans_function(hyp_trans_fn)
            .output_function(hyp_output_fn)
            .build()
            .expect("Safe")
Bharat Garhewal's avatar
Bharat Garhewal committed
344
345
    }

Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
346
    #[allow(clippy::unused_self)]
347
348
    fn run_ly_ads(&mut self, _ly_ads: &mut LyAds) {
        todo!()
349
350
    }

351
352
353
354
355
356
357
358
359
    /**
    Initialise the observation tree.
    If logs are provided, we simply add them all to the tree at this point.
    */
    pub fn init_obs_tree(&mut self, logs: Option<Logs>) {
        if let Some(logs) = logs {
            let mut oracle_ref = self.oq_oracle.borrow_mut();
            for (input_seq, output_seq) in logs {
                let _ = oracle_ref.add_observation(&input_seq, &output_seq);
Bharat Garhewal's avatar
Bharat Garhewal committed
360
361
            }
        }
362
        self.make_obs_tree_adequate();
Bharat Garhewal's avatar
Bharat Garhewal committed
363
364
    }

365
366
367
368
369
370
371
    /// Check if the frontier is consistent with our data structures.
    /// CE processing may add a new frontier state that we miss.
    fn check_frontier_consistency(&mut self) {
        let basis_set = &self.basis;
        let input_alph = self.input_size;
        let temp = RefCell::borrow(&self.oq_oracle);
        let o_tree = temp.borrow_tree();
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
372
373
        let ia = toolbox::inputs_iterator(input_alph).collect_vec();
        let state_input_iterator = Itertools::cartesian_product(basis_set.iter().copied(), ia);
374
375
376
377
378
        let new_front = state_input_iterator
            .filter_map(|(bs, i)| o_tree.get_succ(bs, &[i]))
            .filter(|x| !self.basis.contains(x))
            .filter(|x| !self.frontier_to_basis_map.contains_key(x))
            .map(|fs| {
379
                let maps_to: Vec<_> = basis_set
380
381
382
383
384
                    .par_iter()
                    .copied()
                    .filter(|&s| !states_are_apart(o_tree, fs, s))
                    .collect();
                (fs, maps_to)
Bharat Garhewal's avatar
Bharat Garhewal committed
385
            })
386
            .collect::<Vec<_>>();
387
388
389
390
391
392
        for (fs, mut bs_set) in new_front {
            self.frontier_to_basis_map
                .entry(fs)
                .and_modify(|bs_vec| bs_set.drain(..).for_each(|x| bs_vec.push(x)))
                .or_insert_with(|| bs_set.into_iter().collect());
        }
Bharat's avatar
Bharat committed
393
394
    }

395
    /// Checks whether the hypothesis and the observation tree agree.
Bharat Garhewal's avatar
Bharat Garhewal committed
396
    #[must_use]
397
398
399
400
    pub fn check_consistency(&mut self, hypothesis: &Mealy) -> CounterExample {
        let temp = RefCell::borrow(&self.oq_oracle);
        let o_tree = temp.borrow_tree();
        let mut queue = VecDeque::<_>::new();
Bharat Garhewal's avatar
Bharat Garhewal committed
401
402
        queue.push_back((State::new(0), State::new(0)));
        while !queue.is_empty() {
403
            let (q, r) = queue.pop_front().expect("Always safe!");
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
404
            for i in toolbox::inputs_iterator(self.input_size) {
405
406
407
408
409
410
                if let Some(((out_tree, dest_tree), (dest_hyp, out_hyp))) = o_tree
                    .get_out_succ(q, i)
                    .zip(Some(hypothesis.step_from(r, i)))
                {
                    if out_hyp == out_tree {
                        queue.push_back((dest_tree, dest_hyp));
Bharat Garhewal's avatar
Bharat Garhewal committed
411
                    } else {
412
                        let mut inputs = o_tree.get_access_seq(q);
413
                        inputs.push(i);
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
414
                        let outputs = o_tree.get_observation(None, &inputs).expect("Safe");
415
                        return Some((inputs, outputs));
Bharat Garhewal's avatar
Bharat Garhewal committed
416
417
418
419
420
421
                    }
                }
            }
        }
        None
    }
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
422
423

    #[allow(clippy::unused_self)]
424
425
    pub fn get_ads_score(&self) -> f32 {
        0.0
426
    }
Bharat Garhewal's avatar
Bharat Garhewal committed
427

428
429
430
    /// Number of inputs and number of resets
    pub fn get_counts(&self) -> (usize, usize) {
        RefCell::borrow_mut(&self.oq_oracle).get_counts()
Bharat Garhewal's avatar
Bharat Garhewal committed
431
    }
Bharat Garhewal's avatar
Bharat Garhewal committed
432
}
Bharat Garhewal's avatar
Bharat Garhewal committed
433

434
435
436
437
438
fn get_ce_prefix_idx(ce_output: &[OutputSymbol], hyp_output: &[OutputSymbol]) -> usize {
    for (idx, (&ce_out, &hyp_out)) in ce_output.iter().zip(hyp_output.iter()).enumerate() {
        if ce_out != hyp_out {
            return idx;
        }
Bharat Garhewal's avatar
Bharat Garhewal committed
439
    }
440
    unreachable!();
Bharat Garhewal's avatar
Bharat Garhewal committed
441
}