modality_lang/
model_checker.rs

1use serde::{Serialize, Deserialize};
2use crate::ast::{Model, Graph, Transition, Property, PropertySign, Formula, FormulaExpr};
3
4/// Represents a state in the model (graph name and node name)
5#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
6pub struct State {
7    pub graph_name: String,
8    pub node_name: String,
9}
10
11/// Represents the result of model checking
12#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
13pub struct ModelCheckResult {
14    pub formula: Formula,
15    pub satisfying_states: Vec<State>,
16    pub is_satisfied: bool,
17}
18
19/// Model checker for temporal modal formulas
20pub struct ModelChecker {
21    model: Model,
22}
23
24impl ModelChecker {
25    /// Create a new model checker for the given model
26    pub fn new(model: Model) -> Self {
27        Self { model }
28    }
29
30    /// Check if a formula is satisfied by the model (requires at least one state from each graph)
31    pub fn check_formula(&self, formula: &Formula) -> ModelCheckResult {
32        let satisfying_states = self.evaluate_formula(&formula.expression);
33        
34        // Check if at least one state from each graph satisfies the formula
35        let is_satisfied = self.check_satisfaction_per_graph(&satisfying_states);
36        
37        ModelCheckResult {
38            formula: formula.clone(),
39            satisfying_states: satisfying_states.clone(),
40            is_satisfied,
41        }
42    }
43
44    /// Check if any state satisfies the formula (original behavior)
45    pub fn check_formula_any_state(&self, formula: &Formula) -> ModelCheckResult {
46        let satisfying_states = self.evaluate_formula(&formula.expression);
47        
48        ModelCheckResult {
49            formula: formula.clone(),
50            satisfying_states: satisfying_states.clone(),
51            is_satisfied: !satisfying_states.is_empty(),
52        }
53    }
54
55    /// Check if at least one state from each graph satisfies the formula
56    fn check_satisfaction_per_graph(&self, satisfying_states: &[State]) -> bool {
57        // Get all graph names from the model
58        let model_graphs: std::collections::HashSet<String> = self.model.graphs
59            .iter()
60            .map(|g| g.name.clone())
61            .collect();
62        
63        // Get graph names from states that satisfy the formula
64        let satisfying_graphs: std::collections::HashSet<String> = satisfying_states
65            .iter()
66            .map(|s| s.graph_name.clone())
67            .collect();
68        
69        // Check if all graphs in the model have at least one satisfying state
70        model_graphs.is_subset(&satisfying_graphs)
71    }
72
73    /// Evaluate a formula expression and return all satisfying states
74    fn evaluate_formula(&self, expr: &FormulaExpr) -> Vec<State> {
75        match expr {
76            FormulaExpr::True => {
77                // Current states satisfy true
78                self.current_states()
79            }
80            FormulaExpr::False => {
81                // No states satisfy false
82                Vec::new()
83            }
84            FormulaExpr::And(left, right) => {
85                let left_states = self.evaluate_formula(left);
86                let right_states = self.evaluate_formula(right);
87                self.intersect_states(&left_states, &right_states)
88            }
89            FormulaExpr::Or(left, right) => {
90                let left_states = self.evaluate_formula(left);
91                let right_states = self.evaluate_formula(right);
92                self.union_states(&left_states, &right_states)
93            }
94            FormulaExpr::Not(expr) => {
95                let expr_states = self.evaluate_formula(expr);
96                let current_states = self.current_states();
97                self.difference_states(&current_states, &expr_states)
98            }
99            FormulaExpr::Paren(expr) => {
100                self.evaluate_formula(expr)
101            }
102            FormulaExpr::Diamond(properties, expr) => {
103                self.evaluate_diamond(properties, expr)
104            }
105            FormulaExpr::Box(properties, expr) => {
106                self.evaluate_box(properties, expr)
107            }
108        }
109    }
110
111    /// Evaluate diamond operator: <properties> phi
112    fn evaluate_diamond(&self, properties: &[Property], expr: &FormulaExpr) -> Vec<State> {
113        let target_states = self.evaluate_formula(expr);
114        let mut result = Vec::new();
115
116        for graph in &self.model.graphs {
117            for transition in &graph.transitions {
118                // Check if this transition has all the required properties
119                if self.transition_satisfies_properties(transition, properties) {
120                    // Check if the target state satisfies the inner formula
121                    let from_state = State {
122                        graph_name: graph.name.clone(),
123                        node_name: transition.from.clone(),
124                    };
125                    
126                    let to_state = State {
127                        graph_name: graph.name.clone(),
128                        node_name: transition.to.clone(),
129                    };
130
131                    // If the target state satisfies the formula, then the source state satisfies <properties> phi
132                    if target_states.contains(&to_state) {
133                        result.push(from_state);
134                    }
135                }
136            }
137        }
138
139        result
140    }
141
142    /// Evaluate box operator: [properties] phi
143    fn evaluate_box(&self, properties: &[Property], expr: &FormulaExpr) -> Vec<State> {
144        let target_states = self.evaluate_formula(expr);
145        let mut result = Vec::new();
146
147        for graph in &self.model.graphs {
148            for node in self.get_nodes_in_graph(graph) {
149                let state = State {
150                    graph_name: graph.name.clone(),
151                    node_name: node.clone(),
152                };
153
154                // Check if ALL transitions from this state with all the properties lead to states satisfying phi
155                let transitions_with_properties = self.get_transitions_from_node(graph, &node)
156                    .into_iter()
157                    .filter(|t| self.transition_satisfies_properties(t, properties))
158                    .collect::<Vec<_>>();
159
160                if transitions_with_properties.is_empty() {
161                    // No transitions with these properties, so vacuously true
162                    result.push(state);
163                } else {
164                    // Check if all target states satisfy the formula
165                    let all_targets_satisfy = transitions_with_properties.iter().all(|t| {
166                        let target_state = State {
167                            graph_name: graph.name.clone(),
168                            node_name: t.to.clone(),
169                        };
170                        target_states.contains(&target_state)
171                    });
172
173                    if all_targets_satisfy {
174                        result.push(state);
175                    }
176                }
177            }
178        }
179
180        result
181    }
182
183    /// Check if a transition satisfies a property
184    fn transition_satisfies_property(&self, transition: &Transition, property: &Property) -> bool {
185        transition.properties.iter().any(|p| p == property)
186    }
187
188    /// Check if a transition satisfies all properties in a list
189    /// A transition satisfies a property if:
190    /// - For +property: transition explicitly has +property OR doesn't mention property at all
191    /// - For -property: transition explicitly has -property OR doesn't mention property at all
192    fn transition_satisfies_properties(&self, transition: &Transition, properties: &[Property]) -> bool {
193        properties.iter().all(|property| {
194            // Check if transition explicitly has this property
195            let has_explicit = transition.properties.iter().any(|p| p == property);
196            if has_explicit {
197                return true;
198            }
199            
200            // If transition doesn't mention this property at all, it's usable
201            let property_name = &property.name;
202            let mentions_property = transition.properties.iter().any(|p| p.name == *property_name);
203            !mentions_property
204        })
205    }
206
207    /// Get all nodes in a graph
208    fn get_nodes_in_graph(&self, graph: &Graph) -> Vec<String> {
209        let mut nodes = std::collections::HashSet::new();
210        for transition in &graph.transitions {
211            nodes.insert(transition.from.clone());
212            nodes.insert(transition.to.clone());
213        }
214        nodes.into_iter().collect()
215    }
216
217    /// Get all transitions from a specific node in a graph
218    fn get_transitions_from_node<'a>(&self, graph: &'a Graph, node: &str) -> Vec<&'a Transition> {
219        graph.transitions.iter()
220            .filter(|t| t.from == node)
221            .collect()
222    }
223
224    /// Get all states in the model
225    fn all_states(&self) -> Vec<State> {
226        let mut states = Vec::new();
227        for graph in &self.model.graphs {
228            for node in self.get_nodes_in_graph(graph) {
229                states.push(State {
230                    graph_name: graph.name.clone(),
231                    node_name: node,
232                });
233            }
234        }
235        states
236    }
237
238    /// Get current possible states (if state information is available)
239    fn current_states(&self) -> Vec<State> {
240        if let Some(state_info) = &self.model.state {
241            let mut states = Vec::new();
242            for graph_state in state_info {
243                for node in &graph_state.current_nodes {
244                    states.push(State {
245                        graph_name: graph_state.graph_name.clone(),
246                        node_name: node.clone(),
247                    });
248                }
249            }
250            states
251        } else {
252            // If no state information, return all states
253            self.all_states()
254        }
255    }
256
257    /// Intersect two sets of states
258    fn intersect_states(&self, states1: &[State], states2: &[State]) -> Vec<State> {
259        states1.iter()
260            .filter(|s1| states2.contains(s1))
261            .cloned()
262            .collect()
263    }
264
265    /// Union two sets of states
266    fn union_states(&self, states1: &[State], states2: &[State]) -> Vec<State> {
267        let mut result = states1.to_vec();
268        for state in states2 {
269            if !result.contains(state) {
270                result.push(state.clone());
271            }
272        }
273        result
274    }
275
276    /// Difference of two sets of states (states1 - states2)
277    fn difference_states(&self, states1: &[State], states2: &[State]) -> Vec<State> {
278        states1.iter()
279            .filter(|s| !states2.contains(s))
280            .cloned()
281            .collect()
282    }
283}
284
285#[cfg(test)]
286mod tests {
287    use super::*;
288    use crate::ast::{Model, Graph, Transition, Property, PropertySign, Formula, FormulaExpr};
289
290    fn create_test_model() -> Model {
291        let mut model = Model::new("TestModel".to_string());
292        
293        let mut graph1 = Graph::new("g1".to_string());
294        graph1.add_transition(Transition::new("n1".to_string(), "n2".to_string()));
295        let mut t1 = Transition::new("n1".to_string(), "n2".to_string());
296        t1.add_property(Property::new(PropertySign::Plus, "blue".to_string()));
297        graph1.add_transition(t1);
298        
299        let mut t2 = Transition::new("n2".to_string(), "n3".to_string());
300        t2.add_property(Property::new(PropertySign::Plus, "blue".to_string()));
301        graph1.add_transition(t2);
302        
303        model.add_graph(graph1);
304        model
305    }
306
307    #[test]
308    fn test_evaluate_true() {
309        let model = create_test_model();
310        let checker = ModelChecker::new(model);
311        let formula = Formula::new("True".to_string(), FormulaExpr::True);
312        
313        let result = checker.check_formula(&formula);
314        assert!(result.is_satisfied);
315        assert_eq!(result.satisfying_states.len(), 3); // n1, n2, n3
316    }
317
318    #[test]
319    fn test_evaluate_false() {
320        let model = create_test_model();
321        let checker = ModelChecker::new(model);
322        let formula = Formula::new("False".to_string(), FormulaExpr::False);
323        
324        let result = checker.check_formula(&formula);
325        assert!(!result.is_satisfied);
326        assert_eq!(result.satisfying_states.len(), 0);
327    }
328
329    #[test]
330    fn test_evaluate_diamond() {
331        let model = create_test_model();
332        let checker = ModelChecker::new(model);
333        
334        let formula = Formula::new("DiamondBlueTrue".to_string(), 
335            FormulaExpr::Diamond(
336                vec![Property::new(PropertySign::Plus, "blue".to_string())],
337                Box::new(FormulaExpr::True)
338            )
339        );
340        
341        let result = checker.check_formula(&formula);
342        assert!(result.is_satisfied);
343        // n1 should satisfy <+blue> true because it has a transition to n2 with +blue
344        assert!(result.satisfying_states.iter().any(|s| s.node_name == "n1"));
345    }
346}
modality_lang/model_checker.rs

modality_lang/
model_checker.rs
