smt_str/automata/
inter.rs

1//! Computation of the intersection of two NFAs.
2//! The intersection of two NFAs is an NFA that accepts the intersection of the languages accepted by the two NFAs.
3//! The intersection is computed by constructing a product automaton.
4//! The product automaton has a state for each pair of states from the two input automata.
5//! The transitions are constructed by taking the cartesian product of the transitions of the two input automata.
6
7use std::collections::VecDeque;
8
9use indexmap::IndexMap;
10
11use super::{StateId, Transition, TransitionType, NFA};
12
13/// Computes the intersection of two NFAs.
14/// The intersection of two NFAs is an NFA that accepts the intersection of the languages accepted by the two NFAs.
15/// The intersection is computed by constructing a product automaton, which has at most |N| * |M| states, where N and M are the number of states of the input automata.
16pub fn intersect(n: &NFA, m: &NFA) -> NFA {
17    let mut result = NFA::new();
18    // Maps pairs of states from the input automata to the corresponding state in the result automaton.
19    let mut state_map = IndexMap::new();
20    // Queue of pairs of states from the input automata that need to be processed.
21    let mut queue = VecDeque::new();
22
23    // Add the initial state of the product automaton.
24    if let Some((n_start, m_start)) = n.initial().zip(m.initial()) {
25        let start = result.new_state();
26        result.set_initial(start).unwrap(); // this cannot be an error, as the automaton is empty
27        state_map.insert((n_start, m_start), start);
28        queue.push_back((n_start, m_start));
29    }
30
31    // Process the queue.
32    while let Some((n_state, m_state)) = queue.pop_front() {
33        // Add the transitions from the product state to the product states that correspond to the transitions of the input automata.
34        let mapped_state = *state_map.get(&(n_state, m_state)).unwrap();
35        // If both states are final, the product state is final.
36        if n.is_final(n_state) && m.is_final(m_state) {
37            result.add_final(mapped_state).unwrap();
38        }
39        for t1 in n.transitions_from(n_state).unwrap() {
40            for t2 in m.transitions_from(m_state).unwrap() {
41                let intersections = intersect_transitions(n_state, t1, m_state, t2);
42                for (label, (p1, p2)) in intersections {
43                    let new_dest = state_map.entry((p1, p2)).or_insert_with(|| {
44                        let new_state = result.new_state();
45                        queue.push_back((p1, p2));
46                        new_state
47                    });
48                    result
49                        .add_transition(mapped_state, *new_dest, label)
50                        .unwrap();
51                }
52            }
53        }
54    }
55    result.trim()
56}
57
58/// Intersects the two transitions
59///
60/// - q1: the source state of the first transition
61/// - t1: the first transition leaving the source state q1
62/// - q2: the source state of the second transition
63/// - t2: the second transition leaving the source state q2
64///
65/// Return pairs of the type of the intersection and the destination states, given as pairs of state ids in the input automata.
66fn intersect_transitions(
67    q1: StateId,
68    t1: &Transition,
69    q2: StateId,
70    t2: &Transition,
71) -> Vec<(TransitionType, (StateId, StateId))> {
72    let type1 = t1.label;
73    let type2 = t2.label;
74    let p1 = t1.destination;
75    let p2 = t2.destination;
76
77    let mut res = Vec::new();
78
79    match (type1, type2) {
80        (TransitionType::Range(r1), TransitionType::Range(r2)) => {
81            let inter = r1.intersect(&r2);
82            if !inter.is_empty() {
83                res.push((TransitionType::Range(inter), (p1, p2)));
84            }
85        }
86        (TransitionType::Range(r2), TransitionType::NotRange(r))
87        | (TransitionType::NotRange(r), TransitionType::Range(r2)) => {
88            let comp = r.complement();
89            for c in comp {
90                let inter = c.intersect(&r2);
91                if !inter.is_empty() {
92                    res.push((TransitionType::Range(inter), (p1, p2)));
93                }
94            }
95        }
96        (TransitionType::NotRange(r1), TransitionType::NotRange(r2)) => {
97            for r1 in r1.complement() {
98                for r2 in r2.complement() {
99                    let inter = r1.intersect(&r2);
100                    if !inter.is_empty() {
101                        res.push((TransitionType::Range(inter), (p1, p2)));
102                    }
103                }
104            }
105        }
106        (TransitionType::Epsilon, _) => {
107            // We stay in the same state in the second automaton and move to p1 when reading an epsilon.
108            res.push((TransitionType::Epsilon, (p1, q2)));
109        }
110        (_, TransitionType::Epsilon) => {
111            // We stay in the same state in the first automaton and move to p2 when reading an epsilon.
112            res.push((TransitionType::Epsilon, (q1, p2)));
113        }
114    };
115    res
116}
117
118#[cfg(test)]
119mod tests {
120
121    use quickcheck_macros::quickcheck;
122
123    use crate::alphabet::CharRange;
124
125    use super::*;
126
127    #[test]
128    fn test_intersect_transitions_disjoint() {
129        let q1 = 0;
130        let q2 = 1;
131        let p1 = 2;
132        let p2 = 3;
133        let t1 = Transition::new(TransitionType::Range(CharRange::new('a', 'c')), p1);
134        let t2 = Transition::new(TransitionType::Range(CharRange::new('d', 'e')), p2);
135
136        let res = intersect_transitions(q1, &t1, q2, &t2);
137        assert_eq!(res.len(), 0);
138    }
139
140    #[test]
141    fn test_intersect_transitions_overlap() {
142        let q1 = 0;
143        let q2 = 1;
144        let p1 = 2;
145        let p2 = 3;
146        let t1 = Transition::new(TransitionType::Range(CharRange::new('a', 'g')), p1);
147        let t2 = Transition::new(TransitionType::Range(CharRange::new('d', 'k')), p2);
148
149        let res = intersect_transitions(q1, &t1, q2, &t2);
150        assert_eq!(res.len(), 1);
151        assert_eq!(res[0].0, TransitionType::Range(CharRange::new('d', 'g')));
152    }
153
154    #[test]
155    fn test_intersect_transitions_equal() {
156        let q1 = 0;
157        let q2 = 1;
158        let p1 = 2;
159        let p2 = 3;
160        let t1 = Transition::new(TransitionType::Range(CharRange::new('a', 'g')), p1);
161        let t2 = Transition::new(TransitionType::Range(CharRange::new('a', 'g')), p2);
162
163        let res = intersect_transitions(q1, &t1, q2, &t2);
164        assert_eq!(res.len(), 1);
165        assert_eq!(res[0].0, TransitionType::Range(CharRange::new('a', 'g')));
166    }
167
168    #[quickcheck]
169    fn test_intersect_transitions_ranges(r1: CharRange, r2: CharRange) {
170        let q1 = 0;
171        let q2 = 1;
172        let p1 = 2;
173        let p2 = 3;
174        let t1 = Transition::new(TransitionType::Range(r1), p1);
175        let t2 = Transition::new(TransitionType::Range(r2), p2);
176
177        let res = intersect_transitions(q1, &t1, q2, &t2);
178        if r1.intersect(&r2).is_empty() {
179            assert_eq!(res.len(), 0);
180        } else {
181            assert_eq!(res.len(), 1);
182            assert_eq!(res[0].0, TransitionType::Range(r1.intersect(&r2)));
183            assert_eq!(res[0].1, (p1, p2));
184        }
185    }
186
187    #[test]
188    fn test_intersect_transitions_epsilon() {
189        let q1 = 0;
190        let q2 = 1;
191        let p1 = 2;
192        let p2 = 3;
193        let t1 = Transition::new(TransitionType::Epsilon, p1);
194        let t2 = Transition::new(TransitionType::Range(CharRange::new('a', 'z')), p2);
195
196        let res = intersect_transitions(q1, &t1, q2, &t2);
197        assert_eq!(res.len(), 1);
198        assert_eq!(res[0].0, TransitionType::Epsilon);
199        assert_eq!(res[0].1, (p1, q2));
200    }
201
202    #[test]
203    fn test_intersect_empty() {
204        let a1: NFA = NFA::new();
205        let a2: NFA = NFA::new();
206        let result = intersect(&a1, &a2);
207        assert_eq!(result.states.len(), 0);
208        assert!(result.initial.is_none());
209        assert_eq!(result.finals.len(), 0);
210    }
211
212    #[test]
213    fn test_intersection_simple() {
214        let mut nfa1 = NFA::new();
215        let q0 = nfa1.new_state();
216        let q1 = nfa1.new_state();
217        nfa1.set_initial(q0).unwrap();
218        nfa1.add_final(q1).unwrap();
219        nfa1.add_transition(q0, q1, TransitionType::Range(CharRange::new('a', 'b')))
220            .unwrap();
221
222        let mut nfa2 = NFA::new();
223        let p0 = nfa2.new_state();
224        let p1 = nfa2.new_state();
225        nfa2.set_initial(p0).unwrap();
226        nfa2.add_final(p1).unwrap();
227        nfa2.add_transition(p0, p1, TransitionType::Range(CharRange::new('b', 'c')))
228            .unwrap();
229
230        let result = intersect(&nfa1, &nfa2);
231
232        assert!(result.accepts(&"b".into()));
233        assert!(!result.accepts(&"a".into()));
234        assert!(!result.accepts(&"c".into()));
235    }
236
237    #[test]
238    fn test_intersection_epsilon() {
239        let mut nfa1 = NFA::new();
240        let q0 = nfa1.new_state();
241        let q1 = nfa1.new_state();
242        nfa1.set_initial(q0).unwrap();
243        nfa1.add_final(q1).unwrap();
244        nfa1.add_transition(q0, q1, TransitionType::Epsilon)
245            .unwrap();
246
247        let mut nfa2 = NFA::new();
248        let p0 = nfa2.new_state();
249        let p1 = nfa2.new_state();
250        nfa2.set_initial(p0).unwrap();
251        nfa2.add_final(p1).unwrap();
252        nfa2.add_transition(p0, p1, TransitionType::Range(CharRange::new('a', 'z')))
253            .unwrap();
254
255        let result = intersect(&nfa1, &nfa2);
256
257        assert!(!result.accepts(&"a".into()));
258        assert!(!result.accepts(&"".into()));
259    }
260
261    #[test]
262    fn test_intersection_negated_range() {
263        let mut nfa1 = NFA::new();
264        let q0 = nfa1.new_state();
265        let q1 = nfa1.new_state();
266        nfa1.set_initial(q0).unwrap();
267        nfa1.add_final(q1).unwrap();
268        nfa1.add_transition(q0, q1, TransitionType::NotRange(CharRange::new('a', 'z')))
269            .unwrap();
270
271        let mut nfa2 = NFA::new();
272        let p0 = nfa2.new_state();
273        let p1 = nfa2.new_state();
274        nfa2.set_initial(p0).unwrap();
275        nfa2.add_final(p1).unwrap();
276        nfa2.add_transition(p0, p1, TransitionType::Range(CharRange::new('0', '9')))
277            .unwrap();
278
279        let result = intersect(&nfa1, &nfa2);
280
281        assert!(result.accepts(&"0".into()));
282        assert!(result.accepts(&"9".into()));
283        assert!(!result.accepts(&"a".into()));
284        assert!(!result.accepts(&"z".into()));
285    }
286
287    #[test]
288    fn test_intersection_disjoint() {
289        let mut nfa1 = NFA::new();
290        let q0 = nfa1.new_state();
291        let q1 = nfa1.new_state();
292        nfa1.set_initial(q0).unwrap();
293        nfa1.add_final(q1).unwrap();
294        nfa1.add_transition(q0, q1, TransitionType::Range(CharRange::new('a', 'b')))
295            .unwrap();
296
297        let mut nfa2 = NFA::new();
298        let p0 = nfa2.new_state();
299        let p1 = nfa2.new_state();
300        nfa2.set_initial(p0).unwrap();
301        nfa2.add_final(p1).unwrap();
302        nfa2.add_transition(p0, p1, TransitionType::Range(CharRange::new('c', 'd')))
303            .unwrap();
304
305        let result = intersect(&nfa1, &nfa2);
306
307        assert!(!result.accepts(&"a".into()));
308        assert!(!result.accepts(&"b".into()));
309        assert!(!result.accepts(&"c".into()));
310        assert!(!result.accepts(&"d".into()));
311    }
312
313    #[test]
314    fn test_intersection_multiple_steps() {
315        let mut nfa1 = NFA::new();
316        let q0 = nfa1.new_state();
317        let q1 = nfa1.new_state();
318        let q2 = nfa1.new_state();
319        nfa1.set_initial(q0).unwrap();
320        nfa1.add_final(q2).unwrap();
321        nfa1.add_transition(q0, q1, TransitionType::Range(CharRange::new('a', 'a')))
322            .unwrap();
323        nfa1.add_transition(q1, q2, TransitionType::Range(CharRange::new('b', 'b')))
324            .unwrap();
325
326        let mut nfa2 = NFA::new();
327        let p0 = nfa2.new_state();
328        let p1 = nfa2.new_state();
329        let p2 = nfa2.new_state();
330        nfa2.set_initial(p0).unwrap();
331        nfa2.add_final(p2).unwrap();
332        nfa2.add_transition(p0, p1, TransitionType::Range(CharRange::new('a', 'a')))
333            .unwrap();
334        nfa2.add_transition(p1, p2, TransitionType::Range(CharRange::new('b', 'b')))
335            .unwrap();
336
337        let result = intersect(&nfa1, &nfa2);
338
339        assert!(result.accepts(&"ab".into()));
340        assert!(!result.accepts(&"a".into()));
341        assert!(!result.accepts(&"b".into()));
342        assert!(!result.accepts(&"ba".into()));
343    }
344}
smt_str/automata/inter.rs

smt_str/automata/
inter.rs
