soucha.rs 9.26 KB
Newer Older
1
use super::equivalence_trait::{CounterExample, EquivalenceOracle, ExternalEquivalenceOracle};
2
3
4
use crate::{
    automatadefs::{
        mealy::{InputSymbol, Mealy, OutputSymbol},
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
5
        traits::{FiniteStateMachine, ObservationTree},
6
7
    },
    oracles::membership::Oracle as OQOracle,
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
8
    util::{learning_config::EqOracle, toolbox, writers::overall as MealyWriter},
9
10
11
};
use fnv::FnvHashMap;
use itertools::Itertools;
12
use rayon::iter::{IntoParallelIterator, ParallelIterator};
13
14
15
16
17
18
19
20
use std::{
    cell::RefCell,
    fmt::Display,
    io::{BufRead, BufReader, Write},
    process::{Child, Command, Stdio},
    rc::Rc,
};

21
#[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Copy)]
22
pub enum Method {
23
    H,
24
25
26
    HSI,
    SPY,
    SPYH,
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
    Unused,
}

impl From<EqOracle> for Method {
    fn from(a: EqOracle) -> Self {
        match a {
            EqOracle::SouchaH => Self::H,
            EqOracle::SouchaHSI => Self::HSI,
            EqOracle::SouchaSPY => Self::SPY,
            EqOracle::SouchaSPYH => Self::SPYH,
            _ => Self::Unused,
        }
    }
}

#[derive(
    Debug, PartialEq, Eq, PartialOrd, Ord, derive_builder::Builder, derive_getters::Getters,
)]
pub struct Config {
    #[builder(default = "Method::HSI")]
    /// Which FSMLib CTT should we use?
    method: Method,
    lookahead: usize,
    #[builder(setter(into))]
    exec_loc: String,
52
53
54
55
56
57
58
59
60
}

impl Display for Method {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Method::HSI => write!(f, "hsi"),
            Method::SPY => write!(f, "spy"),
            Method::SPYH => write!(f, "spyh"),
            Method::H => write!(f, "h"),
61
            Method::Unused => write!(f, "unused"),
62
63
64
65
66
67
        }
    }
}

pub struct SouchaOracle<'a, Tree> {
    oq_oracle: Rc<RefCell<OQOracle<'a, Tree>>>,
68
    _executable_loc: String,
69
70
    rev_input_map: FnvHashMap<InputSymbol, String>,
    rev_output_map: FnvHashMap<OutputSymbol, String>,
71
72
    _lookahead: usize,
    config: Config,
73
74
75
76
77
78
79
80
}

impl<'a, T> ExternalEquivalenceOracle<'a, T> for SouchaOracle<'a, T>
where
    T: ObservationTree + Sync + Send,
{
    fn new(
        _output_oracle: Rc<RefCell<OQOracle<'a, T>>>,
81
        _config: Config,
82
        _lookahead: usize,
83
84
85
86
87
88
89
90
91
        _random_seed: u64,
        _rev_input_map: FnvHashMap<InputSymbol, String>,
        _rev_output_map: FnvHashMap<OutputSymbol, String>,
    ) -> Self {
        unimplemented!("Do not call")
    }

    fn with_location(
        output_oracle: Rc<RefCell<OQOracle<'a, T>>>,
92
93
        config: Config,
        _location: String,
94
        _lookahead: usize,
95
96
97
98
99
100
        _random_seed: u64,
        rev_input_map: FnvHashMap<InputSymbol, String>,
        rev_output_map: FnvHashMap<OutputSymbol, String>,
    ) -> Self {
        Self {
            oq_oracle: output_oracle,
101
            _executable_loc: _location,
102
103
            rev_input_map,
            rev_output_map,
104
            _lookahead,
105
            config,
106
107
108
109
        }
    }
}

110
impl<'a, T: ObservationTree + Send + Sync> SouchaOracle<'a, T> {
111
112
    fn soucha_process(&self) -> Child {
        let fsmlib_path = std::fs::canonicalize(self.config.exec_loc().clone()).expect("Safe");
113
        Command::new(fsmlib_path)
114
115
116
117
118
119
120
            // .args(&["-m", "hsi", "-es", self.lookahead.to_string().as_str()])
            .args(&[
                "-m",
                self.config.method().to_string().as_str(),
                "-es",
                self.config.lookahead().to_string().as_str(),
            ])
121
122
123
124
125
126
            .stdin(Stdio::piped())
            .stdout(Stdio::piped())
            .stderr(Stdio::piped())
            .spawn()
            .unwrap()
    }
127

128
129
130
131
132
133
134
    fn read_into_buffer(
        child_out: &mut BufReader<&mut std::process::ChildStdout>,
        buffer_size: usize,
        ret: &mut Vec<Vec<InputSymbol>>,
    ) {
        let mut string_vec = Vec::with_capacity(buffer_size);
        let mut i = 0;
135
        loop {
136
            let mut strline = String::new();
137
138
139
140
141
            let done = child_out.read_line(&mut strline).unwrap();
            if done == 0 && i != 0 {
                // There should be at least one test-case provided
                break;
            }
142
143
144
            if strline.is_empty() {
                continue;
            }
145
            // print!("{}", strline);
146
147
148
            string_vec.push(strline);
            i += 1;
        }
149

150
        // Format: tc_{id} i1, i2, i3,...,iN\n
151
        let input_vec: Vec<Vec<_>> = string_vec
152
            .into_par_iter()
153
154
155
156
157
158
159
160
            .map(|line| {
                let mut split_iter = line.split_ascii_whitespace();
                let _ = split_iter.next();
                split_iter
                    .next()
                    .expect("Test case did not have an input sequence?")
                    .to_string()
            })
161
162
            .map(|line| {
                line.split(',')
163
                    .map(|x| x.parse::<u16>().expect("Safe"))
164
                    .map(InputSymbol::from)
165
166
                    .collect_vec()
            })
167
            .collect();
168

169
170
171
172
173
174
175
176
177
178
179
180
181
182
        for x in input_vec {
            ret.push(x);
        }
    }
    /// Specialised case for when the hypothesis is a single-state FSM.
    #[must_use]
    fn find_counterexample_initial(&mut self, hyp: &Mealy) -> CounterExample {
        // When the hypothesis has size one, there's no point in testing A.C,
        // as we will have no characterising set.
        // A similar argument works for A.I.C, as C is empty.
        // A will contain only the empty sequence,
        // since we are already in the initial state;
        // Therefore, the only thing left is I<=(n+1)
        let input_size = hyp.input_alphabet().len();
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
183
        let input_alphabet = toolbox::inputs_iterator(input_size).collect_vec();
184
        let lookahead_range = (0..=self.config.lookahead() + 1).into_iter().collect_vec();
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
        let infix_closure = || {
            Iterator::flatten(lookahead_range.iter().map(|&n| {
                itertools::repeat_n(input_alphabet.iter().copied(), n as _)
                    .multi_cartesian_product()
            }))
        };
        for input_seq in infix_closure() {
            if let Some(x) = self.run_test(hyp, &input_seq) {
                return Some(x);
            }
        }
        None
    }

    /// Run a single test sequence and return whether it is a CE or not.
    #[inline]
    #[must_use]
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
202
    fn run_test(&mut self, hyp: &Mealy, input_seq: &[InputSymbol]) -> CounterExample {
203
204
205
206
207
        let hyp_output = hyp.trace(input_seq).1.to_vec();
        let sut_output = RefCell::borrow_mut(&self.oq_oracle).output_query(input_seq);
        if hyp_output == sut_output {
            return None;
        }
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
208
        Some((input_seq.to_vec(), sut_output))
209
210
211
212
213
214
215
    }
}

impl<'a, T> EquivalenceOracle<'a, T> for SouchaOracle<'a, T>
where
    T: ObservationTree + Sync + Send,
{
216
    type Options = Config;
217
    fn get_counts(&mut self) -> (usize, usize) {
218
        RefCell::borrow_mut(&self.oq_oracle).get_counts()
219
220
    }

221
222
223
    fn find_counterexample(&mut self, hypothesis: &Mealy) -> CounterExample {
        let method = *self.config.method();
        if hypothesis.states().len() == 1 && (method == Method::H || method == Method::HSI) {
224
225
            return Self::find_counterexample_initial(self, hypothesis);
        }
226
227
228
229
230
231
232
233
234
235
236
237
        let write_config = MealyWriter::WriteConfigBuilder::default()
            .format(MealyWriter::MealyEncoding::Soucha)
            .file_name(None)
            .build()
            .expect("Safe");
        let byte_hyp = MealyWriter::write_machine(
            write_config,
            hypothesis,
            &self.rev_input_map,
            &self.rev_output_map,
        )
        .expect("Safe");
238
        let mut fsmlib_proc = self.soucha_process();
239
        let child_stdin = fsmlib_proc.stdin.as_mut().unwrap();
240
        // println!("Hyp:\n{:?}", String::from_utf8_lossy(&byte_hyp));
241
242
243
244
245
246
247
248
        child_stdin
            .write_all(&byte_hyp)
            .expect("Failed to write hypothesis model to fsmlib program!");
        child_stdin
            .flush()
            .expect("Failed to write hypothesis model to fsmlib program!");
        let _child_stderr = fsmlib_proc.stderr.as_mut().unwrap();
        let mut child_out = BufReader::new(fsmlib_proc.stdout.as_mut().unwrap());
249
        // let start = Instant::now();
250
251
252
253
        let mut oracle_mut_borrow = RefCell::borrow_mut(&self.oq_oracle);
        let mut buffer = Vec::new();
        loop {
            Self::read_into_buffer(&mut child_out, 10000, &mut buffer);
254
255
256
            if buffer.is_empty() {
                return None;
            }
257
258
259
260
261
262
263
264
            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 {
                    fsmlib_proc
                        .kill()
                        .expect("Could not manage to kill H-ADS process.");
                    let ce_input = input_vec.clone();
Bharat Garhewal's avatar
Cleanup    
Bharat Garhewal committed
265
266
                    let ce_output = sut_output;
                    let ret = Some((ce_input, ce_output));
267
268
269
270
271
272
273
                    return ret;
                }
            }
            buffer.clear();
        }
    }

274
275
276
277
278
    fn find_counterexample_with_lookahead(
        &mut self,
        _hypothesis: &Mealy,
        _lookahead: usize,
    ) -> CounterExample {
279
280
281
282
283
        unimplemented!(
            "FSMLib Equivalence Oracles must always have an `es' (extra_state) parameter."
        )
    }
}