omega_automata/
lib.rs

1//! # Omega Automata
2//! 
3//!This crate implements decision procedures and algorithms on
4//!__omega-automata__. __Omega-automata__ are similar to the better-known finite
5//!automata (NFA/DFA/...) except they operate on *infinite* words. They are
6//!commonly used to model systems that can run for an infinite time, such as most
7//!algorithms, protocols, and more.
8
9//!For example, model checking temporal logic properties (commonly used in formal
10//!hardware verification) can be implemented with an optimal worst-case time
11//!complexity via omega automata.
12
13//!## Features
14
15//!Currently, this crate supports the following:
16
17//!- LTL to VWABW (*very weak alternating Büchi automaton*) translation.
18//!- VWABW to GBW (*generalized Büchi automaton*) translation.
19//!- GBW to NBW (*non-deterministic Büchi automaton*) translation.
20//!- NBW emptiness check.
21
22//!### Checking LTL formula satsifiability
23
24//!1. Construct an LTL formula
25//!2. Convert it to a VWABW $\mathit{AM}$
26//!3. Convert *AM* to a GBW *GM*
27//!4. Convert *GM* to an NWB *NM*
28//!5. Check the emptyness of *NM*: It is non-empty iff. the LTL formula is satisfiable.
29
30//!## Examples
31
32//! Let's start with the LTL formula `φ = (□◇x₁ ∧ ◇x₁) ∧ (◇(x₃ ∧ □x₂))`.
33//! Intuitively, `φ` states that any sequence `w = s₁, s₂, s₃, … ∈ X^ω`
34//! of variable assignments (the structure LTL is interpreted over) must
35//! first have infinite `x₁ ∈ sᵢ` (also pronounced `w` *must have infinitely
36//! often* `x₁`), and second it must eventually reach a position `sₖ` such that
37//! `x₃, x₂ ∈ sₖ` and `x₂ ∈ sⱼ` for all `sⱼ` following `sₖ` (also
38//! pronounced `x₂` must hold from `sₖ`).
39//! 
40//!```
41//!use omega_automata::{ltl::*, automata::{*,abw::*,gbw::*,nbw::*}};
42//!let mut formulas = Formulas::default();
43//!let p = formulas.atom(1);
44//!let r = formulas.atom(2);
45//!let q = formulas.atom(3);
46//!let Gr = formulas.globally(r);
47//!let q_and_Gr = formulas.and(q, Gr);
48//!let Fq_and_Gr = formulas.finally(q_and_Gr);
49//!let Fp = formulas.finally(p);
50//!let GFp = formulas.globally(Fp);
51//!let intermediate = formulas.and(GFp, Fp);
52//!let notp = formulas.neg(p);
53//!let Fnotp = formulas.finally(notp);
54//!let GFnotp = formulas.globally(Fnotp);
55//!let res = formulas.and(intermediate, Fq_and_Gr);
56//!let res = formulas.and(res, GFnotp);
57//!let normalized = formulas.normalize(res);
58//!let automata = ltl_to_abw(formulas.access(normalized));
59//!let gbw = vwabw_to_gbw(&automata);
60//!let nbw = gbw_to_nbw(&gbw);
61//!let sat = is_nonempty(&nbw);
62//!assert!(sat)
63//! ```
64#![allow(dead_code)]
65#![cfg_attr(test, allow(non_snake_case))]
66pub mod automata;
67pub mod ltl;
68
69#[cfg(test)]
70mod tests {
71    use crate::automata::{
72        abw::ltl_to_abw,
73        gbw::vwabw_to_gbw,
74        nbw::{gbw_to_nbw, is_nonempty},
75    };
76
77    use super::*;
78    #[test]
79    fn example_test() {
80        println!("It Works!")
81    }
82
83    #[test]
84    fn test_sat2() {
85        let mut formulas = ltl::Formulas::default();
86        let p = formulas.atom(1);
87        let r = formulas.atom(2);
88        let q = formulas.atom(3);
89        let Gr = formulas.globally(r);
90        let q_and_Gr = formulas.and(q, Gr);
91        let Fq_and_Gr = formulas.finally(q_and_Gr);
92        let Fp = formulas.finally(p);
93        let GFp = formulas.globally(Fp);
94        let intermediate = formulas.and(GFp, Fp);
95        let notp = formulas.neg(p);
96        let Fnotp = formulas.finally(notp);
97        let GFnotp = formulas.globally(Fnotp);
98        let res = formulas.and(intermediate, Fq_and_Gr);
99        let res = formulas.and(res, GFnotp);
100        let normalized = formulas.normalize(res);
101        let automata = ltl_to_abw(formulas.access(normalized));
102        let gbw = vwabw_to_gbw(&automata);
103        let nbw = gbw_to_nbw(&gbw);
104        let sat = is_nonempty(&nbw);
105        assert!(sat)
106    }
107}
omega_automata/lib.rs

omega_automata/
lib.rs
