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::error;
18
19use log::info;
20use taco_interval_ta::IntervalThresholdAutomaton;
21use taco_model_checker::{
22    DummyError, ModelChecker, ModelCheckerResult,
23    reachability_specification::{DisjunctionTargetConfig, ReachabilityProperty},
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: Vec<(DisjunctionTargetConfig, Vec<IntervalThresholdAutomaton>)>,
53    /// SMT solver builder used for spurious checks
54    ctx: SMTSolverBuilder,
55}
56
57impl ModelChecker for ACSModelChecker {
58    type ModelCheckerContext = SMTSolverBuilder;
59
60    type ModelCheckerOptions = Option<()>;
61
62    type SpecType = ReachabilityProperty;
63
64    type ThresholdAutomatonType = IntervalThresholdAutomaton;
65
66    type InitializationError = ACSModelCheckerInitializationError;
67
68    type ModelCheckingError = DummyError;
69
70    fn initialize(
71        _mode: Self::ModelCheckerOptions,
72        ta_spec: Vec<(
73            <<Self as ModelChecker>::SpecType as taco_model_checker::SpecificationTrait<
74                Self::ModelCheckerContext,
75            >>::InternalSpecType,
76            Vec<Self::ThresholdAutomatonType>,
77        )>,
78        ctx: Self::ModelCheckerContext,
79    ) -> Result<Self, Self::InitializationError> {
80        if let Some((reach_spec, _)) = ta_spec
81            .iter()
82            .find(|(s, _)| s.contains_reachability_constraint())
83        {
84            return Err(ACSModelCheckerInitializationError::ReachabilitySpec(
85                Box::new(reach_spec.clone()),
86            ));
87        }
88
89        Ok(Self { ta_spec, ctx })
90    }
91
92    fn verify(
93        self,
94        abort_on_violation: bool,
95    ) -> Result<ModelCheckerResult, Self::ModelCheckingError> {
96        let mut unsafe_properties = Vec::new();
97
98        for (spec, tas) in self.ta_spec {
99            for ta in tas.into_iter().map(ACSThresholdAutomaton::new) {
100                let error_graph = ErrorGraph::compute_error_graph(spec.clone(), ta);
101
102                if error_graph.is_empty() {
103                    info!(
104                        "Error graph of property {} is empty, property is SAFE in this interval order.",
105                        spec.name()
106                    );
107                    continue;
108                }
109
110                let solver = self.ctx.new_solver();
111
112                info!(
113                    "Error graph of property {} is not empty, checking paths for spuriousness",
114                    spec.name()
115                );
116                let res = error_graph.check_for_non_spurious_counter_example(solver);
117
118                match res {
119                    ModelCheckerResult::SAFE => info!(
120                        "Error graph of property {} is spurious, property is SAFE in this interval order.",
121                        spec.name()
122                    ),
123                    ModelCheckerResult::UNSAFE(items) => {
124                        info!("Found counterexample to property {}", spec.name());
125                        unsafe_properties.extend(items);
126
127                        if abort_on_violation {
128                            return Ok(ModelCheckerResult::UNSAFE(unsafe_properties));
129                        }
130                    }
131                    ModelCheckerResult::UNKNOWN(_) => info!(
132                        "The model checker could not determine whether property {} is safe or unsafe",
133                        spec.name()
134                    ),
135                }
136            }
137        }
138
139        if unsafe_properties.is_empty() {
140            return Ok(ModelCheckerResult::SAFE);
141        }
142
143        Ok(ModelCheckerResult::UNSAFE(unsafe_properties))
144    }
145}
146
147#[derive(Clone, Debug, PartialEq)]
148pub enum ACSModelCheckerInitializationError {
149    ReachabilitySpec(Box<DisjunctionTargetConfig>),
150}
151
152impl fmt::Display for ACSModelCheckerInitializationError {
153    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
154        match self {
155            ACSModelCheckerInitializationError::ReachabilitySpec(spec) => {
156                write!(
157                    f,
158                    "The counter system model checker does not support reachability specifications, but property {} contains a reachability constraint",
159                    spec.name()
160                )
161            }
162        }
163    }
164}
165
166impl error::Error for ACSModelCheckerInitializationError {}
167
168#[cfg(test)]
169mod tests {
170    use std::collections::HashMap;
171
172    use taco_model_checker::{ModelChecker, ModelCheckerResult, ModelCheckerSetupError};
173    use taco_parser::{ParseTAWithLTL, bymc::ByMCParser};
174    use taco_smt_encoder::SMTSolverBuilderCfg;
175    use taco_threshold_automaton::{
176        ModifiableThresholdAutomaton,
177        expressions::{
178            BooleanExpression, ComparisonOp, IntegerExpression, Location, Parameter, Variable,
179        },
180        general_threshold_automaton::{Action, UpdateExpression, builder::RuleBuilder},
181        path::{Configuration, PathBuilder, Transition},
182    };
183
184    use crate::{ACSModelChecker, ACSModelCheckerInitializationError};
185
186    #[test]
187    fn test_full_model_checker_reach_location_three_rules_one_guard_self_loop() {
188        let test_spec = "
189            skel test_ta1 {
190                shared var1, var2, var3;
191                parameters n, f;
192                
193                assumptions (1) {
194                    n > 3 * f;
195                    n == 1;
196                    f == 0;
197                }
198
199                locations (2) {
200                    loc1 : [0];
201                    loc2 : [1];
202                    loc3 : [2];
203                }
204
205                inits (1) {
206                    loc1 == n - f;
207                    loc2 == 0;
208                    loc3 == 0;
209                    var1 == 0;
210                    var2 == 0;
211                    var3 == 0;
212                }
213
214                rules (4) {
215                    0: loc1 -> loc1
216                        when(true)
217                        do {var1' == var1 + 1};
218                    1: loc1 -> loc2
219                        when(true)
220                        do {};
221                    2: loc2 -> loc3
222                        when(var1 > 3 && var2 <= 0 && var1 <= 4)
223                        do {};
224                    
225                }
226
227                specifications (1) {
228                    test1:
229                        [](loc3 == 0)
230                }
231            }
232            ";
233
234        let (ta, spec) = ByMCParser::new().parse_ta_and_spec(test_spec).unwrap();
235
236        let mc = ACSModelChecker::new(
237            Some(SMTSolverBuilderCfg::new_z3()),
238            None,
239            Vec::new(),
240            ta.clone(),
241            spec.into_iter(),
242        );
243        let mc = mc.unwrap();
244        let res = mc.verify(true).unwrap();
245
246        // Replicate spec ta that is created for ta builder
247        let mut spec_ta = ta.clone();
248        spec_ta.set_name("test_ta1-test1".into());
249
250        // Replicate interval ta for path builder
251
252        let path = PathBuilder::new(spec_ta)
253            .add_parameter_assignment(HashMap::from([
254                (Parameter::new("n"), 1),
255                (Parameter::new("f"), 0),
256            ]))
257            .unwrap()
258            .add_configuration(Configuration::new(
259                HashMap::from([
260                    (Variable::new("var1"), 0),
261                    (Variable::new("var2"), 0),
262                    (Variable::new("var3"), 0),
263                ]),
264                HashMap::from([
265                    (Location::new("loc1"), 1),
266                    (Location::new("loc2"), 0),
267                    (Location::new("loc3"), 0),
268                ]),
269            ))
270            .unwrap()
271            .add_transition(Transition::new(
272                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc1"))
273                    .with_action(Action::new_with_update(
274                        Variable::new("var1"),
275                        UpdateExpression::Inc(1),
276                    ))
277                    .build(),
278                1,
279            ))
280            .unwrap()
281            .add_configuration(Configuration::new(
282                HashMap::from([
283                    (Variable::new("var1"), 1),
284                    (Variable::new("var2"), 0),
285                    (Variable::new("var3"), 0),
286                ]),
287                HashMap::from([
288                    (Location::new("loc1"), 1),
289                    (Location::new("loc2"), 0),
290                    (Location::new("loc3"), 0),
291                ]),
292            ))
293            .unwrap()
294            .add_transition(Transition::new(
295                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc1"))
296                    .with_action(Action::new_with_update(
297                        Variable::new("var1"),
298                        UpdateExpression::Inc(1),
299                    ))
300                    .build(),
301                2,
302            ))
303            .unwrap()
304            .add_configuration(Configuration::new(
305                HashMap::from([
306                    (Variable::new("var1"), 3),
307                    (Variable::new("var2"), 0),
308                    (Variable::new("var3"), 0),
309                ]),
310                HashMap::from([
311                    (Location::new("loc1"), 1),
312                    (Location::new("loc2"), 0),
313                    (Location::new("loc3"), 0),
314                ]),
315            ))
316            .unwrap()
317            .add_transition(Transition::new(
318                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc1"))
319                    .with_action(Action::new_with_update(
320                        Variable::new("var1"),
321                        UpdateExpression::Inc(1),
322                    ))
323                    .build(),
324                1,
325            ))
326            .unwrap()
327            .add_configuration(Configuration::new(
328                HashMap::from([
329                    (Variable::new("var1"), 4),
330                    (Variable::new("var2"), 0),
331                    (Variable::new("var3"), 0),
332                ]),
333                HashMap::from([
334                    (Location::new("loc1"), 1),
335                    (Location::new("loc2"), 0),
336                    (Location::new("loc3"), 0),
337                ]),
338            ))
339            .unwrap()
340            .add_transition(Transition::new(
341                RuleBuilder::new(1, Location::new("loc1"), Location::new("loc2")).build(),
342                1,
343            ))
344            .unwrap()
345            .add_configuration(Configuration::new(
346                HashMap::from([
347                    (Variable::new("var1"), 4),
348                    (Variable::new("var2"), 0),
349                    (Variable::new("var3"), 0),
350                ]),
351                HashMap::from([
352                    (Location::new("loc1"), 0),
353                    (Location::new("loc2"), 1),
354                    (Location::new("loc3"), 0),
355                ]),
356            ))
357            .unwrap()
358            .add_transition(Transition::new(
359                RuleBuilder::new(2, Location::new("loc2"), Location::new("loc3"))
360                    .with_guard(
361                        BooleanExpression::ComparisonExpression(
362                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
363                            ComparisonOp::Gt,
364                            Box::new(IntegerExpression::Const(3)),
365                        ) & BooleanExpression::ComparisonExpression(
366                            Box::new(IntegerExpression::Atom(Variable::new("var2"))),
367                            ComparisonOp::Leq,
368                            Box::new(IntegerExpression::Const(0)),
369                        ) & BooleanExpression::ComparisonExpression(
370                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
371                            ComparisonOp::Leq,
372                            Box::new(IntegerExpression::Const(4)),
373                        ),
374                    )
375                    .build(),
376                1,
377            ))
378            .unwrap()
379            .add_configuration(Configuration::new(
380                HashMap::from([
381                    (Variable::new("var1"), 4),
382                    (Variable::new("var2"), 0),
383                    (Variable::new("var3"), 0),
384                ]),
385                HashMap::from([
386                    (Location::new("loc1"), 0),
387                    (Location::new("loc2"), 0),
388                    (Location::new("loc3"), 1),
389                ]),
390            ))
391            .unwrap()
392            .build()
393            .unwrap();
394
395        let res = match res {
396            ModelCheckerResult::SAFE => {
397                unreachable!("Expected UNSAFE result based on test specification")
398            }
399            ModelCheckerResult::UNSAFE(v) => {
400                assert_eq!(v.len(), 1);
401                *v[0].1.clone()
402            }
403            ModelCheckerResult::UNKNOWN(_) => todo!(),
404        };
405
406        assert_eq!(
407            res,
408            path.clone(),
409            "Got:\n{}\n\nExpected:\n{}\n\n",
410            res,
411            path
412        );
413    }
414
415    #[test]
416    fn test_full_model_checker_reach_location_three_rules_one_guard_self_loop_with_var_constr() {
417        let test_spec = "
418            skel test_ta1 {
419                shared var1, var2, var3;
420                parameters n, f;
421                
422                assumptions (1) {
423                    n > 3 * f;
424                    n == 1;
425                    f == 0;
426                }
427
428                locations (2) {
429                    loc1 : [0];
430                    loc2 : [1];
431                    loc3 : [2];
432                }
433
434                inits (1) {
435                    loc1 == n - f;
436                    loc2 == 0;
437                    loc3 == 0;
438                    var1 == 0;
439                    var2 == 0;
440                    var3 == 0;
441                }
442
443                rules (4) {
444                    0: loc1 -> loc1
445                        when(true)
446                        do {var1' == var1 + 1};
447                    1: loc1 -> loc2
448                        when(true)
449                        do {};
450                    2: loc2 -> loc3
451                        when(var1 > 3 && var2 <= 0 && var1 < 6 )
452                        do {};
453                    
454                }
455
456                specifications (1) {
457                    test1:
458                        []((loc3 == 0) || (var1 < 5))
459                }
460            }
461            ";
462
463        let (ta, spec) = ByMCParser::new().parse_ta_and_spec(test_spec).unwrap();
464
465        let mc = ACSModelChecker::new(
466            Some(SMTSolverBuilderCfg::new_z3()),
467            None,
468            Vec::new(),
469            ta.clone(),
470            spec.into_iter(),
471        );
472        let mc = mc.unwrap();
473        let res = mc.verify(true).unwrap();
474
475        // Replicate spec ta that is created for ta builder
476        let mut spec_ta = ta.clone();
477        spec_ta.set_name("test_ta1-test1".into());
478
479        // Replicate interval ta for path builder
480
481        let path = PathBuilder::new(spec_ta)
482            .add_parameter_assignment(HashMap::from([
483                (Parameter::new("n"), 1),
484                (Parameter::new("f"), 0),
485            ]))
486            .unwrap()
487            .add_configuration(Configuration::new(
488                HashMap::from([
489                    (Variable::new("var1"), 0),
490                    (Variable::new("var2"), 0),
491                    (Variable::new("var3"), 0),
492                ]),
493                HashMap::from([
494                    (Location::new("loc1"), 1),
495                    (Location::new("loc2"), 0),
496                    (Location::new("loc3"), 0),
497                ]),
498            ))
499            .unwrap()
500            .add_transition(Transition::new(
501                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc1"))
502                    .with_action(Action::new_with_update(
503                        Variable::new("var1"),
504                        UpdateExpression::Inc(1),
505                    ))
506                    .build(),
507                5,
508            ))
509            .unwrap()
510            .add_configuration(Configuration::new(
511                HashMap::from([
512                    (Variable::new("var1"), 5),
513                    (Variable::new("var2"), 0),
514                    (Variable::new("var3"), 0),
515                ]),
516                HashMap::from([
517                    (Location::new("loc1"), 1),
518                    (Location::new("loc2"), 0),
519                    (Location::new("loc3"), 0),
520                ]),
521            ))
522            .unwrap()
523            .add_transition(Transition::new(
524                RuleBuilder::new(1, Location::new("loc1"), Location::new("loc2")).build(),
525                1,
526            ))
527            .unwrap()
528            .add_configuration(Configuration::new(
529                HashMap::from([
530                    (Variable::new("var1"), 5),
531                    (Variable::new("var2"), 0),
532                    (Variable::new("var3"), 0),
533                ]),
534                HashMap::from([
535                    (Location::new("loc1"), 0),
536                    (Location::new("loc2"), 1),
537                    (Location::new("loc3"), 0),
538                ]),
539            ))
540            .unwrap()
541            .add_transition(Transition::new(
542                RuleBuilder::new(2, Location::new("loc2"), Location::new("loc3"))
543                    .with_guard(
544                        BooleanExpression::ComparisonExpression(
545                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
546                            ComparisonOp::Gt,
547                            Box::new(IntegerExpression::Const(3)),
548                        ) & BooleanExpression::ComparisonExpression(
549                            Box::new(IntegerExpression::Atom(Variable::new("var2"))),
550                            ComparisonOp::Leq,
551                            Box::new(IntegerExpression::Const(0)),
552                        ) & BooleanExpression::ComparisonExpression(
553                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
554                            ComparisonOp::Lt,
555                            Box::new(IntegerExpression::Const(6)),
556                        ),
557                    )
558                    .build(),
559                1,
560            ))
561            .unwrap()
562            .add_configuration(Configuration::new(
563                HashMap::from([
564                    (Variable::new("var1"), 5),
565                    (Variable::new("var2"), 0),
566                    (Variable::new("var3"), 0),
567                ]),
568                HashMap::from([
569                    (Location::new("loc1"), 0),
570                    (Location::new("loc2"), 0),
571                    (Location::new("loc3"), 1),
572                ]),
573            ))
574            .unwrap()
575            .build()
576            .unwrap();
577
578        let res = match res {
579            ModelCheckerResult::SAFE => {
580                unreachable!("Expected UNSAFE result based on test specification")
581            }
582            ModelCheckerResult::UNSAFE(v) => {
583                assert_eq!(v.len(), 1);
584                *v[0].1.clone()
585            }
586            ModelCheckerResult::UNKNOWN(_) => todo!(),
587        };
588
589        assert_eq!(
590            res,
591            path.clone(),
592            "Got:\n{}\n\nExpected:\n{}\n\n",
593            res,
594            path
595        );
596    }
597
598    #[test]
599    fn test_err_on_reach_spec() {
600        let test_spec = "
601            skel test_ta1 {
602                shared var1, var2, var3;
603                parameters n, f;
604                
605                assumptions (1) {
606                    n > 3 * f;
607                    n == 1;
608                    f == 0;
609                }
610
611                locations (2) {
612                    loc1 : [0];
613                    loc2 : [1];
614                    loc3 : [2];
615                }
616
617                inits (1) {
618                    loc1 == n - f;
619                    loc2 == 0;
620                    loc3 == 0;
621                    var1 == 0;
622                    var2 == 0;
623                    var3 == 0;
624                }
625
626                rules (4) {
627                    0: loc1 -> loc1
628                        when(true)
629                        do {var1' == var1 + 1};
630                    1: loc1 -> loc2
631                        when(true)
632                        do {};
633                    2: loc2 -> loc3
634                        when(var1 > 3 && var2 <= 0 && var1 <= 4)
635                        do {};
636                    
637                }
638
639                specifications (1) {
640                    test1:
641                        [](loc3 == 0 && loc2 != 0)
642                }
643            }
644            ";
645
646        let (ta, spec) = ByMCParser::new().parse_ta_and_spec(test_spec).unwrap();
647
648        let mc = ACSModelChecker::new(
649            Some(SMTSolverBuilderCfg::new_z3()),
650            None,
651            Vec::new(),
652            ta.clone(),
653            spec.into_iter(),
654        );
655
656        assert!(mc.is_err());
657
658        assert!(matches!(
659            mc.unwrap_err(),
660            ModelCheckerSetupError::ErrorInitializingModelChecker(
661                ACSModelCheckerInitializationError::ReachabilitySpec(_)
662            )
663        ));
664    }
665}
taco_acs_model_checker/lib.rs

taco_acs_model_checker/
lib.rs
