smt_str/automata/
comp.rs

1//! Complementation of an automaton.
2//! The complement of an automaton is an automaton that recognizes precisely those strings that are not recognized by the original automaton.
3
4use crate::alphabet::{Alphabet, CharRange};
5
6use super::{det::determinize, TransitionType, NFA};
7
8/// Compute the complement of an NFA.
9/// The resulting NFA accepts all string that are not accepted by the input NFA and rejects all strings that are accepted by the input NFA.
10/// This is achieved by swapping the final and non-final states of the input automaton.
11/// This requires that the automaton is deterministic. If the input automaton is not deterministic, it will be determinized first.
12/// If the the input automaton is already deterministic, the algorithm takes O(n) time, where n is the number of states in the automaton.
13/// If the input automaton is not deterministic, the algorithm takes another O(2^n) time for determinization, where n is the number of states in the automaton.
14pub fn complement(nfa: &NFA) -> NFA {
15    let mut det = if !nfa.is_det() {
16        determinize(nfa)
17    } else {
18        nfa.clone()
19    };
20
21    if det.is_empty() {
22        return NFA::universal();
23    }
24
25    // Additionally, we need to add a new sink that we transition to when the dfa reaches a dead end.
26    let sink = det.new_state();
27    det.add_transition(sink, sink, TransitionType::Range(CharRange::all()))
28        .unwrap(); // Cycle on all characters
29
30    // For each state, compute the alphabet of character for which no move is possible.
31    // Then add a transition to the sink for all of these characters.
32    for state in det.states() {
33        let mut alph = Alphabet::default();
34        for t in det.transitions_from(state).unwrap() {
35            match t.get_type() {
36                &TransitionType::Range(r) => alph.insert(r),
37                &TransitionType::NotRange(r) => {
38                    r.complement().into_iter().for_each(|r| alph.insert(r))
39                }
40                TransitionType::Epsilon => unreachable!("DFA cannot have epsilon transitions"),
41            }
42        }
43        // Complement the alphabet to get the alphabet of characters for which no move is possible.
44        let comp = alph.complement();
45        for r in comp.iter_ranges() {
46            det.add_transition(state, sink, TransitionType::Range(r))
47                .unwrap();
48        }
49    }
50
51    det.finals = det.states().filter(|s| !det.finals.contains(s)).collect();
52    det.trim()
53}
54
55#[cfg(test)]
56mod tests {
57    use super::*;
58
59    #[test]
60    fn test_complement_basic() {
61        let mut nfa = NFA::new();
62        let q0 = nfa.new_state();
63        let q1 = nfa.new_state();
64
65        nfa.set_initial(q0).unwrap();
66        nfa.add_final(q1).unwrap();
67
68        nfa.add_transition(q0, q1, TransitionType::Range(CharRange::new('a', 'a')))
69            .unwrap();
70
71        let complement_dfa = complement(&nfa);
72
73        assert!(!complement_dfa.accepts(&"a".into())); // Previously accepted, now rejected
74        assert!(complement_dfa.accepts(&"b".into())); // Previously rejected, now accepted
75        assert!(complement_dfa.accepts(&"z".into())); // Anything except "a" should be accepted
76    }
77
78    #[test]
79    fn test_complement_handles_determinization() {
80        let mut nfa = NFA::new();
81        let q0 = nfa.new_state();
82        let q1 = nfa.new_state();
83        let q2 = nfa.new_state();
84
85        nfa.set_initial(q0).unwrap();
86        nfa.add_final(q2).unwrap();
87
88        // Non-deterministic transitions
89        nfa.add_transition(q0, q1, TransitionType::Range(CharRange::new('a', 'a')))
90            .unwrap();
91        nfa.add_transition(q0, q2, TransitionType::Range(CharRange::new('a', 'a')))
92            .unwrap();
93
94        let complement_dfa = complement(&nfa);
95
96        assert!(!complement_dfa.accepts(&"a".into())); // "a" was accepted in the original
97        assert!(complement_dfa.accepts(&"b".into())); // Previously rejected
98    }
99
100    #[test]
101    fn test_complement_universal_automaton() {
102        let nfa = NFA::universal();
103
104        let complement_dfa = complement(&nfa).trim();
105        assert_eq!(complement_dfa.num_states(), 0); // Complement of a universal automaton should be empty
106    }
107
108    #[test]
109    fn test_complement_empty_automaton() {
110        let nfa = NFA::new(); // Empty automaton
111
112        let complement_dfa = complement(&nfa);
113
114        assert!(complement_dfa.num_states() == 1); // Should only have the sink state
115        assert!(complement_dfa.accepts(&"x".into())); // Everything should be accepted
116    }
117
118    #[test]
119    fn test_complement_handles_sink_correctly() {
120        let mut nfa = NFA::new();
121        let q0 = nfa.new_state();
122        let q1 = nfa.new_state();
123
124        nfa.set_initial(q0).unwrap();
125        nfa.add_final(q1).unwrap();
126
127        nfa.add_transition(q0, q1, TransitionType::Range(CharRange::new('x', 'x')))
128            .unwrap();
129
130        let complement_dfa = complement(&nfa);
131
132        assert!(!complement_dfa.accepts(&"x".into())); // "x" should now be rejected
133        assert!(complement_dfa.accepts(&"y".into())); // Anything except "x" should be accepted
134    }
135
136    #[test]
137    fn test_complement_multiple_transitions() {
138        let mut nfa = NFA::new();
139        let q0 = nfa.new_state();
140        let q1 = nfa.new_state();
141        let q2 = nfa.new_state();
142
143        nfa.set_initial(q0).unwrap();
144        nfa.add_final(q2).unwrap();
145
146        nfa.add_transition(q0, q1, TransitionType::Range(CharRange::new('a', 'c')))
147            .unwrap();
148        nfa.add_transition(q1, q2, TransitionType::Range(CharRange::new('d', 'f')))
149            .unwrap();
150
151        let complement_dfa = complement(&nfa);
152
153        assert!(!complement_dfa.accepts(&"ad".into())); // Previously accepted
154        assert!(complement_dfa.accepts(&"az".into())); // Previously rejected
155        assert!(complement_dfa.accepts(&"bq".into())); // Previously rejected
156    }
157}
smt_str/automata/comp.rs

smt_str/automata/
comp.rs
