ceetle/model/
tl_syntax.rs

1use std::fmt;
2
3/// # `CTLFormula`
4/// `CTLFormula` represents a Computional Tree Logic formula that is used to verify models. 
5/// It will almost always be easier to generate `CTLFormula`s using the `ctl` macro.
6pub enum CTLFormula<T: PartialEq> {
7    True,
8    False,
9    Atom(T),
10    And(Box<CTLFormula<T>>, Box<CTLFormula<T>>),
11    Or(Box<CTLFormula<T>>, Box<CTLFormula<T>>),
12    Not(Box<CTLFormula<T>>),
13    Imply(Box<CTLFormula<T>>, Box<CTLFormula<T>>),
14    AG(Box<CTLFormula<T>>),
15    AF(Box<CTLFormula<T>>),
16    AX(Box<CTLFormula<T>>),
17    AU(Box<CTLFormula<T>>, Box<CTLFormula<T>>),
18    EG(Box<CTLFormula<T>>),
19    EF(Box<CTLFormula<T>>),
20    EX(Box<CTLFormula<T>>),
21    EU(Box<CTLFormula<T>>, Box<CTLFormula<T>>),
22}
23
24// Formatting for println!("{}")
25impl<T: fmt::Display + PartialEq> fmt::Display for CTLFormula<T> {
26    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
27        match self {
28            Self::True => {
29                write!(f, "⊤")
30            }
31            Self::False => {
32                write!(f, "⊥")
33            }
34            Self::Atom(value) => {
35                write!(f, "{}", value)
36            }
37            Self::And(value, value2) => {
38                write!(f, "({}∧{})", value, value2)
39            }
40            Self::Or(value, value2) => {
41                write!(f, "({}∨{})", value, value2)
42            }
43            Self::Not(value) => {
44                write!(f, "¬{}", value)
45            }
46            Self::Imply(value, value2) => {
47                write!(f, "({}→{})", value, value2)
48            }
49            Self::AG(value) => {
50                write!(f, "AG{}", value)
51            }
52            Self::AF(value) => {
53                write!(f, "AF{}", value)
54            }
55            Self::AX(value) => {
56                write!(f, "AX{}", value)
57            }
58            Self::AU(value, value2) => {
59                write!(f, "A[{} U {}]", value, value2)
60            }
61            Self::EG(value) => {
62                write!(f, "EG{}", value)
63            }
64            Self::EF(value) => {
65                write!(f, "EF{}", value)
66            }
67            Self::EX(value) => {
68                write!(f, "EX{}", value)
69            }
70            Self::EU(value, value2) => {
71                write!(f, "E[{} U {}]", value, value2)
72            }
73        }
74    }
75}
ceetle/model/tl_syntax.rs

ceetle/model/
tl_syntax.rs
