aimds_analysis/
ltl_checker.rs

1//! Linear Temporal Logic (LTL) verification
2//!
3//! Provides LTL formula parsing and basic verification
4
5use crate::errors::AnalysisResult;
6use std::collections::HashMap;
7
8/// LTL formula representation
9#[derive(Debug, Clone, serde::Serialize, serde::Deserialize)]
10pub enum LTLFormula {
11    /// Atomic proposition
12    Atom(String),
13    /// Negation (¬φ)
14    Not(Box<LTLFormula>),
15    /// Conjunction (φ ∧ ψ)
16    And(Box<LTLFormula>, Box<LTLFormula>),
17    /// Disjunction (φ ∨ ψ)
18    Or(Box<LTLFormula>, Box<LTLFormula>),
19    /// Globally (Gφ)
20    Globally(Box<LTLFormula>),
21    /// Finally (Fφ)
22    Finally(Box<LTLFormula>),
23}
24
25impl LTLFormula {
26    /// Parse LTL formula from string (simplified)
27    pub fn parse(s: &str) -> AnalysisResult<Self> {
28        let s = s.trim();
29
30        if let Some(stripped) = s.strip_prefix("G ") {
31            let inner = Self::parse(stripped)?;
32            return Ok(LTLFormula::Globally(Box::new(inner)));
33        }
34
35        if let Some(stripped) = s.strip_prefix("F ") {
36            let inner = Self::parse(stripped)?;
37            return Ok(LTLFormula::Finally(Box::new(inner)));
38        }
39
40        // Atomic proposition
41        Ok(LTLFormula::Atom(s.to_string()))
42    }
43}
44
45/// Execution trace for LTL verification
46#[derive(Debug, Clone)]
47pub struct Trace {
48    /// Sequence of propositions
49    pub propositions: Vec<HashMap<String, bool>>,
50}
51
52impl Trace {
53    /// Create new empty trace
54    pub fn new() -> Self {
55        Self {
56            propositions: Vec::new(),
57        }
58    }
59
60    /// Add state to trace
61    pub fn add_state(&mut self, props: HashMap<String, bool>) {
62        self.propositions.push(props);
63    }
64
65    /// Get length of trace
66    pub fn len(&self) -> usize {
67        self.propositions.len()
68    }
69
70    /// Check if trace is empty
71    pub fn is_empty(&self) -> bool {
72        self.propositions.is_empty()
73    }
74}
75
76impl Default for Trace {
77    fn default() -> Self {
78        Self::new()
79    }
80}
81
82/// LTL model checker
83pub struct LTLChecker {
84    #[allow(dead_code)]
85    max_depth: usize,
86}
87
88impl LTLChecker {
89    /// Create new LTL checker
90    pub fn new() -> Self {
91        Self {
92            max_depth: 100,
93        }
94    }
95
96    /// Check if formula holds on trace
97    pub fn check_formula(&self, formula: &LTLFormula, trace: &Trace) -> bool {
98        if trace.is_empty() {
99            return false;
100        }
101
102        self.check_at_position(formula, trace, 0)
103    }
104
105    #[allow(clippy::only_used_in_recursion)]
106    fn check_at_position(&self, formula: &LTLFormula, trace: &Trace, pos: usize) -> bool {
107        if pos >= trace.len() {
108            return false;
109        }
110
111        match formula {
112            LTLFormula::Atom(prop) => {
113                trace.propositions[pos].get(prop).copied().unwrap_or(false)
114            }
115            LTLFormula::Not(f) => {
116                !self.check_at_position(f, trace, pos)
117            }
118            LTLFormula::And(l, r) => {
119                self.check_at_position(l, trace, pos) && self.check_at_position(r, trace, pos)
120            }
121            LTLFormula::Or(l, r) => {
122                self.check_at_position(l, trace, pos) || self.check_at_position(r, trace, pos)
123            }
124            LTLFormula::Globally(f) => {
125                (pos..trace.len()).all(|i| self.check_at_position(f, trace, i))
126            }
127            LTLFormula::Finally(f) => {
128                (pos..trace.len()).any(|i| self.check_at_position(f, trace, i))
129            }
130        }
131    }
132
133    /// Generate counterexample if formula doesn't hold
134    pub fn generate_counterexample(&self, formula: &LTLFormula, trace: &Trace) -> Option<Trace> {
135        if self.check_formula(formula, trace) {
136            return None;
137        }
138
139        // Return minimal counterexample
140        let mut counterexample = Trace::new();
141
142        for i in 0..trace.len() {
143            counterexample.add_state(trace.propositions[i].clone());
144
145            if !self.check_formula(formula, &counterexample) {
146                return Some(counterexample);
147            }
148        }
149
150        Some(trace.clone())
151    }
152}
153
154impl Default for LTLChecker {
155    fn default() -> Self {
156        Self::new()
157    }
158}
159
160#[cfg(test)]
161mod tests {
162    use super::*;
163
164    #[test]
165    fn test_parse_globally() {
166        let formula = LTLFormula::parse("G authenticated").unwrap();
167        assert!(matches!(formula, LTLFormula::Globally(_)));
168    }
169
170    #[test]
171    fn test_check_atom() {
172        let checker = LTLChecker::new();
173        let mut trace = Trace::new();
174
175        let mut props = HashMap::new();
176        props.insert("authenticated".to_string(), true);
177        trace.add_state(props);
178
179        let formula = LTLFormula::Atom("authenticated".to_string());
180        assert!(checker.check_formula(&formula, &trace));
181    }
182}
aimds_analysis/ltl_checker.rs

aimds_analysis/
ltl_checker.rs
