taco_acs_model_checker/
error_graph.rs

1//! Error Graph
2//!
3//! This module contains the error graph construction based on the counter
4//! system of a threshold automaton. The error graph is computed backwards from
5//! the error states, until no new states are discovered.
6//!
7//! An error graph is said to be "empty" if it does not contain any initial
8//! states, which implies that no error state is reachable from the initial
9//! states.
10//!
11//! If the error graph is not empty, all possible paths need to be checked,
12//! whether an actual non-spurious path exists. Such a path would be a counter
13//! example to the property.
14//!
15//! The core logic for this exploration is implemented in the `node` module.
16
17use std::{cell::RefCell, collections::VecDeque, rc::Rc};
18
19use log::info;
20use taco_model_checker::{ModelCheckerResult, reachability_specification::DisjunctionTargetConfig};
21use taco_smt_encoder::SMTSolver;
22
23use crate::{
24    acs_threshold_automaton::{
25        ACSThresholdAutomaton, configuration::partially_ordered_cfg_map::PartiallyOrderedConfigMap,
26    },
27    error_graph::{node::ErrorGraphNode, spurious_path_checker::SpuriousGraphChecker},
28};
29
30mod edge;
31mod node;
32mod spurious_path_checker;
33
34/// Type alias for references to nodes in the error graph
35///
36/// The error graph is built using [`RefCell`], a type that implements the
37/// internal mutability pattern. [`RefCell`] will check the borrow checker
38/// constraints at runtime, therefore borrows must be done with care!
39type NodeRef = Rc<RefCell<ErrorGraphNode>>;
40
41impl From<ErrorGraphNode> for NodeRef {
42    fn from(value: ErrorGraphNode) -> Self {
43        Rc::new(RefCell::new(value))
44    }
45}
46
47/// Error Graph storing all paths from initial abstract configurations to error
48/// configurations
49pub struct ErrorGraph {
50    /// All nodes that have an initial configuration
51    initial_leafs: Vec<NodeRef>,
52    /// Threshold automaton for which the error graph has been constructed
53    ta: ACSThresholdAutomaton,
54    /// Specification for which the error graph has been constructed
55    spec: DisjunctionTargetConfig,
56}
57
58impl ErrorGraph {
59    /// Compute the error graph of the given specification
60    ///
61    /// Constructing the error graph can be a time and memory heavy operation.
62    pub fn compute_error_graph(spec: DisjunctionTargetConfig, ta: ACSThresholdAutomaton) -> Self {
63        // explore the error path
64        let explored_cfgs = Self::construct_full_error_graph(&spec, &ta);
65
66        // statistics
67        let len_before_init = explored_cfgs.len();
68
69        // Retain only nodes that are initial and their successors
70        let initial_leafs: Vec<NodeRef> = explored_cfgs
71            .get_all_values()
72            .filter(|node| node.borrow().config().is_initial(&ta))
73            .collect();
74
75        let max_error_level = initial_leafs
76            .iter()
77            .map(|n| n.borrow().error_level())
78            .max()
79            .unwrap_or(0);
80
81        info!(
82            "Finished error graph construction for property '{}'. Explored {len_before_init} configurations of which {} are initial and have to be checked for spuriousness (max. error level {max_error_level})",
83            spec.name(),
84            initial_leafs.len(),
85        );
86
87        Self {
88            initial_leafs,
89            ta,
90            spec,
91        }
92    }
93
94    /// Compute the full error graph for the [`ACSThresholdAutomaton`] and the
95    /// given [`DisjunctionTargetConfig`]
96    fn construct_full_error_graph(
97        spec: &DisjunctionTargetConfig,
98        ta: &ACSThresholdAutomaton,
99    ) -> PartiallyOrderedConfigMap<NodeRef> {
100        let mut explored_cfgs = ErrorGraphNode::new_roots_from_spec(spec, ta);
101        let mut unexplored_queue = explored_cfgs.values().cloned().collect::<VecDeque<_>>();
102
103        while let Some(unexplored) = unexplored_queue.pop_front() {
104            ErrorGraphNode::compute_predecessors_and_insert_to_graph(
105                &mut explored_cfgs,
106                &mut unexplored_queue,
107                &unexplored,
108                ta,
109            );
110        }
111
112        explored_cfgs
113    }
114
115    /// Check whether the error graph is empty, i.e. whether no counter example
116    /// exists
117    pub fn is_empty(&self) -> bool {
118        self.initial_leafs.is_empty()
119    }
120
121    /// Check whether a non-spurious counter example exists
122    ///
123    /// This method might not terminate for threshold automata with resets
124    pub fn check_for_non_spurious_counter_example(self, context: SMTSolver) -> ModelCheckerResult {
125        let mut visitor = SpuriousGraphChecker::new(&self.ta, self.spec.clone(), context);
126
127        visitor.find_violation(&self)
128    }
129}
130
131#[cfg(test)]
132mod tests {
133
134    use taco_interval_ta::IntervalThresholdAutomaton;
135    use taco_model_checker::{
136        SpecificationTrait, TATrait, reachability_specification::ReachabilityProperty,
137    };
138    use taco_parser::{ParseTAWithLTL, bymc::ByMCParser};
139    use taco_smt_encoder::SMTSolverBuilder;
140    use taco_threshold_automaton::expressions::Location;
141
142    use crate::{
143        acs_threshold_automaton::{
144            ACSThresholdAutomaton,
145            configuration::{ACSIntervalState, ACSLocState, ACSTAConfig},
146        },
147        error_graph::ErrorGraph,
148    };
149
150    #[test]
151    fn test_small_automaton_empty_err_graph() {
152        let test_spec = "
153            skel test_ta1 {
154                shared var1, var2, var3;
155                parameters n, f;
156                
157                assumptions (1) {
158                    n > 3 * f;
159                    n == 1;
160                }
161
162                locations (2) {
163                    loc1 : [0];
164                    loc2 : [1];
165                    loc3 : [2];
166                }
167
168                inits (1) {
169                    loc1 == n - f;
170                    loc2 == 0;
171                    loc3 == 0;
172                    var1 == 0;
173                    var2 == 0;
174                    var3 == 0;
175                }
176
177                rules (4) {
178                    0: loc1 -> loc2
179                        when(true)
180                        do {};
181                }
182
183                specifications (1) {
184                    test1:
185                        [](loc3 == 0)
186                }
187            }
188          ";
189
190        let (ta, spec) = ByMCParser::new().parse_ta_and_spec(test_spec).unwrap();
191        let ctx = SMTSolverBuilder::default();
192
193        let spec = ReachabilityProperty::try_from_eltl(spec.into_iter(), &ctx).unwrap();
194
195        let spec_ta = ReachabilityProperty::transform_threshold_automaton(ta, spec, &ctx);
196
197        assert_eq!(spec_ta.len(), 1);
198        let (spec, ta) = spec_ta.into_iter().next().unwrap();
199
200        let mut ta = IntervalThresholdAutomaton::try_from_general_ta(ta, &ctx, &spec)
201            .expect("Failed to create interval ta");
202        assert_eq!(ta.len(), 1, "Expected one interval automaton to be parsed");
203
204        let ta = ACSThresholdAutomaton::from(ta.pop().unwrap());
205
206        let e_graph = ErrorGraph::compute_error_graph(spec, ta);
207
208        assert!(
209            e_graph.is_empty(),
210            "Got configs: {:?}",
211            e_graph.initial_leafs
212        );
213    }
214
215    #[test]
216    fn test_small_automaton_chain_finds_init() {
217        let test_spec = "
218            skel test_ta1 {
219                shared var1, var2, var3;
220                parameters n, f;
221                
222                assumptions (1) {
223                    n > 3 * f;
224                    n == 1;
225                }
226
227                locations (2) {
228                    loc1 : [0];
229                    loc2 : [1];
230                    loc3 : [2];
231                    loc4 : [3];
232                    loc5 : [4];
233                }
234
235                inits (1) {
236                    loc1 == n - f;
237                    loc2 == 0;
238                    loc3 == 0;
239                    loc4 == 0;
240                    loc5 == 0;
241                    var1 == 0;
242                    var2 == 0;
243                    var3 == 0;
244                }
245
246                rules (4) {
247                    0: loc1 -> loc2
248                        when(true)
249                        do {};
250                    1: loc2 -> loc3
251                        when(true)
252                        do {};
253                    2: loc3 -> loc4
254                        when(true)
255                        do {};
256                    3: loc4 -> loc5
257                        when(true)
258                        do {};
259                }
260
261                specifications (1) {
262                    test1:
263                        [](loc5 == 0)
264                }
265            }
266          ";
267
268        let (ta, spec) = ByMCParser::new().parse_ta_and_spec(test_spec).unwrap();
269        let ctx = SMTSolverBuilder::default();
270
271        let spec = ReachabilityProperty::try_from_eltl(spec.into_iter(), &ctx).unwrap();
272
273        let spec_ta = ReachabilityProperty::transform_threshold_automaton(ta, spec, &ctx);
274
275        assert_eq!(spec_ta.len(), 1);
276        let (spec, ta) = spec_ta.into_iter().next().unwrap();
277
278        let mut ta = IntervalThresholdAutomaton::try_from_general_ta(ta, &ctx, &spec)
279            .expect("Failed to create interval ta");
280        assert_eq!(ta.len(), 1, "Expected one interval automaton to be parsed");
281
282        let ta = ACSThresholdAutomaton::from(ta.pop().unwrap());
283
284        let e_graph = ErrorGraph::compute_error_graph(spec, ta.clone());
285
286        assert!(!e_graph.is_empty(),);
287
288        let mut expected_loc_state = ACSLocState::new_empty(&ta);
289        expected_loc_state[ta.to_cs_loc(&Location::new("loc1"))] = 1;
290        let expected_interval_state = ACSIntervalState::new_mock_zero(&ta);
291        let expected_config = ACSTAConfig::new_mock(expected_loc_state, expected_interval_state);
292
293        assert!(
294            e_graph
295                .initial_leafs
296                .into_iter()
297                .any(|l| l.borrow().config() == &expected_config)
298        );
299    }
300}
taco_acs_model_checker/error_graph.rs

taco_acs_model_checker/
error_graph.rs
