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

taco_acs_model_checker/error_graph/
spurious_path_checker.rs
