glushkovizer/automata/inner_automata/
prop.rs

1//! Module for testing the properties of an automaton
2
3use super::{dfs::DFSInfo, door::DoorType, InnerAutomata};
4use std::collections::HashSet;
5use std::hash::Hash;
6
7impl<'a, T, V> InnerAutomata<'a, T, V>
8where
9    T: Eq + Hash + Clone,
10{
11    /// Returns if the automaton is standard
12    pub fn is_standard(&self) -> bool {
13        if let Some(rs) = self.inputs().next() {
14            return rs.as_ref().get_previous().count() == 0;
15        }
16        return false;
17    }
18
19    /// Returns if the automaton is deterministic
20    pub fn is_deterministic(&self) -> bool {
21        self.is_standard() && self.states().all(|rs| rs.get_symbols_out_count() <= 1)
22    }
23
24    /// Returns if the automaton is fully deterministic
25    pub fn is_fully_deterministic(&self) -> bool {
26        self.is_standard() && self.states().all(|rs| rs.get_symbols_out_count() == 1)
27    }
28
29    /// Returns if the automaton is homogeneous
30    pub fn is_homogeneous(&self) -> bool {
31        self.states().all(|rs| rs.get_symbols_in_count() <= 1)
32    }
33
34    /// Returns if the automaton is accessible
35    pub fn is_accessible(&self) -> bool {
36        let mut order = Vec::default();
37        self.inputs().for_each(|rs| order.push(rs.clone()));
38        self.states().for_each(|rs| {
39            if !order.contains(rs) {
40                order.push(rs.clone())
41            }
42        });
43        let DFSInfo {
44            prefix: _,
45            suffix: _,
46            predecessor,
47        } = self.dfs(order, false);
48        let mut res = false;
49        self.states()
50            .try_for_each(|rs| {
51                if predecessor.get(rs).is_none() {
52                    if res {
53                        return Err(());
54                    } else {
55                        res = true;
56                    }
57                }
58                Ok(())
59            })
60            .is_ok()
61    }
62
63    /// Returns if the automaton is coaccessible
64    pub fn is_coaccessible(&self) -> bool {
65        let mut order = Vec::default();
66        self.outputs().for_each(|rs| order.push(rs.clone()));
67        self.states().for_each(|rs| {
68            if !order.contains(rs) {
69                order.push(rs.clone())
70            }
71        });
72        let DFSInfo {
73            prefix: _,
74            suffix: _,
75            predecessor,
76        } = self.dfs(order, true);
77        let mut res = false;
78        self.states()
79            .try_for_each(|rs| {
80                if predecessor.get(rs).is_none() {
81                    if res {
82                        return Err(());
83                    } else {
84                        res = true;
85                    }
86                }
87                Ok(())
88            })
89            .is_ok()
90    }
91
92    /// Returns whether the automaton is strongly connected
93    pub fn is_strongly_connected(&self) -> bool {
94        self.kosaraju().len() <= 1
95    }
96
97    /// Returns whether the automaton is a orbit
98    pub fn is_orbit(&self) -> bool {
99        self.is_strongly_connected()
100            && (self.states_count() != 1
101                || unsafe { self.states().next().unwrap_unchecked() }
102                    .as_ref()
103                    .get_follows()
104                    .any(|(_, set)| set.into_iter().any(|rs| self.states.contains(rs))))
105    }
106
107    /// Returns whether the orbit is stable
108    pub fn is_stable(&self) -> bool {
109        if !self.is_orbit() {
110            return false;
111        }
112        let mut inp = HashSet::new();
113        let mut out = HashSet::new();
114        let door = self.get_door();
115        door.into_iter().for_each(|l| {
116            l.into_iter().for_each(|(rs, dtype)| match dtype {
117                DoorType::None => (),
118                DoorType::In => {
119                    inp.insert(rs);
120                }
121                DoorType::Out => {
122                    out.insert(rs);
123                }
124                DoorType::Both => {
125                    out.insert(rs.clone());
126                    inp.insert(rs);
127                }
128            })
129        });
130
131        out.into_iter().all(|output| {
132            output
133                .as_ref()
134                .get_follows()
135                .any(|(_, set)| set.intersection(&inp).count() != 0)
136        })
137    }
138
139    /// Returns whether the orbit is strongly stable
140    pub fn is_strongly_stable(&self) -> bool
141    where
142        V: Clone + Eq,
143    {
144        if !self.is_orbit() {
145            return false;
146        }
147        let copy = InnerAutomata::clone(self);
148        let mut inp = HashSet::new();
149        let mut out = HashSet::new();
150        let door = copy.get_door();
151        door.into_iter().for_each(|l| {
152            l.into_iter().for_each(|(rs, dtype)| match dtype {
153                DoorType::None => (),
154                DoorType::In => {
155                    inp.insert(rs);
156                }
157                DoorType::Out => {
158                    out.insert(rs);
159                }
160                DoorType::Both => {
161                    out.insert(rs.clone());
162                    inp.insert(rs);
163                }
164            })
165        });
166
167        if !out.iter().all(|output| {
168            output
169                .as_ref()
170                .get_follows()
171                .any(|(_, set)| set.intersection(&inp).count() != 0)
172        }) {
173            return false;
174        }
175
176        out.into_iter().for_each(|output| {
177            output.as_ref().get_follows().for_each(|(symbol, set)| {
178                set.into_iter().for_each(|to| {
179                    if inp.contains(to) {
180                        output.remove_follow(to, symbol);
181                    }
182                });
183            });
184        });
185
186        copy.extract_scc()
187            .into_iter()
188            .filter(|inner| inner.is_orbit())
189            .all(|subinner| subinner.is_strongly_stable())
190    }
191
192    /// Returns whether the orbit is transverse
193    pub fn is_transverse(&self) -> bool {
194        if !self.is_orbit() {
195            return false;
196        }
197        let mut inp = HashSet::new();
198        let mut out = HashSet::new();
199        let mut fin = false;
200        let mut fout = false;
201        let door = self.get_door();
202        door.into_iter()
203            .try_for_each(|l| {
204                l.into_iter().try_for_each(|(rs, dtype)| match dtype {
205                    DoorType::None => Ok(()),
206                    DoorType::In => {
207                        if !fin {
208                            rs.as_ref().get_previous().for_each(|(_, set)| {
209                                set.into_iter().for_each(|rs| {
210                                    inp.insert(rs.clone());
211                                })
212                            });
213                            fin = true;
214                            return Ok(());
215                        }
216                        fin = true;
217                        rs.as_ref().get_previous().try_for_each(|(_, set)| {
218                            set.into_iter().try_for_each(|rs| {
219                                if inp.contains(rs) {
220                                    Ok(())
221                                } else {
222                                    Err(())
223                                }
224                            })
225                        })
226                    }
227                    DoorType::Out => {
228                        if out.is_empty() {
229                            rs.as_ref().get_follows().for_each(|(_, set)| {
230                                set.into_iter().for_each(|rs| {
231                                    out.insert(rs.clone());
232                                })
233                            });
234                            fout = true;
235                            return Ok(());
236                        }
237                        fout = true;
238                        rs.as_ref().get_follows().try_for_each(|(_, set)| {
239                            set.into_iter().try_for_each(|rs| {
240                                if out.contains(rs) {
241                                    Ok(())
242                                } else {
243                                    Err(())
244                                }
245                            })
246                        })
247                    }
248                    DoorType::Both => {
249                        if inp.is_empty() {
250                            rs.as_ref().get_previous().for_each(|(_, set)| {
251                                set.into_iter().for_each(|rs| {
252                                    inp.insert(rs.clone());
253                                })
254                            });
255                            fin = true;
256                            return Ok(());
257                        }
258                        fin = true;
259                        rs.as_ref().get_previous().try_for_each(|(_, set)| {
260                            set.into_iter().try_for_each(|rs| {
261                                if inp.contains(rs) {
262                                    Ok(())
263                                } else {
264                                    Err(())
265                                }
266                            })
267                        })?;
268                        if out.is_empty() {
269                            rs.as_ref().get_follows().for_each(|(_, set)| {
270                                set.into_iter().for_each(|rs| {
271                                    out.insert(rs.clone());
272                                })
273                            });
274                            fout = true;
275                            return Ok(());
276                        }
277                        fout = true;
278                        rs.as_ref().get_follows().try_for_each(|(_, set)| {
279                            set.into_iter().try_for_each(|rs| {
280                                if out.contains(rs) {
281                                    Ok(())
282                                } else {
283                                    Err(())
284                                }
285                            })
286                        })
287                    }
288                })
289            })
290            .is_ok()
291    }
292
293    /// Returns whether the orbit is strongly transverse
294    pub fn is_strongly_transverse(&self) -> bool
295    where
296        V: Clone + Eq,
297    {
298        if !self.is_orbit() {
299            return false;
300        }
301        let copy = InnerAutomata::clone(self);
302        let mut inp = HashSet::new();
303        let mut out = HashSet::new();
304        let mut fin = false;
305        let mut fout = false;
306        let door = copy.get_door();
307        if door
308            .into_iter()
309            .try_for_each(|l| {
310                l.into_iter().try_for_each(|(rs, dtype)| match dtype {
311                    DoorType::None => Ok(()),
312                    DoorType::In => {
313                        if !fin {
314                            rs.as_ref().get_previous().for_each(|(_, set)| {
315                                set.into_iter().for_each(|rs| {
316                                    inp.insert(rs.clone());
317                                })
318                            });
319                            fin = true;
320                            return Ok(());
321                        }
322                        fin = true;
323                        rs.as_ref().get_previous().try_for_each(|(_, set)| {
324                            set.into_iter().try_for_each(|rs| {
325                                if inp.contains(rs) {
326                                    Ok(())
327                                } else {
328                                    Err(())
329                                }
330                            })
331                        })
332                    }
333                    DoorType::Out => {
334                        if out.is_empty() {
335                            rs.as_ref().get_follows().for_each(|(_, set)| {
336                                set.into_iter().for_each(|rs| {
337                                    out.insert(rs.clone());
338                                })
339                            });
340                            fout = true;
341                            return Ok(());
342                        }
343                        fout = true;
344                        rs.as_ref().get_follows().try_for_each(|(_, set)| {
345                            set.into_iter().try_for_each(|rs| {
346                                if out.contains(rs) {
347                                    Ok(())
348                                } else {
349                                    Err(())
350                                }
351                            })
352                        })
353                    }
354                    DoorType::Both => {
355                        if inp.is_empty() {
356                            rs.as_ref().get_previous().for_each(|(_, set)| {
357                                set.into_iter().for_each(|rs| {
358                                    inp.insert(rs.clone());
359                                })
360                            });
361                            fin = true;
362                            return Ok(());
363                        }
364                        fin = true;
365                        rs.as_ref().get_previous().try_for_each(|(_, set)| {
366                            set.into_iter().try_for_each(|rs| {
367                                if inp.contains(rs) {
368                                    Ok(())
369                                } else {
370                                    Err(())
371                                }
372                            })
373                        })?;
374                        if out.is_empty() {
375                            rs.as_ref().get_follows().for_each(|(_, set)| {
376                                set.into_iter().for_each(|rs| {
377                                    out.insert(rs.clone());
378                                })
379                            });
380                            fout = true;
381                            return Ok(());
382                        }
383                        fout = true;
384                        rs.as_ref().get_follows().try_for_each(|(_, set)| {
385                            set.into_iter().try_for_each(|rs| {
386                                if out.contains(rs) {
387                                    Ok(())
388                                } else {
389                                    Err(())
390                                }
391                            })
392                        })
393                    }
394                })
395            })
396            .is_err()
397        {
398            return false;
399        }
400
401        out.into_iter().for_each(|output| {
402            output.as_ref().get_follows().for_each(|(symbol, set)| {
403                set.into_iter().for_each(|to| {
404                    if inp.contains(to) {
405                        output.remove_follow(to, symbol);
406                    }
407                });
408            });
409        });
410
411        copy.extract_scc()
412            .into_iter()
413            .filter(|inner| inner.is_orbit())
414            .all(|subinner| subinner.is_strongly_transverse())
415    }
416}