taco_acs_model_checker/
lib.rs

1//! Abstract Counter System Model Checker
2//!
3//! This crate implements a counter system based model checker as described
4//! in the paper
5//! ["Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata"](https://arxiv.org/abs/2406.19880).
6//! This model checker will construct the explicit counter system (`ACS` in the
7//! paper), starting from potential error states and checking whether an initial
8//! state is reachable.
9//! If a path is found, the SMT checker will be used to check whether the path
10//! is spurious.
11//!
12//! Note that this model checker does not support "reachability" specifications,
13//! i.e. specifications, that require a location to be not covered by any
14//! process.
15
16use core::fmt;
17use std::{convert::Infallible, error};
18
19use log::{info, warn};
20use taco_interval_ta::IntervalThresholdAutomaton;
21use taco_model_checker::{
22    ModelChecker, ModelCheckerResult, TASpecOf,
23    internal_spec::{ErrorSpec, ErrorTarget},
24};
25use taco_smt_encoder::SMTSolverBuilder;
26
27use crate::{acs_threshold_automaton::ACSThresholdAutomaton, error_graph::ErrorGraph};
28
29pub mod partial_ord;
30
31pub mod error_graph;
32
33pub mod acs_threshold_automaton;
34
35/// Counter system based model checker
36///
37/// This crate implements a counter system based model checker as described
38/// in the paper
39/// ["Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata"](https://arxiv.org/abs/2406.19880).
40/// This model checker will construct the explicit counter system (`ACS` in the
41/// paper), starting from potential error states and checking whether an initial
42/// state is reachable.
43/// If a path is found, the SMT checker will be used to check whether the path
44/// is spurious.
45///
46/// Note that this model checker does not support "reachability" specifications,
47/// i.e. specifications, that require a location to be not covered by any
48/// process.
49#[derive(Debug, Clone)]
50pub struct ACSModelChecker {
51    /// Threshold automata and specifications to check
52    ta_spec: TASpecOf<Self>,
53    /// Properties that could not be translated
54    unknown: Vec<String>,
55    /// SMT solver builder used for spurious checks
56    ctx: SMTSolverBuilder,
57}
58
59impl ModelChecker for ACSModelChecker {
60    type ModelCheckerContext = SMTSolverBuilder;
61
62    type ModelCheckerOptions = Option<()>;
63
64    type SpecType = ErrorSpec;
65
66    type ThresholdAutomatonType = IntervalThresholdAutomaton;
67
68    type InitializationError = ACSModelCheckerInitializationError;
69
70    type ModelCheckingError = Infallible;
71
72    fn initialize(
73        _mode: Self::ModelCheckerOptions,
74        ta_spec: TASpecOf<Self>,
75        unknown: Vec<String>,
76        ctx: Self::ModelCheckerContext,
77    ) -> Result<Self, Self::InitializationError> {
78        if let Some((_, reach_spec, _)) = ta_spec
79            .iter()
80            .find(|(_, s, _)| s.contains_reachability_constraint())
81        {
82            return Err(ACSModelCheckerInitializationError::ReachabilitySpec(
83                Box::new(reach_spec.clone()),
84            ));
85        }
86
87        Ok(Self {
88            ta_spec,
89            unknown,
90            ctx,
91        })
92    }
93
94    fn verify(
95        self,
96        abort_on_violation: bool,
97    ) -> Result<ModelCheckerResult, Self::ModelCheckingError> {
98        let mut unsafe_properties = Vec::new();
99        let mut unknown_properties = self.unknown;
100
101        for (name, target, tas) in self.ta_spec {
102            let ErrorTarget::Reach(spec) = target else {
103                warn!("Property '{name}' ({target}) is not supported by the ACS model checker");
104                unknown_properties.push(name);
105                continue;
106            };
107
108            for ta in tas.into_iter().map(ACSThresholdAutomaton::new) {
109                let error_graph = ErrorGraph::compute_error_graph(spec.clone(), ta);
110
111                if error_graph.is_empty() {
112                    info!(
113                        "Error graph of property {} is empty, property is SAFE in this interval order.",
114                        spec
115                    );
116                    continue;
117                }
118
119                let solver = self.ctx.new_solver();
120
121                info!(
122                    "Error graph of property {} is not empty, checking paths for spuriousness",
123                    spec
124                );
125                let res = error_graph.check_for_non_spurious_counter_example(solver);
126
127                match res {
128                    ModelCheckerResult::SAFE => info!(
129                        "Error graph of property {} is spurious, property is SAFE in this interval order.",
130                        spec
131                    ),
132                    ModelCheckerResult::UNSAFE { violations, .. } => {
133                        info!("Found counterexample to property {}", name);
134                        unsafe_properties
135                            .extend(violations.into_iter().map(|(_, p)| (name.clone(), p)));
136
137                        if abort_on_violation {
138                            return Ok(ModelCheckerResult::UNSAFE {
139                                violations: unsafe_properties,
140                                unknown: unknown_properties,
141                            });
142                        }
143                    }
144                    ModelCheckerResult::UNKNOWN(_) => {
145                        info!(
146                            "The model checker could not determine whether property {} is safe or unsafe",
147                            spec
148                        );
149                        unknown_properties.push(name.clone());
150                    }
151                }
152            }
153        }
154
155        if !unsafe_properties.is_empty() {
156            return Ok(ModelCheckerResult::UNSAFE {
157                violations: unsafe_properties,
158                unknown: unknown_properties,
159            });
160        }
161        if !unknown_properties.is_empty() {
162            return Ok(ModelCheckerResult::UNKNOWN(unknown_properties));
163        }
164
165        Ok(ModelCheckerResult::SAFE)
166    }
167}
168
169#[derive(Clone, Debug, PartialEq)]
170pub enum ACSModelCheckerInitializationError {
171    ReachabilitySpec(Box<ErrorTarget>),
172}
173
174impl fmt::Display for ACSModelCheckerInitializationError {
175    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
176        match self {
177            ACSModelCheckerInitializationError::ReachabilitySpec(spec) => {
178                write!(
179                    f,
180                    "The counter system model checker does not support reachability specifications, but property {} contains a reachability constraint",
181                    spec
182                )
183            }
184        }
185    }
186}
187
188impl error::Error for ACSModelCheckerInitializationError {}
189
190#[cfg(test)]
191mod tests {
192    use std::collections::HashMap;
193
194    use taco_model_checker::{ModelChecker, ModelCheckerResult, ModelCheckerSetupError};
195    use taco_parser::{ParseTAWithLTL, bymc::ByMCParser};
196    use taco_smt_encoder::SMTSolverBuilderCfg;
197    use taco_threshold_automaton::{
198        expressions::{
199            BooleanExpression, ComparisonOp, IntegerExpression, Location, Parameter, Variable,
200        },
201        general_threshold_automaton::{Action, UpdateExpression, builder::RuleBuilder},
202        path::{Configuration, PathBuilder, Transition},
203    };
204
205    use crate::{ACSModelChecker, ACSModelCheckerInitializationError};
206
207    #[test]
208    fn test_full_model_checker_reach_location_three_rules_one_guard_self_loop() {
209        let test_spec = "
210            skel test_ta1 {
211                shared var1, var2, var3;
212                parameters n, f;
213                
214                assumptions (1) {
215                    n > 3 * f;
216                    n == 1;
217                    f == 0;
218                }
219
220                locations (2) {
221                    loc1 : [0];
222                    loc2 : [1];
223                    loc3 : [2];
224                }
225
226                inits (1) {
227                    loc1 == n - f;
228                    loc2 == 0;
229                    loc3 == 0;
230                    var1 == 0;
231                    var2 == 0;
232                    var3 == 0;
233                }
234
235                rules (4) {
236                    0: loc1 -> loc1
237                        when(true)
238                        do {var1' == var1 + 1};
239                    1: loc1 -> loc2
240                        when(true)
241                        do {};
242                    2: loc2 -> loc3
243                        when(var1 > 3 && var2 <= 0 && var1 <= 4)
244                        do {};
245                    
246                }
247
248                specifications (1) {
249                    test1:
250                        [](loc3 == 0)
251                }
252            }
253            ";
254
255        let (ta, spec) = ByMCParser::new().parse_ta_and_spec(test_spec).unwrap();
256
257        let mc = ACSModelChecker::new(
258            Some(SMTSolverBuilderCfg::new_z3()),
259            None,
260            Vec::new(),
261            ta.clone(),
262            spec.into_iter(),
263        );
264        let mc = mc.unwrap();
265        let res = mc.verify(true).unwrap();
266
267        let path = PathBuilder::new(ta.clone())
268            .add_parameter_assignment(HashMap::from([
269                (Parameter::new("n"), 1),
270                (Parameter::new("f"), 0),
271            ]))
272            .unwrap()
273            .add_configuration(Configuration::new(
274                HashMap::from([
275                    (Variable::new("var1"), 0),
276                    (Variable::new("var2"), 0),
277                    (Variable::new("var3"), 0),
278                ]),
279                HashMap::from([
280                    (Location::new("loc1"), 1),
281                    (Location::new("loc2"), 0),
282                    (Location::new("loc3"), 0),
283                ]),
284            ))
285            .unwrap()
286            .add_transition(Transition::new(
287                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc1"))
288                    .with_action(Action::new_with_update(
289                        Variable::new("var1"),
290                        UpdateExpression::Inc(1),
291                    ))
292                    .build(),
293                1,
294            ))
295            .unwrap()
296            .add_configuration(Configuration::new(
297                HashMap::from([
298                    (Variable::new("var1"), 1),
299                    (Variable::new("var2"), 0),
300                    (Variable::new("var3"), 0),
301                ]),
302                HashMap::from([
303                    (Location::new("loc1"), 1),
304                    (Location::new("loc2"), 0),
305                    (Location::new("loc3"), 0),
306                ]),
307            ))
308            .unwrap()
309            .add_transition(Transition::new(
310                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc1"))
311                    .with_action(Action::new_with_update(
312                        Variable::new("var1"),
313                        UpdateExpression::Inc(1),
314                    ))
315                    .build(),
316                2,
317            ))
318            .unwrap()
319            .add_configuration(Configuration::new(
320                HashMap::from([
321                    (Variable::new("var1"), 3),
322                    (Variable::new("var2"), 0),
323                    (Variable::new("var3"), 0),
324                ]),
325                HashMap::from([
326                    (Location::new("loc1"), 1),
327                    (Location::new("loc2"), 0),
328                    (Location::new("loc3"), 0),
329                ]),
330            ))
331            .unwrap()
332            .add_transition(Transition::new(
333                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc1"))
334                    .with_action(Action::new_with_update(
335                        Variable::new("var1"),
336                        UpdateExpression::Inc(1),
337                    ))
338                    .build(),
339                1,
340            ))
341            .unwrap()
342            .add_configuration(Configuration::new(
343                HashMap::from([
344                    (Variable::new("var1"), 4),
345                    (Variable::new("var2"), 0),
346                    (Variable::new("var3"), 0),
347                ]),
348                HashMap::from([
349                    (Location::new("loc1"), 1),
350                    (Location::new("loc2"), 0),
351                    (Location::new("loc3"), 0),
352                ]),
353            ))
354            .unwrap()
355            .add_transition(Transition::new(
356                RuleBuilder::new(1, Location::new("loc1"), Location::new("loc2")).build(),
357                1,
358            ))
359            .unwrap()
360            .add_configuration(Configuration::new(
361                HashMap::from([
362                    (Variable::new("var1"), 4),
363                    (Variable::new("var2"), 0),
364                    (Variable::new("var3"), 0),
365                ]),
366                HashMap::from([
367                    (Location::new("loc1"), 0),
368                    (Location::new("loc2"), 1),
369                    (Location::new("loc3"), 0),
370                ]),
371            ))
372            .unwrap()
373            .add_transition(Transition::new(
374                RuleBuilder::new(2, Location::new("loc2"), Location::new("loc3"))
375                    .with_guard(
376                        BooleanExpression::ComparisonExpression(
377                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
378                            ComparisonOp::Gt,
379                            Box::new(IntegerExpression::Const(3)),
380                        ) & BooleanExpression::ComparisonExpression(
381                            Box::new(IntegerExpression::Atom(Variable::new("var2"))),
382                            ComparisonOp::Leq,
383                            Box::new(IntegerExpression::Const(0)),
384                        ) & BooleanExpression::ComparisonExpression(
385                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
386                            ComparisonOp::Leq,
387                            Box::new(IntegerExpression::Const(4)),
388                        ),
389                    )
390                    .build(),
391                1,
392            ))
393            .unwrap()
394            .add_configuration(Configuration::new(
395                HashMap::from([
396                    (Variable::new("var1"), 4),
397                    (Variable::new("var2"), 0),
398                    (Variable::new("var3"), 0),
399                ]),
400                HashMap::from([
401                    (Location::new("loc1"), 0),
402                    (Location::new("loc2"), 0),
403                    (Location::new("loc3"), 1),
404                ]),
405            ))
406            .unwrap()
407            .build()
408            .unwrap();
409
410        let res = match res {
411            ModelCheckerResult::SAFE => {
412                unreachable!("Expected UNSAFE result based on test specification")
413            }
414            ModelCheckerResult::UNSAFE { violations: v, .. } => {
415                assert_eq!(v.len(), 1);
416                *v[0].1.clone()
417            }
418            ModelCheckerResult::UNKNOWN(_) => todo!(),
419        };
420
421        assert_eq!(
422            res,
423            path.clone(),
424            "Got:\n{}\n\nExpected:\n{}\n\n",
425            res,
426            path
427        );
428    }
429
430    #[test]
431    fn test_full_model_checker_reach_location_three_rules_one_guard_self_loop_with_var_constr() {
432        let test_spec = "
433            skel test_ta1 {
434                shared var1, var2, var3;
435                parameters n, f;
436                
437                assumptions (1) {
438                    n > 3 * f;
439                    n == 1;
440                    f == 0;
441                }
442
443                locations (2) {
444                    loc1 : [0];
445                    loc2 : [1];
446                    loc3 : [2];
447                }
448
449                inits (1) {
450                    loc1 == n - f;
451                    loc2 == 0;
452                    loc3 == 0;
453                    var1 == 0;
454                    var2 == 0;
455                    var3 == 0;
456                }
457
458                rules (4) {
459                    0: loc1 -> loc1
460                        when(true)
461                        do {var1' == var1 + 1};
462                    1: loc1 -> loc2
463                        when(true)
464                        do {};
465                    2: loc2 -> loc3
466                        when(var1 > 3 && var2 <= 0 && var1 < 6 )
467                        do {};
468                    
469                }
470
471                specifications (1) {
472                    test1:
473                        []((loc3 == 0) || (var1 < 5))
474                }
475            }
476            ";
477
478        let (ta, spec) = ByMCParser::new().parse_ta_and_spec(test_spec).unwrap();
479
480        let mc = ACSModelChecker::new(
481            Some(SMTSolverBuilderCfg::new_z3()),
482            None,
483            Vec::new(),
484            ta.clone(),
485            spec.into_iter(),
486        );
487        let mc = mc.unwrap();
488        let res = mc.verify(true).unwrap();
489
490        // Replicate interval ta for path builder
491
492        let path = PathBuilder::new(ta.clone())
493            .add_parameter_assignment(HashMap::from([
494                (Parameter::new("n"), 1),
495                (Parameter::new("f"), 0),
496            ]))
497            .unwrap()
498            .add_configuration(Configuration::new(
499                HashMap::from([
500                    (Variable::new("var1"), 0),
501                    (Variable::new("var2"), 0),
502                    (Variable::new("var3"), 0),
503                ]),
504                HashMap::from([
505                    (Location::new("loc1"), 1),
506                    (Location::new("loc2"), 0),
507                    (Location::new("loc3"), 0),
508                ]),
509            ))
510            .unwrap()
511            .add_transition(Transition::new(
512                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc1"))
513                    .with_action(Action::new_with_update(
514                        Variable::new("var1"),
515                        UpdateExpression::Inc(1),
516                    ))
517                    .build(),
518                5,
519            ))
520            .unwrap()
521            .add_configuration(Configuration::new(
522                HashMap::from([
523                    (Variable::new("var1"), 5),
524                    (Variable::new("var2"), 0),
525                    (Variable::new("var3"), 0),
526                ]),
527                HashMap::from([
528                    (Location::new("loc1"), 1),
529                    (Location::new("loc2"), 0),
530                    (Location::new("loc3"), 0),
531                ]),
532            ))
533            .unwrap()
534            .add_transition(Transition::new(
535                RuleBuilder::new(1, Location::new("loc1"), Location::new("loc2")).build(),
536                1,
537            ))
538            .unwrap()
539            .add_configuration(Configuration::new(
540                HashMap::from([
541                    (Variable::new("var1"), 5),
542                    (Variable::new("var2"), 0),
543                    (Variable::new("var3"), 0),
544                ]),
545                HashMap::from([
546                    (Location::new("loc1"), 0),
547                    (Location::new("loc2"), 1),
548                    (Location::new("loc3"), 0),
549                ]),
550            ))
551            .unwrap()
552            .add_transition(Transition::new(
553                RuleBuilder::new(2, Location::new("loc2"), Location::new("loc3"))
554                    .with_guard(
555                        BooleanExpression::ComparisonExpression(
556                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
557                            ComparisonOp::Gt,
558                            Box::new(IntegerExpression::Const(3)),
559                        ) & BooleanExpression::ComparisonExpression(
560                            Box::new(IntegerExpression::Atom(Variable::new("var2"))),
561                            ComparisonOp::Leq,
562                            Box::new(IntegerExpression::Const(0)),
563                        ) & BooleanExpression::ComparisonExpression(
564                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
565                            ComparisonOp::Lt,
566                            Box::new(IntegerExpression::Const(6)),
567                        ),
568                    )
569                    .build(),
570                1,
571            ))
572            .unwrap()
573            .add_configuration(Configuration::new(
574                HashMap::from([
575                    (Variable::new("var1"), 5),
576                    (Variable::new("var2"), 0),
577                    (Variable::new("var3"), 0),
578                ]),
579                HashMap::from([
580                    (Location::new("loc1"), 0),
581                    (Location::new("loc2"), 0),
582                    (Location::new("loc3"), 1),
583                ]),
584            ))
585            .unwrap()
586            .build()
587            .unwrap();
588
589        let res = match res {
590            ModelCheckerResult::SAFE => {
591                unreachable!("Expected UNSAFE result based on test specification")
592            }
593            ModelCheckerResult::UNSAFE { violations: v, .. } => {
594                assert_eq!(v.len(), 1);
595                *v[0].1.clone()
596            }
597            ModelCheckerResult::UNKNOWN(_) => todo!(),
598        };
599
600        assert_eq!(
601            res,
602            path.clone(),
603            "Got:\n{}\n\nExpected:\n{}\n\n",
604            res,
605            path
606        );
607    }
608
609    #[test]
610    fn test_err_on_reach_spec() {
611        let test_spec = "
612            skel test_ta1 {
613                shared var1, var2, var3;
614                parameters n, f;
615                
616                assumptions (1) {
617                    n > 3 * f;
618                    n == 1;
619                    f == 0;
620                }
621
622                locations (2) {
623                    loc1 : [0];
624                    loc2 : [1];
625                    loc3 : [2];
626                }
627
628                inits (1) {
629                    loc1 == n - f;
630                    loc2 == 0;
631                    loc3 == 0;
632                    var1 == 0;
633                    var2 == 0;
634                    var3 == 0;
635                }
636
637                rules (4) {
638                    0: loc1 -> loc1
639                        when(true)
640                        do {var1' == var1 + 1};
641                    1: loc1 -> loc2
642                        when(true)
643                        do {};
644                    2: loc2 -> loc3
645                        when(var1 > 3 && var2 <= 0 && var1 <= 4)
646                        do {};
647                    
648                }
649
650                specifications (1) {
651                    test1:
652                        [](loc3 == 0 && loc2 != 0)
653                }
654            }
655            ";
656
657        let (ta, spec) = ByMCParser::new().parse_ta_and_spec(test_spec).unwrap();
658
659        let mc = ACSModelChecker::new(
660            Some(SMTSolverBuilderCfg::new_z3()),
661            None,
662            Vec::new(),
663            ta.clone(),
664            spec.into_iter(),
665        );
666
667        assert!(mc.is_err());
668
669        assert!(matches!(
670            mc.unwrap_err(),
671            ModelCheckerSetupError::ErrorInitializingModelChecker(
672                ACSModelCheckerInitializationError::ReachabilitySpec(_)
673            )
674        ));
675    }
676
677    /// Check that results are reported per property name, and that
678    /// properties the model checker cannot decide are reported as unknown
679    #[test]
680    fn test_result_reporting_per_property() {
681        let run = |specs: &str| {
682            let (ta, spec) = ByMCParser::new()
683                .parse_ta_and_spec(&format!(
684                    "
685            skel test_ta1 {{
686                shared var1;
687                parameters n, f;
688
689                assumptions (1) {{
690                    n > 3 * f;
691                    n == 1;
692                }}
693
694                locations (2) {{
695                    loc1 : [0];
696                    loc2 : [1];
697                    loc3 : [2];
698                }}
699
700                inits (1) {{
701                    loc1 == n - f;
702                    loc2 == 0;
703                    loc3 == 0;
704                    var1 == 0;
705                }}
706
707                rules (4) {{
708                    0: loc1 -> loc2
709                        when(true)
710                        do {{}};
711                }}
712
713                specifications (1) {{
714                    {specs}
715                }}
716            }}
717                    "
718                ))
719                .unwrap();
720
721            let mc = ACSModelChecker::new(
722                Some(SMTSolverBuilderCfg::new_z3()),
723                None,
724                Vec::new(),
725                ta,
726                spec.expressions().iter().cloned(),
727            );
728            mc.expect("Failed to create model checker")
729                .verify(false)
730                .expect("Failed to model check")
731        };
732
733        let res = run("
734            holds: [](loc3 == 0);
735            reach_violated: [](loc2 == 0);
736            init_violated: loc1 == 0;
737            untranslatable: [](<>(loc1 == 0 || [](loc2 == 0)));
738        ");
739        let ModelCheckerResult::UNSAFE {
740            violations,
741            unknown,
742        } = res
743        else {
744            panic!("Expected UNSAFE, got {res:?}");
745        };
746        assert_eq!(unknown, vec!["untranslatable"]);
747        let mut names = violations
748            .iter()
749            .map(|(n, _)| n.as_str())
750            .collect::<Vec<_>>();
751        names.sort();
752        assert_eq!(names, vec!["init_violated", "reach_violated"]);
753
754        let res = run("
755            holds: [](loc3 == 0);
756            liveness: <>(loc2 != 0);
757            untranslatable: [](<>(loc1 == 0 || [](loc2 == 0)));
758        ");
759        let ModelCheckerResult::UNKNOWN(mut unknown) = res else {
760            panic!("Expected UNKNOWN, got {res:?}");
761        };
762        unknown.sort();
763        assert_eq!(unknown, vec!["liveness", "untranslatable"]);
764    }
765}
taco_acs_model_checker/lib.rs

taco_acs_model_checker/
lib.rs
