taco_acs_model_checker/error_graph/
spurious_path_checker.rs

1//! Check an error graph for non spurious paths
2
3use log::debug;
4use std::{
5    collections::{HashMap, HashSet},
6    ops::Deref,
7    rc::Rc,
8};
9use taco_display_utils::join_iterator;
10use taco_model_checker::ModelCheckerResult;
11use taco_model_checker::reachability_specification::DisjunctionTargetConfig;
12use taco_smt_encoder::SMTSolverContext;
13use taco_smt_encoder::expression_encoding::EncodeToSMT;
14use taco_smt_encoder::expression_encoding::ctx_mgr::SMTConfigMgr;
15use taco_smt_encoder::expression_encoding::step_ctx::LazyStepContext;
16use taco_smt_encoder::{
17    SMTSolver,
18    expression_encoding::{
19        DeclaresVariable,
20        config_ctx::ConfigCtx,
21        ta_encoding::{encode_initial_constraints, encode_resilience_condition},
22    },
23};
24use taco_threshold_automaton::ThresholdAutomaton;
25
26use crate::acs_threshold_automaton::configuration::ACSTAConfig;
27use crate::{
28    acs_threshold_automaton::ACSThresholdAutomaton,
29    error_graph::{ErrorGraph, NodeRef},
30};
31
32/// Compact type alias for step contexts in this module
33type StepCtx = LazyStepContext<ACSThresholdAutomaton, ConfigCtx>;
34
35pub struct SpuriousGraphChecker {
36    solver: SMTSolver,
37    spec: DisjunctionTargetConfig,
38    cs_ta: Rc<ACSThresholdAutomaton>,
39    ctx_mgr: SMTConfigMgr<StepCtx, ConfigCtx>,
40}
41
42impl SpuriousGraphChecker {
43    pub fn new(
44        ta: &ACSThresholdAutomaton,
45        spec: DisjunctionTargetConfig,
46        mut solver: SMTSolver,
47    ) -> Self {
48        let params = Rc::new(
49            ta.parameters()
50                .map(|p| {
51                    let expr = p
52                        .declare_variable(&mut solver, 0)
53                        .expect("Failed to declare parameter SMT variables");
54                    solver
55                        .assert(solver.gte(expr, solver.numeral(0)))
56                        .expect("Failed to assert param gt 0");
57
58                    (p.clone(), expr)
59                })
60                .collect::<HashMap<_, _>>(),
61        );
62
63        let ctx = ConfigCtx::new(&mut solver, ta, params.clone(), 0);
64
65        // Encode the resilience conditions
66        let rc = encode_resilience_condition(ta, &solver, &ctx);
67        solver
68            .assert(rc)
69            .expect("Failed to assert resilience condition");
70
71        // Encode the condition on the first variable
72        let init_cond = encode_initial_constraints(ta, &solver, &ctx);
73        solver
74            .assert(init_cond)
75            .expect("Failed to assert initial condition");
76
77        let mut ctx_mgr = SMTConfigMgr::new(params);
78        ctx_mgr.push_cfg(Rc::new(ctx));
79
80        Self {
81            solver,
82            ctx_mgr,
83            spec,
84            cs_ta: Rc::new(ta.clone()),
85        }
86    }
87
88    pub fn find_violation(&mut self, e_graph: &ErrorGraph) -> ModelCheckerResult {
89        debug!(
90            "Error graph exploration of ta '{}' and specification '{}' found the following initial configurations, that can potentially reach the error state: {}",
91            self.cs_ta,
92            self.spec,
93            join_iterator(
94                e_graph
95                    .initial_leafs
96                    .iter()
97                    .map(|n| n.borrow().config().display_compact(&self.cs_ta)),
98                ","
99            )
100        );
101
102        for init_node in e_graph.initial_leafs.iter() {
103            let init_cfg = self.ctx_mgr.configs().next().unwrap().clone();
104
105            let res_check_node = self.explore_node_for_violation(init_node, init_cfg, 1);
106
107            if !res_check_node.is_safe() {
108                return res_check_node;
109            }
110        }
111
112        ModelCheckerResult::SAFE
113    }
114
115    fn explore_node_for_violation(
116        &mut self,
117        node: &NodeRef,
118        prev_cfg_ctx: Rc<ConfigCtx>,
119        index: usize,
120    ) -> ModelCheckerResult {
121        // Push a new frame before encoding the conditions of this node
122        // Should be popped before returning
123        self.solver
124            .push()
125            .expect("Failed to push frame for configuration");
126
127        let cfg_constr = node.borrow().config().encode_config_constraints_to_smt(
128            &self.cs_ta,
129            &self.solver,
130            prev_cfg_ctx.deref(),
131        );
132        self.solver
133            .assert(cfg_constr)
134            .expect("Failed to assert configuration constraints");
135
136        debug!(
137            "Exploring configuration: {}",
138            node.borrow().config().display_compact(&self.cs_ta)
139        );
140
141        // Spurious checks on error nodes will be conducted anyway
142        if node.borrow().error_level() > 0
143            && !self
144                .solver
145                .assert_and_check_expr(self.solver.true_())
146                .expect("Failed to check spurious")
147                .is_sat()
148        {
149            self.solver.pop().expect("Failed to pop frame");
150            debug!("Explored path was spurious");
151            return ModelCheckerResult::SAFE;
152        }
153
154        // Create a new context for the next configuration
155        let cfg_primed_ctx = Rc::new(ConfigCtx::new(
156            &mut self.solver,
157            self.cs_ta.deref(),
158            self.ctx_mgr.params().clone(),
159            index,
160        ));
161        self.ctx_mgr.push_cfg_primed(cfg_primed_ctx.clone());
162
163        // Compute the sequence of rules applicable for a steady path and
164        // the nodes for step transitions
165        let mut visited_nodes_cache = HashSet::<ACSTAConfig>::new();
166        let (s, step_nodes, contains_err_state) =
167            Self::collect_enabled_rules_and_next_nodes(node, &mut visited_nodes_cache);
168        debug!(
169            "Steady step with rules : {}",
170            join_iterator(s.iter().map(|u| format!("'{u}'")), ",")
171        );
172
173        // Encode and assert the steady condition
174        let steady_ctx: LazyStepContext<ACSThresholdAutomaton, ConfigCtx> = self
175            .encode_and_assert_steady_path_with_rules(
176                &s,
177                prev_cfg_ctx,
178                cfg_primed_ctx.clone(),
179                index,
180            );
181        self.ctx_mgr.push_steady(steady_ctx);
182
183        for node in step_nodes {
184            // for each node and an edge to a new interval
185            self.solver.push().expect("Failed to push frame");
186
187            let res = self.explore_next_interval_state_transition(
188                &node,
189                cfg_primed_ctx.clone(),
190                index + 1,
191            );
192            if !res.is_safe() {
193                return res;
194            }
195
196            self.solver.pop().expect("Failed to pop frame");
197        }
198
199        // Currently in error state: Check spuriousness and return result
200        if node.borrow().error_level() == 0 || (contains_err_state) {
201            let res = self.check_spurious_error(&cfg_primed_ctx);
202            if !res.is_safe() {
203                return res;
204            }
205        }
206
207        // current path is safe, remove the contexts assumptions
208        self.solver
209            .pop()
210            .expect("Failed to pop frame for configuration");
211        self.ctx_mgr.pop_steady();
212        self.ctx_mgr.pop_cfg_primed();
213
214        ModelCheckerResult::SAFE
215    }
216
217    fn explore_next_interval_state_transition(
218        &mut self,
219        next_node: &NodeRef,
220        prev_cfg: Rc<ConfigCtx>,
221        index: usize,
222    ) -> ModelCheckerResult {
223        let node = next_node.borrow();
224        let is = node.config().interval_state().clone();
225
226        // Create the variables for the next config
227        let nxt_cfg = Rc::new(ConfigCtx::new(
228            &mut self.solver,
229            self.cs_ta.deref(),
230            self.ctx_mgr.params().clone(),
231            index,
232        ));
233        self.ctx_mgr.push_cfg(nxt_cfg.clone());
234
235        // find outgoing transition (cannot be self-loop)
236        for next_edge in node
237            .parents()
238            .chain(node.back_edges())
239            .filter(|e| e.node().borrow().config().interval_state() != &is)
240        {
241            self.solver.push().expect("Failed to push context");
242
243            debug!(
244                "Exploring step to configuration '{}' using '{}'",
245                next_edge
246                    .node()
247                    .borrow()
248                    .config()
249                    .display_compact(&self.cs_ta),
250                join_iterator(next_edge.get_ids_of_rules(), ",")
251            );
252
253            let cfg_constr = node.config().encode_config_constraints_to_smt(
254                &self.cs_ta,
255                &self.solver,
256                prev_cfg.deref(),
257            );
258            self.solver
259                .assert(cfg_constr)
260                .expect("Failed to assert configuration constraints");
261
262            let rules = next_edge
263                .get_ids_of_rules()
264                .map(|id| {
265                    self.cs_ta
266                        .get_rule_by_id(id)
267                        .expect("Failed to find rule id")
268                })
269                .cloned();
270
271            let step_ctx = LazyStepContext::new(
272                rules,
273                self.cs_ta.clone(),
274                prev_cfg.clone(),
275                nxt_cfg.clone(),
276                index,
277                &mut self.solver,
278            );
279            self.ctx_mgr.push_step(step_ctx.clone());
280
281            let step_constr = step_ctx.encode_phi_step(&self.solver);
282            self.solver
283                .assert(step_constr)
284                .expect("Failed to assert step constraints");
285
286            let res = self.explore_node_for_violation(next_edge.node(), nxt_cfg.clone(), index + 1);
287            if !res.is_safe() {
288                return res;
289            }
290
291            self.solver
292                .pop()
293                .expect("Failed to pop solver context after exploring step");
294            self.ctx_mgr.pop_step();
295        }
296
297        self.ctx_mgr.pop_cfg();
298
299        ModelCheckerResult::SAFE
300    }
301
302    fn encode_and_assert_steady_path_with_rules(
303        &mut self,
304        appl_rules: &HashSet<u32>,
305        prev_cfg: Rc<ConfigCtx>,
306        next_cfg: Rc<ConfigCtx>,
307        index: usize,
308    ) -> StepCtx {
309        let rules_to_appl = appl_rules
310            .iter()
311            .map(|id| {
312                self.cs_ta
313                    .get_rule_by_id(*id)
314                    .expect("Failed to find rule id")
315            })
316            .cloned();
317
318        let step_ctx = LazyStepContext::new(
319            rules_to_appl,
320            self.cs_ta.clone(),
321            prev_cfg,
322            next_cfg,
323            index,
324            &mut self.solver,
325        );
326
327        let steady_path = step_ctx.encode_phi_steady(&self.solver);
328
329        self.solver
330            .assert(steady_path)
331            .expect("Failed to assert steady condition");
332
333        step_ctx
334    }
335
336    /// This function collects the orders in which rules are applicable while
337    /// staying in the same interval state along with the rules that would allow
338    /// to transition out of the interval state.
339    ///
340    /// The first set (`HashSet<u32>`) represents all applicable rules, and the
341    /// second value is a vector of next nodes.
342    /// - The second element (`Vec<NodeRef>`) contains nodes that represent possible transitions out of the current interval state.
343    /// - The third element (`bool`) is true if any of the traversed nodes are in an error state, false otherwise.
344    fn collect_enabled_rules_and_next_nodes(
345        org_node: &NodeRef,
346        visited_nodes: &mut HashSet<ACSTAConfig>,
347    ) -> (HashSet<u32>, Vec<NodeRef>, bool) {
348        let mut next_is = Vec::new();
349        let mut applicable_rules = HashSet::new();
350        let mut s_contains_err_state = false;
351
352        let is = org_node.borrow().config().interval_state().clone();
353        let node = org_node.borrow();
354
355        // add node to visited set
356        visited_nodes.insert(node.config().clone());
357
358        // add self-loops
359        applicable_rules.extend(node.self_loops());
360
361        let mut exists_new_is = false;
362
363        for successor_edge in node.parents().chain(node.back_edges()) {
364            // Resets can enable back edges and cycles
365            if successor_edge.node().borrow().config() == node.config() {
366                applicable_rules.extend(successor_edge.get_ids_of_rules());
367                continue;
368            }
369
370            // if we are remain in the same interval state, add all the rules
371            // of the edge to the possible sequence of rules
372            if successor_edge.node().borrow().config().interval_state() == &is {
373                // Potentially, we are already in an error state
374                if successor_edge.node().borrow().error_level() == 0 {
375                    s_contains_err_state = true;
376                }
377
378                applicable_rules.extend(successor_edge.get_ids_of_rules());
379
380                if !visited_nodes.contains(successor_edge.node().borrow().config()) {
381                    // recursively compute applicable rules
382                    let (s, nxt, suc_s_contains_err_state) =
383                        Self::collect_enabled_rules_and_next_nodes(
384                            successor_edge.node(),
385                            visited_nodes,
386                        );
387                    s_contains_err_state |= suc_s_contains_err_state;
388                    next_is.extend(nxt);
389                    applicable_rules.extend(s);
390                }
391
392                continue;
393            }
394
395            exists_new_is = true;
396        }
397
398        if exists_new_is {
399            next_is.push(org_node.clone());
400        }
401
402        (applicable_rules, next_is, s_contains_err_state)
403    }
404
405    // return true if spurious
406    // removes the current context if spurious
407    fn check_spurious_error(&mut self, ctx: &ConfigCtx) -> ModelCheckerResult {
408        // encode error and check sat
409        self.solver
410            .push()
411            .expect("Failed to push frame for err cond");
412
413        let err_cond = self
414            .spec
415            .encode_to_smt_with_ctx(&self.solver, ctx)
416            .expect("Failed to encode error condition");
417
418        let res = self
419            .solver
420            .assert_and_check_expr(err_cond)
421            .expect("Failed to check spurious");
422
423        if res.is_sat() {
424            let path = self.ctx_mgr.extract_error_path(
425                res,
426                &mut self.solver,
427                self.cs_ta.get_interval_ta().get_ta().clone(),
428            );
429            return ModelCheckerResult::UNSAFE(vec![(
430                self.spec.name().to_string(),
431                Box::new(path),
432            )]);
433        }
434
435        self.solver
436            .pop()
437            .expect("Failed to pop frame for error condition");
438
439        debug!("Checked for error, but error has not been reached.");
440
441        ModelCheckerResult::SAFE
442    }
443}
444
445#[cfg(test)]
446mod tests {
447    use std::collections::HashMap;
448
449    use taco_interval_ta::IntervalThresholdAutomaton;
450    use taco_model_checker::{
451        ModelCheckerResult, TATrait, reachability_specification::TargetConfig,
452    };
453    use taco_parser::{ParseTA, bymc::ByMCParser};
454    use taco_smt_encoder::SMTSolverBuilder;
455    use taco_threshold_automaton::{
456        expressions::{
457            BooleanConnective, BooleanExpression, ComparisonOp, IntegerExpression, Location,
458            Parameter, Variable,
459        },
460        general_threshold_automaton::{Action, UpdateExpression, builder::RuleBuilder},
461        path::{Configuration, PathBuilder, Transition},
462    };
463
464    use crate::{acs_threshold_automaton::ACSThresholdAutomaton, error_graph::ErrorGraph};
465
466    #[test]
467    fn test_initial_error_condition_fullfilled() {
468        let test_spec = "
469            skel test_ta1 {
470                shared var1, var2, var3;
471                parameters n, f;
472                
473                assumptions (1) {
474                    n == 1;
475                }
476
477                locations (2) {
478                    loc1 : [0];
479                    loc2 : [1];
480                    loc3 : [2];
481                }
482
483                inits (1) {
484                    loc1 == 0;
485                    loc2 == n;
486                    loc3 == 0;
487                    var1 == 0;
488                    var2 == 0;
489                    var3 == 0;
490                }
491
492                rules (4) {
493                    0: loc1 -> loc2
494                        when(true)
495                        do {};
496                }
497
498                specifications (1) {
499                    test1:
500                        [](loc2 == 0)
501                }
502            }
503            ";
504
505        let ta = ByMCParser::new().parse_ta(test_spec).unwrap();
506        let solver_builder = SMTSolverBuilder::default();
507
508        let spec = TargetConfig::new_cover([Location::new("loc2")])
509            .unwrap()
510            .into_disjunct_with_name("test");
511
512        let test_tas =
513            IntervalThresholdAutomaton::try_from_general_ta(ta.clone(), &solver_builder, &spec)
514                .unwrap();
515        assert_eq!(test_tas.len(), 1);
516
517        let test_ta = test_tas[0].clone();
518
519        let cs_ta = ACSThresholdAutomaton::from(test_ta);
520
521        let path = PathBuilder::new(ta)
522            .add_parameter_assignment(HashMap::from([
523                (Parameter::new("n"), 1),
524                (Parameter::new("f"), 0),
525            ]))
526            .unwrap()
527            .add_configuration(Configuration::new(
528                HashMap::from([
529                    (Variable::new("var1"), 0),
530                    (Variable::new("var2"), 0),
531                    (Variable::new("var3"), 0),
532                ]),
533                HashMap::from([
534                    (Location::new("loc1"), 0),
535                    (Location::new("loc2"), 1),
536                    (Location::new("loc3"), 0),
537                ]),
538            ))
539            .unwrap()
540            .build()
541            .unwrap();
542
543        let e_graph = ErrorGraph::compute_error_graph(spec, cs_ta);
544        assert!(!e_graph.is_empty());
545
546        let ctx = SMTSolverBuilder::default();
547        let res = e_graph.check_for_non_spurious_counter_example(ctx.new_solver());
548        assert!(!res.is_safe());
549
550        let res = match res {
551            ModelCheckerResult::SAFE => unreachable!("checked above"),
552            ModelCheckerResult::UNSAFE(v) => {
553                assert_eq!(v.len(), 1);
554                *v[0].1.clone()
555            }
556            ModelCheckerResult::UNKNOWN(_) => todo!(),
557        };
558
559        assert_eq!(
560            res,
561            path.clone(),
562            "Got:\n{}\n\nExpected:\n{}\n\n",
563            res,
564            path
565        );
566    }
567
568    #[test]
569    fn test_spec_reach_location_one_rule_one_process_no_guards() {
570        let test_spec = "
571            skel test_ta1 {
572                shared var1, var2, var3;
573                parameters n, f;
574                
575                assumptions (1) {
576                    n == 1;
577                }
578
579                locations (2) {
580                    loc1 : [0];
581                    loc2 : [1];
582                    loc3 : [2];
583                }
584
585                inits (1) {
586                    loc1 == 1;
587                    loc2 == 0;
588                    loc3 == 0;
589                    var1 == 0;
590                    var2 == 0;
591                    var3 == 0;
592                }
593
594                rules (4) {
595                    0: loc1 -> loc2
596                        when(true)
597                        do {};
598                }
599
600                specifications (1) {
601                    test1:
602                        [](loc2 == 0)
603                }
604            }
605            ";
606
607        let ta = ByMCParser::new().parse_ta(test_spec).unwrap();
608        let solver_builder = SMTSolverBuilder::default();
609
610        let spec = TargetConfig::new_cover([Location::new("loc2")])
611            .unwrap()
612            .into_disjunct_with_name("test");
613
614        let test_tas =
615            IntervalThresholdAutomaton::try_from_general_ta(ta.clone(), &solver_builder, &spec)
616                .unwrap();
617        assert_eq!(test_tas.len(), 1);
618
619        let test_ta = test_tas[0].clone();
620
621        let cs_ta = ACSThresholdAutomaton::from(test_ta);
622
623        let path = PathBuilder::new(ta)
624            .add_parameter_assignment(HashMap::from([
625                (Parameter::new("n"), 1),
626                (Parameter::new("f"), 0),
627            ]))
628            .unwrap()
629            .add_configuration(Configuration::new(
630                HashMap::from([
631                    (Variable::new("var1"), 0),
632                    (Variable::new("var2"), 0),
633                    (Variable::new("var3"), 0),
634                ]),
635                HashMap::from([
636                    (Location::new("loc1"), 1),
637                    (Location::new("loc2"), 0),
638                    (Location::new("loc3"), 0),
639                ]),
640            ))
641            .unwrap()
642            .add_transition(Transition::new(
643                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc2")).build(),
644                1,
645            ))
646            .unwrap()
647            .add_configuration(Configuration::new(
648                HashMap::from([
649                    (Variable::new("var1"), 0),
650                    (Variable::new("var2"), 0),
651                    (Variable::new("var3"), 0),
652                ]),
653                HashMap::from([
654                    (Location::new("loc1"), 0),
655                    (Location::new("loc2"), 1),
656                    (Location::new("loc3"), 0),
657                ]),
658            ))
659            .unwrap()
660            .build()
661            .unwrap();
662
663        let e_graph = ErrorGraph::compute_error_graph(spec, cs_ta);
664        assert!(!e_graph.is_empty());
665
666        let ctx = SMTSolverBuilder::default();
667        let res = e_graph.check_for_non_spurious_counter_example(ctx.new_solver());
668        assert!(!res.is_safe());
669
670        let res = match res {
671            ModelCheckerResult::SAFE => unreachable!("checked above"),
672            ModelCheckerResult::UNSAFE(v) => {
673                assert_eq!(v.len(), 1);
674                *v[0].1.clone()
675            }
676            ModelCheckerResult::UNKNOWN(_) => todo!(),
677        };
678
679        assert_eq!(
680            res,
681            path.clone(),
682            "Got:\n{}\n\nExpected:\n{}\n\n",
683            res,
684            path
685        );
686    }
687
688    #[test]
689    fn test_spec_reach_location_one_rule_5_process_no_guards() {
690        let test_spec = "
691            skel test_ta1 {
692                shared var1, var2, var3;
693                parameters n, f;
694                
695                assumptions (1) {
696                    n > 3 * f;
697                    n == 5;
698                    f == 0;
699                }
700
701                locations (2) {
702                    loc1 : [0];
703                    loc2 : [1];
704                    loc3 : [2];
705                }
706
707                inits (1) {
708                    loc1 == n - f;
709                    loc2 == 0;
710                    loc3 == 0;
711                    var1 == 0;
712                    var2 == 0;
713                    var3 == 0;
714                }
715
716                rules (4) {
717                    0: loc1 -> loc2
718                        when(true)
719                        do {};
720                }
721
722                specifications (1) {
723                    test1:
724                        [](loc2 == 0)
725                }
726            }
727            ";
728
729        let ta = ByMCParser::new().parse_ta(test_spec).unwrap();
730        let solver_builder = SMTSolverBuilder::default();
731
732        let spec = TargetConfig::new_general_cover([(Location::new("loc2"), 5)])
733            .unwrap()
734            .into_disjunct_with_name("test");
735
736        let test_tas =
737            IntervalThresholdAutomaton::try_from_general_ta(ta.clone(), &solver_builder, &spec)
738                .unwrap();
739        assert_eq!(test_tas.len(), 1);
740
741        let test_ta = test_tas[0].clone();
742
743        let cs_ta = ACSThresholdAutomaton::from(test_ta);
744
745        let path = PathBuilder::new(ta)
746            .add_parameter_assignment(HashMap::from([
747                (Parameter::new("n"), 5),
748                (Parameter::new("f"), 0),
749            ]))
750            .unwrap()
751            .add_configuration(Configuration::new(
752                HashMap::from([
753                    (Variable::new("var1"), 0),
754                    (Variable::new("var2"), 0),
755                    (Variable::new("var3"), 0),
756                ]),
757                HashMap::from([
758                    (Location::new("loc1"), 5),
759                    (Location::new("loc2"), 0),
760                    (Location::new("loc3"), 0),
761                ]),
762            ))
763            .unwrap()
764            .add_transition(Transition::new(
765                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc2")).build(),
766                5,
767            ))
768            .unwrap()
769            .add_configuration(Configuration::new(
770                HashMap::from([
771                    (Variable::new("var1"), 0),
772                    (Variable::new("var2"), 0),
773                    (Variable::new("var3"), 0),
774                ]),
775                HashMap::from([
776                    (Location::new("loc1"), 0),
777                    (Location::new("loc2"), 5),
778                    (Location::new("loc3"), 0),
779                ]),
780            ))
781            .unwrap()
782            .build()
783            .unwrap();
784        let e_graph = ErrorGraph::compute_error_graph(spec, cs_ta);
785        assert!(!e_graph.is_empty());
786
787        let ctx = SMTSolverBuilder::default();
788        let res = e_graph.check_for_non_spurious_counter_example(ctx.new_solver());
789        assert!(!res.is_safe());
790
791        let res = match res {
792            ModelCheckerResult::SAFE => unreachable!("checked above"),
793            ModelCheckerResult::UNSAFE(v) => {
794                assert_eq!(v.len(), 1);
795                *v[0].1.clone()
796            }
797            ModelCheckerResult::UNKNOWN(_) => todo!(),
798        };
799
800        assert_eq!(
801            res,
802            path.clone(),
803            "Got:\n{}\n\nExpected:\n{}\n\n",
804            res,
805            path
806        );
807    }
808
809    #[test]
810    fn test_spec_unreachable_location_graph() {
811        let test_spec = "
812            skel test_ta1 {
813                shared var1, var2, var3;
814                parameters n, t, f;
815                
816                assumptions (1) {
817                    n > 3 * f;
818                }
819
820                locations (2) {
821                    loc1 : [0];
822                    loc2 : [1];
823                    loc3 : [2];
824                }
825
826                inits (1) {
827                    loc1 == n - f;
828                    loc2 == 0;
829                    loc3 == 0;
830                    var1 == 0;
831                    var2 == 0;
832                    var3 == 0;
833                }
834
835                rules (4) {
836                    0: loc1 -> loc2
837                        when(true)
838                        do {};
839                }
840
841                specifications (1) {
842                    test1:
843                        [](loc3 == 0)
844                }
845            }
846            ";
847
848        let ta = ByMCParser::new().parse_ta(test_spec).unwrap();
849        let solver_builder = SMTSolverBuilder::default();
850
851        let spec = TargetConfig::new_cover([Location::new("loc3")])
852            .unwrap()
853            .into_disjunct_with_name("test");
854
855        let test_tas =
856            IntervalThresholdAutomaton::try_from_general_ta(ta.clone(), &solver_builder, &spec)
857                .unwrap();
858        assert_eq!(test_tas.len(), 1);
859
860        let test_ta = test_tas[0].clone();
861
862        let cs_ta = ACSThresholdAutomaton::from(test_ta);
863
864        let e_graph = ErrorGraph::compute_error_graph(spec, cs_ta);
865        assert!(e_graph.is_empty());
866
867        let ctx = SMTSolverBuilder::default();
868        let res = e_graph.check_for_non_spurious_counter_example(ctx.new_solver());
869        assert!(res.is_safe());
870
871        assert_eq!(res, ModelCheckerResult::SAFE);
872    }
873
874    #[test]
875    fn test_spec_reach_location_two_rules_one_guard() {
876        let test_spec = "
877            skel test_ta1 {
878                shared var1, var2, var3;
879                parameters n, f;
880                
881                assumptions (1) {
882                    n > 3 * f;
883                    n == 5;
884                    f == 0;
885                }
886
887                locations (2) {
888                    loc1 : [0];
889                    loc2 : [1];
890                    loc3 : [2];
891                }
892
893                inits (1) {
894                    loc1 == n - f;
895                    loc2 == 0;
896                    loc3 == 0;
897                    var1 == 0;
898                    var2 == 0;
899                    var3 == 0;
900                }
901
902                rules (4) {
903                    0: loc1 -> loc2
904                        when(var1 >= 4 && var2 <= 0)
905                        do {};
906                    1: loc1 -> loc3
907                        when(true)
908                        do {var1' == var1 + 1};
909                }
910
911                specifications (1) {
912                    test1:
913                        [](loc2 == 0)
914                }
915            }
916            ";
917
918        let ta = ByMCParser::new().parse_ta(test_spec).unwrap();
919        let solver_builder = SMTSolverBuilder::default();
920
921        let spec = TargetConfig::new_cover([Location::new("loc2")])
922            .unwrap()
923            .into_disjunct_with_name("test");
924
925        let test_tas =
926            IntervalThresholdAutomaton::try_from_general_ta(ta.clone(), &solver_builder, &spec)
927                .unwrap();
928        assert_eq!(test_tas.len(), 1);
929
930        let test_ta = test_tas[0].clone();
931
932        let cs_ta = ACSThresholdAutomaton::from(test_ta);
933
934        let path = PathBuilder::new(ta)
935            .add_parameter_assignment(HashMap::from([
936                (Parameter::new("n"), 5),
937                (Parameter::new("f"), 0),
938            ]))
939            .unwrap()
940            .add_configuration(Configuration::new(
941                HashMap::from([
942                    (Variable::new("var1"), 0),
943                    (Variable::new("var2"), 0),
944                    (Variable::new("var3"), 0),
945                ]),
946                HashMap::from([
947                    (Location::new("loc1"), 5),
948                    (Location::new("loc2"), 0),
949                    (Location::new("loc3"), 0),
950                ]),
951            ))
952            .unwrap()
953            .add_transition(Transition::new(
954                RuleBuilder::new(1, Location::new("loc1"), Location::new("loc3"))
955                    .with_action(Action::new_with_update(
956                        Variable::new("var1"),
957                        UpdateExpression::Inc(1),
958                    ))
959                    .build(),
960                1,
961            ))
962            .unwrap()
963            .add_configuration(Configuration::new(
964                HashMap::from([
965                    (Variable::new("var1"), 1),
966                    (Variable::new("var2"), 0),
967                    (Variable::new("var3"), 0),
968                ]),
969                HashMap::from([
970                    (Location::new("loc1"), 4),
971                    (Location::new("loc2"), 0),
972                    (Location::new("loc3"), 1),
973                ]),
974            ))
975            .unwrap()
976            .add_transition(Transition::new(
977                RuleBuilder::new(1, Location::new("loc1"), Location::new("loc3"))
978                    .with_action(Action::new_with_update(
979                        Variable::new("var1"),
980                        UpdateExpression::Inc(1),
981                    ))
982                    .build(),
983                2,
984            ))
985            .unwrap()
986            .add_configuration(Configuration::new(
987                HashMap::from([
988                    (Variable::new("var1"), 3),
989                    (Variable::new("var2"), 0),
990                    (Variable::new("var3"), 0),
991                ]),
992                HashMap::from([
993                    (Location::new("loc1"), 2),
994                    (Location::new("loc2"), 0),
995                    (Location::new("loc3"), 3),
996                ]),
997            ))
998            .unwrap()
999            .add_transition(Transition::new(
1000                RuleBuilder::new(1, Location::new("loc1"), Location::new("loc3"))
1001                    .with_action(Action::new_with_update(
1002                        Variable::new("var1"),
1003                        UpdateExpression::Inc(1),
1004                    ))
1005                    .build(),
1006                1,
1007            ))
1008            .unwrap()
1009            .add_configuration(Configuration::new(
1010                HashMap::from([
1011                    (Variable::new("var1"), 4),
1012                    (Variable::new("var2"), 0),
1013                    (Variable::new("var3"), 0),
1014                ]),
1015                HashMap::from([
1016                    (Location::new("loc1"), 1),
1017                    (Location::new("loc2"), 0),
1018                    (Location::new("loc3"), 4),
1019                ]),
1020            ))
1021            .unwrap()
1022            .add_transition(Transition::new(
1023                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc2"))
1024                    .with_guard(BooleanExpression::BinaryExpression(
1025                        Box::new(BooleanExpression::ComparisonExpression(
1026                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
1027                            ComparisonOp::Geq,
1028                            Box::new(IntegerExpression::Const(4)),
1029                        )),
1030                        BooleanConnective::And,
1031                        Box::new(BooleanExpression::ComparisonExpression(
1032                            Box::new(IntegerExpression::Atom(Variable::new("var2"))),
1033                            ComparisonOp::Leq,
1034                            Box::new(IntegerExpression::Const(0)),
1035                        )),
1036                    ))
1037                    .build(),
1038                1,
1039            ))
1040            .unwrap()
1041            .add_configuration(Configuration::new(
1042                HashMap::from([
1043                    (Variable::new("var1"), 4),
1044                    (Variable::new("var2"), 0),
1045                    (Variable::new("var3"), 0),
1046                ]),
1047                HashMap::from([
1048                    (Location::new("loc1"), 0),
1049                    (Location::new("loc2"), 1),
1050                    (Location::new("loc3"), 4),
1051                ]),
1052            ))
1053            .unwrap()
1054            .build()
1055            .unwrap();
1056
1057        let e_graph = ErrorGraph::compute_error_graph(spec, cs_ta);
1058        assert!(!e_graph.is_empty());
1059
1060        let ctx = SMTSolverBuilder::default();
1061        let res = e_graph.check_for_non_spurious_counter_example(ctx.new_solver());
1062        assert!(!res.is_safe());
1063
1064        let res = match res {
1065            ModelCheckerResult::SAFE => unreachable!("checked above"),
1066            ModelCheckerResult::UNSAFE(v) => {
1067                assert_eq!(v.len(), 1);
1068                *v[0].1.clone()
1069            }
1070            ModelCheckerResult::UNKNOWN(_) => todo!(),
1071        };
1072
1073        assert_eq!(
1074            res,
1075            path.clone(),
1076            "Got:\n{}\n\nExpected:\n{}\n\n",
1077            res,
1078            path
1079        );
1080    }
1081
1082    #[test]
1083    fn test_spec_reach_location_three_rules_one_guard_self_loop() {
1084        let test_spec = "
1085            skel test_ta1 {
1086                shared var1, var2, var3;
1087                parameters n, f;
1088                
1089                assumptions (1) {
1090                    n > 3 * f;
1091                    n == 1;
1092                    f == 0;
1093                }
1094
1095                locations (2) {
1096                    loc1 : [0];
1097                    loc2 : [1];
1098                    loc3 : [2];
1099                }
1100
1101                inits (1) {
1102                    loc1 == n - f;
1103                    loc2 == 0;
1104                    loc3 == 0;
1105                    var1 == 0;
1106                    var2 == 0;
1107                    var3 == 0;
1108                }
1109
1110                rules (4) {
1111                    0: loc1 -> loc1
1112                        when(true)
1113                        do {var1' == var1 + 1};
1114                    1: loc1 -> loc2
1115                        when(true)
1116                        do {};
1117                    2: loc2 -> loc3
1118                        when(var1 > 3 && var2 <= 0 && var1 <= 4)
1119                        do {};
1120                    
1121                }
1122
1123                specifications (1) {
1124                    test1:
1125                        [](loc3 == 0)
1126                }
1127            }
1128            ";
1129
1130        let ta = ByMCParser::new().parse_ta(test_spec).unwrap();
1131        let solver_builder = SMTSolverBuilder::default();
1132
1133        let spec = TargetConfig::new_cover([Location::new("loc3")])
1134            .unwrap()
1135            .into_disjunct_with_name("test");
1136
1137        let test_tas =
1138            IntervalThresholdAutomaton::try_from_general_ta(ta.clone(), &solver_builder, &spec)
1139                .unwrap();
1140        assert_eq!(test_tas.len(), 1);
1141
1142        let test_ta = test_tas[0].clone();
1143
1144        let cs_ta = ACSThresholdAutomaton::from(test_ta);
1145
1146        let path = PathBuilder::new(ta)
1147            .add_parameter_assignment(HashMap::from([
1148                (Parameter::new("n"), 1),
1149                (Parameter::new("f"), 0),
1150            ]))
1151            .unwrap()
1152            .add_configuration(Configuration::new(
1153                HashMap::from([
1154                    (Variable::new("var1"), 0),
1155                    (Variable::new("var2"), 0),
1156                    (Variable::new("var3"), 0),
1157                ]),
1158                HashMap::from([
1159                    (Location::new("loc1"), 1),
1160                    (Location::new("loc2"), 0),
1161                    (Location::new("loc3"), 0),
1162                ]),
1163            ))
1164            .unwrap()
1165            .add_transition(Transition::new(
1166                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc1"))
1167                    .with_action(Action::new_with_update(
1168                        Variable::new("var1"),
1169                        UpdateExpression::Inc(1),
1170                    ))
1171                    .build(),
1172                1,
1173            ))
1174            .unwrap()
1175            .add_configuration(Configuration::new(
1176                HashMap::from([
1177                    (Variable::new("var1"), 1),
1178                    (Variable::new("var2"), 0),
1179                    (Variable::new("var3"), 0),
1180                ]),
1181                HashMap::from([
1182                    (Location::new("loc1"), 1),
1183                    (Location::new("loc2"), 0),
1184                    (Location::new("loc3"), 0),
1185                ]),
1186            ))
1187            .unwrap()
1188            .add_transition(Transition::new(
1189                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc1"))
1190                    .with_action(Action::new_with_update(
1191                        Variable::new("var1"),
1192                        UpdateExpression::Inc(1),
1193                    ))
1194                    .build(),
1195                2,
1196            ))
1197            .unwrap()
1198            .add_configuration(Configuration::new(
1199                HashMap::from([
1200                    (Variable::new("var1"), 3),
1201                    (Variable::new("var2"), 0),
1202                    (Variable::new("var3"), 0),
1203                ]),
1204                HashMap::from([
1205                    (Location::new("loc1"), 1),
1206                    (Location::new("loc2"), 0),
1207                    (Location::new("loc3"), 0),
1208                ]),
1209            ))
1210            .unwrap()
1211            .add_transition(Transition::new(
1212                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc1"))
1213                    .with_action(Action::new_with_update(
1214                        Variable::new("var1"),
1215                        UpdateExpression::Inc(1),
1216                    ))
1217                    .build(),
1218                1,
1219            ))
1220            .unwrap()
1221            .add_configuration(Configuration::new(
1222                HashMap::from([
1223                    (Variable::new("var1"), 4),
1224                    (Variable::new("var2"), 0),
1225                    (Variable::new("var3"), 0),
1226                ]),
1227                HashMap::from([
1228                    (Location::new("loc1"), 1),
1229                    (Location::new("loc2"), 0),
1230                    (Location::new("loc3"), 0),
1231                ]),
1232            ))
1233            .unwrap()
1234            .add_transition(Transition::new(
1235                RuleBuilder::new(1, Location::new("loc1"), Location::new("loc2")).build(),
1236                1,
1237            ))
1238            .unwrap()
1239            .add_configuration(Configuration::new(
1240                HashMap::from([
1241                    (Variable::new("var1"), 4),
1242                    (Variable::new("var2"), 0),
1243                    (Variable::new("var3"), 0),
1244                ]),
1245                HashMap::from([
1246                    (Location::new("loc1"), 0),
1247                    (Location::new("loc2"), 1),
1248                    (Location::new("loc3"), 0),
1249                ]),
1250            ))
1251            .unwrap()
1252            .add_transition(Transition::new(
1253                RuleBuilder::new(2, Location::new("loc2"), Location::new("loc3"))
1254                    .with_guard(
1255                        BooleanExpression::ComparisonExpression(
1256                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
1257                            ComparisonOp::Gt,
1258                            Box::new(IntegerExpression::Const(3)),
1259                        ) & BooleanExpression::ComparisonExpression(
1260                            Box::new(IntegerExpression::Atom(Variable::new("var2"))),
1261                            ComparisonOp::Leq,
1262                            Box::new(IntegerExpression::Const(0)),
1263                        ) & BooleanExpression::ComparisonExpression(
1264                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
1265                            ComparisonOp::Leq,
1266                            Box::new(IntegerExpression::Const(4)),
1267                        ),
1268                    )
1269                    .build(),
1270                1,
1271            ))
1272            .unwrap()
1273            .add_configuration(Configuration::new(
1274                HashMap::from([
1275                    (Variable::new("var1"), 4),
1276                    (Variable::new("var2"), 0),
1277                    (Variable::new("var3"), 0),
1278                ]),
1279                HashMap::from([
1280                    (Location::new("loc1"), 0),
1281                    (Location::new("loc2"), 0),
1282                    (Location::new("loc3"), 1),
1283                ]),
1284            ))
1285            .unwrap()
1286            .build()
1287            .unwrap();
1288
1289        let e_graph = ErrorGraph::compute_error_graph(spec, cs_ta);
1290        assert!(!e_graph.is_empty());
1291
1292        let ctx = SMTSolverBuilder::default();
1293        let res = e_graph.check_for_non_spurious_counter_example(ctx.new_solver());
1294        assert!(!res.is_safe());
1295
1296        let res = match res {
1297            ModelCheckerResult::SAFE => unreachable!("checked above"),
1298            ModelCheckerResult::UNSAFE(v) => {
1299                assert_eq!(v.len(), 1);
1300                *v[0].1.clone()
1301            }
1302            ModelCheckerResult::UNKNOWN(_) => todo!(),
1303        };
1304
1305        assert_eq!(
1306            res,
1307            path.clone(),
1308            "Got:\n{}\n\nExpected:\n{}\n\n",
1309            res,
1310            path
1311        );
1312    }
1313}
taco_acs_model_checker/error_graph/spurious_path_checker.rs

taco_acs_model_checker/error_graph/
spurious_path_checker.rs
