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, internal_spec::upwards_closed_set::UpwardsClosedSet};
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: UpwardsClosedSet,
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: UpwardsClosedSet, 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,
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: &UpwardsClosedSet,
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,
137        internal_spec::{ErrorSpec, ErrorTarget},
138    };
139    use taco_parser::{ParseTAWithLTL, bymc::ByMCParser};
140    use taco_smt_encoder::SMTSolverBuilder;
141    use taco_threshold_automaton::expressions::Location;
142
143    use crate::{
144        acs_threshold_automaton::{
145            ACSThresholdAutomaton,
146            configuration::{ACSIntervalState, ACSLocState, ACSTAConfig},
147        },
148        error_graph::ErrorGraph,
149    };
150
151    #[test]
152    fn test_small_automaton_empty_err_graph() {
153        let test_spec = "
154            skel test_ta1 {
155                shared var1, var2, var3;
156                parameters n, f;
157                
158                assumptions (1) {
159                    n > 3 * f;
160                    n == 1;
161                }
162
163                locations (2) {
164                    loc1 : [0];
165                    loc2 : [1];
166                    loc3 : [2];
167                }
168
169                inits (1) {
170                    loc1 == n - f;
171                    loc2 == 0;
172                    loc3 == 0;
173                    var1 == 0;
174                    var2 == 0;
175                    var3 == 0;
176                }
177
178                rules (4) {
179                    0: loc1 -> loc2
180                        when(true)
181                        do {};
182                }
183
184                specifications (1) {
185                    test1:
186                        [](loc3 == 0)
187                }
188            }
189          ";
190
191        let (ta, spec) = ByMCParser::new().parse_ta_and_spec(test_spec).unwrap();
192        let ctx = SMTSolverBuilder::default();
193
194        let (spec, _) = ErrorSpec::try_from_eltl(spec.into_iter(), &ctx).unwrap();
195
196        let spec_ta = ErrorSpec::transform_threshold_automaton(ta, spec, &ctx);
197
198        assert_eq!(spec_ta.len(), 1);
199        let (_, spec, ta) = spec_ta.into_iter().next().unwrap();
200
201        let mut ta = IntervalThresholdAutomaton::try_from_general_ta(ta, &ctx, &spec)
202            .expect("Failed to create interval ta");
203        assert_eq!(ta.len(), 1, "Expected one interval automaton to be parsed");
204
205        let ta = ACSThresholdAutomaton::from(ta.pop().unwrap());
206
207        let ErrorTarget::Reach(spec) = spec else {
208            panic!("Test case failed");
209        };
210
211        let e_graph = ErrorGraph::compute_error_graph(spec, ta);
212
213        assert!(
214            e_graph.is_empty(),
215            "Got configs: {:?}",
216            e_graph.initial_leafs
217        );
218    }
219
220    #[test]
221    fn test_small_automaton_chain_finds_init() {
222        let test_spec = "
223            skel test_ta1 {
224                shared var1, var2, var3;
225                parameters n, f;
226                
227                assumptions (1) {
228                    n > 3 * f;
229                    n == 1;
230                }
231
232                locations (2) {
233                    loc1 : [0];
234                    loc2 : [1];
235                    loc3 : [2];
236                    loc4 : [3];
237                    loc5 : [4];
238                }
239
240                inits (1) {
241                    loc1 == n - f;
242                    loc2 == 0;
243                    loc3 == 0;
244                    loc4 == 0;
245                    loc5 == 0;
246                    var1 == 0;
247                    var2 == 0;
248                    var3 == 0;
249                }
250
251                rules (4) {
252                    0: loc1 -> loc2
253                        when(true)
254                        do {};
255                    1: loc2 -> loc3
256                        when(true)
257                        do {};
258                    2: loc3 -> loc4
259                        when(true)
260                        do {};
261                    3: loc4 -> loc5
262                        when(true)
263                        do {};
264                }
265
266                specifications (1) {
267                    test1:
268                        [](loc5 == 0)
269                }
270            }
271          ";
272
273        let (ta, spec) = ByMCParser::new().parse_ta_and_spec(test_spec).unwrap();
274        let ctx = SMTSolverBuilder::default();
275
276        let (spec, _) = ErrorSpec::try_from_eltl(spec.into_iter(), &ctx).unwrap();
277
278        let spec_ta = ErrorSpec::transform_threshold_automaton(ta, spec, &ctx);
279
280        assert_eq!(spec_ta.len(), 1);
281        let (_, spec, ta) = spec_ta.into_iter().next().unwrap();
282
283        let mut ta = IntervalThresholdAutomaton::try_from_general_ta(ta, &ctx, &spec)
284            .expect("Failed to create interval ta");
285        assert_eq!(ta.len(), 1, "Expected one interval automaton to be parsed");
286
287        let ta = ACSThresholdAutomaton::from(ta.pop().unwrap());
288
289        let ErrorTarget::Reach(spec) = spec else {
290            panic!("Test case failed");
291        };
292
293        let e_graph = ErrorGraph::compute_error_graph(spec, ta.clone());
294
295        assert!(!e_graph.is_empty(),);
296
297        let mut expected_loc_state = ACSLocState::new_empty(&ta);
298        expected_loc_state[ta.to_cs_loc(&Location::new("loc1"))] = 1;
299        let expected_interval_state = ACSIntervalState::new_mock_zero(&ta);
300        let expected_config = ACSTAConfig::new_mock(expected_loc_state, expected_interval_state);
301
302        assert!(
303            e_graph
304                .initial_leafs
305                .into_iter()
306                .any(|l| l.borrow().config() == &expected_config)
307        );
308    }
309}
taco_acs_model_checker/error_graph.rs

taco_acs_model_checker/
error_graph.rs
