taco_smt_model_checker/
lib.rs

1//! This module implements the encoding of query on threshold automata into SMT
2//! expressions. The algorithm is based on the encoding described in the paper
3//! ["Complexity of Verification and Synthesis of Threshold Automata"](https://arxiv.org/abs/2002.08507)
4//! by A. R. Balasubramanian, Javier Esparza, Marijana Lazic.
5//!
6//! The paper does not provide a complete encoding of the threshold automata,
7//! instead many implementation details are not provided. As we were not
8//! provided with the source code (nor an executable) of the implementation used
9//! in the paper, we  had to make some assumptions about the implementation
10//! details.
11//!
12//! We will explicitly mark functions that are not directly described in the
13//! paper.
14
15use core::fmt;
16use std::error;
17
18use log::{info, warn};
19use smt_encoding::{ContextMgrError, EContextMgr};
20use taco_model_checker::internal_spec::{
21    ErrorSpec, ErrorTarget, upwards_closed_set::UpwardsClosedSet,
22};
23use taco_model_checker::{ModelChecker, ModelCheckerResult, TASpecOf, TASpecification};
24use taco_smt_encoder::SMTSolverBuilder;
25use taco_threshold_automaton::{
26    ThresholdAutomaton, general_threshold_automaton::GeneralThresholdAutomaton,
27};
28
29#[cfg(feature = "parallel")]
30use futures::StreamExt;
31#[cfg(feature = "parallel")]
32use futures::stream::FuturesUnordered;
33#[cfg(feature = "parallel")]
34use std::sync::{Arc, atomic::AtomicUsize};
35#[cfg(feature = "parallel")]
36use std::{collections::HashMap, sync::atomic::Ordering};
37#[cfg(feature = "parallel")]
38use taco_threshold_automaton::path::Path;
39#[cfg(feature = "parallel")]
40use tokio::runtime::Builder;
41#[cfg(feature = "parallel")]
42use tokio::task::JoinHandle;
43
44pub mod smt_encoding;
45
46/// Options to the SMT model checker
47#[derive(Debug, Clone, PartialEq, Default)]
48pub struct SMTModelCheckerOptions {
49    /// Enable concurrent model checking (default: false / off)
50    #[cfg(feature = "parallel")]
51    parallel: bool,
52}
53
54impl SMTModelCheckerOptions {
55    #[cfg(feature = "parallel")]
56    pub fn new_parallel() -> Self {
57        Self { parallel: true }
58    }
59
60    #[cfg(feature = "parallel")]
61    pub fn new(parallel: bool) -> Self {
62        Self { parallel }
63    }
64}
65
66/// Errors that can occur during the initialization of the SMT model checker
67#[derive(Debug, Clone, PartialEq, Eq)]
68pub enum SMTModelCheckerInitializationError {
69    /// Threshold automaton has decrements or resets
70    ResetsOrDecrements,
71}
72
73impl fmt::Display for SMTModelCheckerInitializationError {
74    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
75        match self {
76            SMTModelCheckerInitializationError::ResetsOrDecrements => {
77                write!(f, "Threshold automaton has decrements or resets")
78            }
79        }
80    }
81}
82
83impl error::Error for SMTModelCheckerInitializationError {}
84
85#[derive(Debug, Clone)]
86pub struct SMTModelChecker {
87    _opts: SMTModelCheckerOptions,
88    solver_builder: SMTSolverBuilder,
89    ta_spec: TASpecOf<Self>,
90    /// Properties that could not be translated
91    unknown: Vec<String>,
92}
93
94impl ModelChecker for SMTModelChecker {
95    type ModelCheckerContext = SMTSolverBuilder;
96
97    type ModelCheckerOptions = SMTModelCheckerOptions;
98
99    type SpecType = ErrorSpec;
100
101    type ThresholdAutomatonType = GeneralThresholdAutomaton;
102
103    type InitializationError = SMTModelCheckerInitializationError;
104
105    type ModelCheckingError = ContextMgrError;
106
107    fn initialize(
108        opts: Self::ModelCheckerOptions,
109        ta_spec: TASpecOf<Self>,
110        unknown: Vec<String>,
111        ctx: Self::ModelCheckerContext,
112    ) -> Result<Self, Self::InitializationError> {
113        if ta_spec
114            .iter()
115            .any(|(_, _, tas)| tas.iter().any(|ta| ta.has_decrements_or_resets()))
116        {
117            return Err(SMTModelCheckerInitializationError::ResetsOrDecrements);
118        }
119
120        Ok(Self {
121            _opts: opts,
122            solver_builder: ctx,
123            ta_spec,
124            unknown,
125        })
126    }
127
128    fn verify(
129        self,
130        abort_on_violation: bool,
131    ) -> Result<taco_model_checker::ModelCheckerResult, Self::ModelCheckingError> {
132        #[cfg(feature = "parallel")]
133        if self._opts.parallel {
134            return self.model_check_concurrent(abort_on_violation);
135        }
136
137        self.model_check_non_concurrent(abort_on_violation)
138    }
139}
140
141impl SMTModelChecker {
142    /// Execute the model checker sequentially
143    fn model_check_non_concurrent(
144        self,
145        abort_on_violation: bool,
146    ) -> Result<ModelCheckerResult, ContextMgrError> {
147        let mut unsafe_prop = Vec::new();
148        let mut unknown_prop = self.unknown;
149
150        for (name, target, tas_to_check) in self.ta_spec.into_iter() {
151            let ErrorTarget::Reach(target) = target else {
152                warn!("Property '{name}' ({target}) is not supported by the SMT model checker");
153                unknown_prop.push(name);
154                continue;
155            };
156
157            info!(
158                "Starting to check property '{}', which requires {} model checker run(s).",
159                name,
160                tas_to_check.len()
161            );
162            let mut found_counter_ex = false;
163            for ta in tas_to_check.into_iter() {
164                let target_var_constr = target.var_constraint().into_iter().collect::<Vec<_>>();
165
166                let ctx_mgr = EContextMgr::new(ta, &target_var_constr, &self.solver_builder)?;
167                let res = ctx_mgr.check_spec(&target);
168                if let Some(p) = res {
169                    info!("Property {} is not satisfied!", name);
170
171                    unsafe_prop.push((name.clone(), Box::new(p)));
172
173                    if abort_on_violation {
174                        return Ok(ModelCheckerResult::UNSAFE {
175                            violations: unsafe_prop,
176                            unknown: unknown_prop,
177                        });
178                    }
179
180                    found_counter_ex = true;
181                    break;
182                }
183            }
184
185            if !found_counter_ex {
186                info!(
187                    "Finished verifying property '{}'. The property holds!",
188                    name
189                );
190            }
191        }
192
193        if !unsafe_prop.is_empty() {
194            return Ok(ModelCheckerResult::UNSAFE {
195                violations: unsafe_prop,
196                unknown: unknown_prop,
197            });
198        }
199        if !unknown_prop.is_empty() {
200            return Ok(ModelCheckerResult::UNKNOWN(unknown_prop));
201        }
202
203        Ok(ModelCheckerResult::SAFE)
204    }
205
206    #[cfg(feature = "parallel")]
207    /// Verify all properties concurrently
208    ///
209    /// This method will build a multi-threaded runtime and will attempt to
210    /// check each property concurrently to attempt to reduce the overall
211    /// runtime.
212    ///
213    /// TODO: The setup is still very rudimentary and could be fine tuned in the
214    /// future
215    fn model_check_concurrent(
216        self,
217        abort_on_violation: bool,
218    ) -> Result<ModelCheckerResult, ContextMgrError> {
219        use std::collections::HashMap;
220
221        let runtime = Builder::new_multi_thread()
222            .thread_name("taco-smt-mc")
223            .build()
224            .unwrap();
225
226        let mut completed_map: HashMap<String, (usize, Arc<AtomicUsize>)> = HashMap::new();
227        let mut unknown_prop = self.unknown;
228
229        let futures = FuturesUnordered::new();
230        for (name, target, tas_to_check) in self.ta_spec.into_iter() {
231            let ErrorTarget::Reach(target) = target else {
232                warn!("Property '{name}' ({target}) is not supported by the SMT model checker");
233                unknown_prop.push(name);
234                continue;
235            };
236
237            info!(
238                "Queuing checks for property '{}', which requires {} model checker run(s).",
239                name,
240                tas_to_check.len()
241            );
242
243            // Multiple targets can belong to the same property
244            let (expected, completed_safe_counter) = completed_map
245                .entry(name.clone())
246                .or_insert_with(|| (0, Arc::new(AtomicUsize::new(0))));
247            *expected += tas_to_check.len();
248            let completed_safe_counter = completed_safe_counter.clone();
249
250            for ta in tas_to_check.into_iter() {
251                let ft = runtime.spawn(Self::check_single_target(
252                    ta,
253                    name.clone(),
254                    target.clone(),
255                    self.solver_builder.clone(),
256                    completed_safe_counter.clone(),
257                ));
258                futures.push(ft.into_future());
259            }
260        }
261
262        let res = runtime.spawn(Self::wait_for_mc_results(
263            futures,
264            abort_on_violation,
265            completed_map,
266            unknown_prop,
267        ));
268        runtime
269            .block_on(res)
270            .expect("Task panicked or runtime error")
271    }
272
273    #[cfg(feature = "parallel")]
274    /// Helper method to collect the results and abort early if desired
275    ///
276    // TODO: early abort is currently not working. It would require rewriting
277    // the model checker in an asynchronous fashion
278    async fn wait_for_mc_results(
279        mut futures: FuturesUnordered<JoinHandle<Result<ModelCheckerResult, ContextMgrError>>>,
280        abort_on_violation: bool,
281        completed_map: HashMap<String, (usize, Arc<AtomicUsize>)>,
282        unknown_prop: Vec<String>,
283    ) -> Result<ModelCheckerResult, ContextMgrError> {
284        let mut found_violations: Vec<(String, Box<Path>)> = Vec::new();
285
286        while let Some(result) = futures.next().await {
287            let res = result.expect("Task panicked or runtime error")?;
288
289            if let ModelCheckerResult::UNSAFE { mut violations, .. } = res {
290                if abort_on_violation {
291                    futures.into_iter().for_each(|f| {
292                        f.abort();
293                    });
294                    return Ok(ModelCheckerResult::UNSAFE {
295                        violations,
296                        unknown: unknown_prop,
297                    });
298                }
299                found_violations.append(&mut violations);
300            }
301        }
302
303        for (property_name, (expected_safe, terminated_safe)) in completed_map {
304            if expected_safe == terminated_safe.load(Ordering::SeqCst) {
305                info!("Finished verifying property '{property_name}'. The property holds!")
306            }
307        }
308
309        if !found_violations.is_empty() {
310            return Ok(ModelCheckerResult::UNSAFE {
311                violations: found_violations,
312                unknown: unknown_prop,
313            });
314        }
315        if !unknown_prop.is_empty() {
316            return Ok(ModelCheckerResult::UNKNOWN(unknown_prop));
317        }
318
319        Ok(ModelCheckerResult::SAFE)
320    }
321
322    #[cfg(feature = "parallel")]
323    /// Check reachability of a single [`DisjunctionTargetConfig`]
324    async fn check_single_target(
325        ta: GeneralThresholdAutomaton,
326        name: String,
327        target: UpwardsClosedSet,
328        solver_builder: SMTSolverBuilder,
329        safe_counter: Arc<AtomicUsize>,
330    ) -> Result<ModelCheckerResult, ContextMgrError> {
331        let target_var_constr = target.var_constraint().into_iter().collect::<Vec<_>>();
332
333        let ctx_mgr = EContextMgr::new(ta, &target_var_constr, &solver_builder)?;
334        let res = ctx_mgr.check_spec(&target);
335
336        if let Some(p) = res {
337            info!("Property {} is not satisfied!", target);
338
339            return Ok(ModelCheckerResult::UNSAFE {
340                violations: vec![(name, Box::new(p))],
341                unknown: Vec::new(),
342            });
343        }
344
345        safe_counter.fetch_add(1, Ordering::SeqCst);
346        Ok(ModelCheckerResult::SAFE)
347    }
348}
349
350impl Default for SMTModelChecker {
351    fn default() -> Self {
352        Self::new_mc()
353    }
354}
355
356impl SMTModelChecker {
357    pub fn new_mc() -> Self {
358        Self {
359            _opts: SMTModelCheckerOptions::default(),
360            solver_builder: SMTSolverBuilder::default(),
361            ta_spec: Vec::new(),
362            unknown: Vec::new(),
363        }
364    }
365
366    pub fn new_mc_with_opts(opts: SMTModelCheckerOptions) -> Self {
367        Self {
368            _opts: opts,
369            solver_builder: SMTSolverBuilder::default(),
370            ta_spec: Vec::new(),
371            unknown: Vec::new(),
372        }
373    }
374}
375
376#[cfg(test)]
377mod tests {
378
379    use super::*;
380    use std::collections::HashMap;
381    use taco_model_checker::ModelChecker;
382    use taco_model_checker::internal_spec::upwards_closed_set::UpwardsClosedSet;
383    use taco_parser::{ParseTA, ParseTAWithLTL, bymc::ByMCParser};
384    use taco_smt_encoder::SMTSolverBuilderCfg;
385    use taco_threshold_automaton::{
386        expressions::{
387            BooleanExpression, ComparisonOp, IntegerExpression, Location, Parameter, Variable,
388        },
389        general_threshold_automaton::{Action, UpdateExpression, builder::RuleBuilder},
390        path::{Configuration, PathBuilder, Transition},
391    };
392
393    #[test]
394    fn test_can_initialize_true() {
395        let test_spec = "
396            skel test_ta1 {
397                shared var1, var2, var3;
398                parameters n, f;
399                
400                assumptions (1) {
401                    n > 3 * f;
402                    n == 1;
403                }
404
405                locations (2) {
406                    loc1 : [0];
407                    loc2 : [1];
408                    loc3 : [2];
409                }
410
411                inits (1) {
412                    loc1 == n - f;
413                    loc2 == 0;
414                    loc3 == 0;
415                    var1 == 0;
416                    var2 == 0;
417                    var3 == 0;
418                }
419
420                rules (4) {
421                    0: loc1 -> loc2
422                        when(true)
423                        do {};
424                }
425            }
426            ";
427
428        let ta = ByMCParser::new().parse_ta(test_spec).unwrap();
429        let spec = UpwardsClosedSet::new_cover([Location::new("loc1")]);
430
431        let mc = SMTModelChecker::initialize(
432            SMTModelCheckerOptions::default(),
433            vec![("test".to_string(), ErrorTarget::Reach(spec), vec![ta])],
434            Vec::new(),
435            SMTSolverBuilder::default(),
436        );
437        assert!(mc.is_ok());
438    }
439
440    #[test]
441    fn test_can_initialize_false() {
442        let test_spec = "
443            skel test_ta1 {
444                shared var1, var2, var3;
445                parameters n, f;
446                
447                assumptions (1) {
448                    n > 3 * f;
449                    n == 1;
450                }
451
452                locations (2) {
453                    loc1 : [0];
454                    loc2 : [1];
455                    loc3 : [2];
456                }
457
458                inits (1) {
459                    loc1 == n - f;
460                    loc2 == 0;
461                    loc3 == 0;
462                    var1 == 0;
463                    var2 == 0;
464                    var3 == 0;
465                }
466
467                rules (4) {
468                    0: loc1 -> loc2
469                        when(true)
470                        do { var1' == 0; };
471                }
472            }
473            ";
474
475        let ta = ByMCParser::new().parse_ta(test_spec).unwrap();
476        let spec = UpwardsClosedSet::new_cover([Location::new("loc1")]);
477
478        let mc = SMTModelChecker::initialize(
479            SMTModelCheckerOptions::default(),
480            vec![("test".to_string(), ErrorTarget::Reach(spec), vec![ta])],
481            Vec::new(),
482            SMTSolverBuilder::default(),
483        );
484
485        assert!(mc.is_err());
486    }
487
488    #[test]
489    fn test_smt_model_checker_simple_unsafe() {
490        let test_spec = "
491            skel test_ta1 {
492                shared var1, var2, var3;
493                parameters n, f;
494                
495                assumptions (1) {
496                    n > 3 * f;
497                    n == 1;
498                }
499
500                locations (2) {
501                    loc1 : [0];
502                    loc2 : [1];
503                    loc3 : [2];
504                }
505
506                inits (1) {
507                    loc1 == n - f;
508                    loc2 == 0;
509                    loc3 == 0;
510                    var1 == 0;
511                    var2 == 0;
512                    var3 == 0;
513                }
514
515                rules (4) {
516                    0: loc1 -> loc2
517                        when(true)
518                        do {};
519                }
520
521                specifications (1) {
522                    test1:
523                        [](loc1 == 0)
524                }
525            }
526            ";
527
528        let ta = ByMCParser::new().parse_ta(test_spec).unwrap();
529        let spec = UpwardsClosedSet::new_cover([Location::new("loc1")]);
530
531        let mc = SMTModelChecker::initialize(
532            SMTModelCheckerOptions::default(),
533            vec![("test".to_string(), ErrorTarget::Reach(spec), vec![ta])],
534            Vec::new(),
535            SMTSolverBuilder::default(),
536        )
537        .unwrap();
538        let res = mc.verify(true);
539        assert!(res.is_ok());
540        assert!(matches!(res.unwrap(), ModelCheckerResult::UNSAFE { .. }));
541    }
542
543    #[cfg(feature = "parallel")]
544    #[test]
545    fn test_smt_model_checker_simple_unsafe_parallel() {
546        let test_spec = "
547            skel test_ta1 {
548                shared var1, var2, var3;
549                parameters n, f;
550                
551                assumptions (1) {
552                    n > 3 * f;
553                    n == 1;
554                }
555
556                locations (2) {
557                    loc1 : [0];
558                    loc2 : [1];
559                    loc3 : [2];
560                }
561
562                inits (1) {
563                    loc1 == n - f;
564                    loc2 == 0;
565                    loc3 == 0;
566                    var1 == 0;
567                    var2 == 0;
568                    var3 == 0;
569                }
570
571                rules (4) {
572                    0: loc1 -> loc2
573                        when(true)
574                        do {};
575                }
576
577                specifications (1) {
578                    test1:
579                        [](loc1 == 0)
580                }
581            }
582            ";
583
584        let ta = ByMCParser::new().parse_ta(test_spec).unwrap();
585        let spec = UpwardsClosedSet::new_cover([Location::new("loc1")]);
586
587        let mc = SMTModelChecker::initialize(
588            SMTModelCheckerOptions::new_parallel(),
589            vec![("test".to_string(), ErrorTarget::Reach(spec), vec![ta])],
590            Vec::new(),
591            SMTSolverBuilder::default(),
592        )
593        .unwrap();
594        let res = mc.verify(true);
595        assert!(res.is_ok());
596        assert!(matches!(res.unwrap(), ModelCheckerResult::UNSAFE { .. }));
597    }
598
599    #[test]
600    fn test_smt_model_checker_simple_safe() {
601        let test_spec = "
602            skel test_ta1 {
603                shared var1, var2, var3;
604                parameters n, f;
605                
606                assumptions (1) {
607                    n > 3 * f;
608                    n == 1;
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 -> loc2
628                        when(true)
629                        do {};
630                }
631
632                specifications (1) {
633                    test1:
634                        [](loc3 == 0)
635                }
636            }
637            ";
638
639        let ta = ByMCParser::new().parse_ta(test_spec).unwrap();
640        let spec = UpwardsClosedSet::new_cover([Location::new("loc3")]);
641
642        let mc = SMTModelChecker::initialize(
643            SMTModelCheckerOptions::default(),
644            vec![("test".to_string(), ErrorTarget::Reach(spec), vec![ta])],
645            Vec::new(),
646            SMTSolverBuilder::default(),
647        )
648        .unwrap();
649        let res = mc.verify(false);
650        assert!(res.is_ok());
651        assert!(matches!(res.unwrap(), ModelCheckerResult::SAFE));
652    }
653
654    #[cfg(feature = "parallel")]
655    #[test]
656    fn test_smt_model_checker_simple_safe_parallel() {
657        let test_spec = "
658            skel test_ta1 {
659                shared var1, var2, var3;
660                parameters n, f;
661                
662                assumptions (1) {
663                    n > 3 * f;
664                    n == 1;
665                }
666
667                locations (2) {
668                    loc1 : [0];
669                    loc2 : [1];
670                    loc3 : [2];
671                }
672
673                inits (1) {
674                    loc1 == n - f;
675                    loc2 == 0;
676                    loc3 == 0;
677                    var1 == 0;
678                    var2 == 0;
679                    var3 == 0;
680                }
681
682                rules (4) {
683                    0: loc1 -> loc2
684                        when(true)
685                        do {};
686                }
687
688                specifications (1) {
689                    test1:
690                        [](loc3 == 0)
691                }
692            }
693            ";
694
695        let ta = ByMCParser::new().parse_ta(test_spec).unwrap();
696        let spec = UpwardsClosedSet::new_cover([Location::new("loc3")]);
697
698        let mc = SMTModelChecker::initialize(
699            SMTModelCheckerOptions::new_parallel(),
700            vec![("test".to_string(), ErrorTarget::Reach(spec), vec![ta])],
701            Vec::new(),
702            SMTSolverBuilder::default(),
703        )
704        .unwrap();
705        let res = mc.verify(false);
706        assert!(res.is_ok());
707        assert!(matches!(res.unwrap(), ModelCheckerResult::SAFE));
708    }
709
710    #[test]
711    fn test_smt_model_checker_simple_safe_new_mc() {
712        let test_spec = "
713            skel test_ta1 {
714                shared var1, var2, var3;
715                parameters n, f;
716                
717                assumptions (1) {
718                    n > 3 * f;
719                    n == 1;
720                }
721
722                locations (2) {
723                    loc1 : [0];
724                    loc2 : [1];
725                    loc3 : [2];
726                }
727
728                inits (1) {
729                    loc1 == n - f;
730                    loc2 == 0;
731                    loc3 == 0;
732                    var1 == 0;
733                    var2 == 0;
734                    var3 == 0;
735                }
736
737                rules (4) {
738                    0: loc1 -> loc2
739                        when(true)
740                        do {};
741                }
742
743                specifications (1) {
744                    test1:
745                        [](loc3 == 0)
746                }
747            }
748          ";
749
750        let (ta, spec) = ByMCParser::new().parse_ta_and_spec(test_spec).unwrap();
751
752        let mc = SMTModelChecker::new(
753            Some(SMTSolverBuilderCfg::new_z3()),
754            SMTModelCheckerOptions::default(),
755            Vec::new(),
756            ta,
757            spec.expressions().iter().cloned(),
758        )
759        .expect("Failed to create SMT model checker");
760
761        let res = mc.verify(false).expect("Failed to model check");
762        assert!(matches!(res, ModelCheckerResult::SAFE));
763    }
764
765    #[cfg(feature = "parallel")]
766    #[test]
767    fn test_smt_model_checker_simple_safe_new_mc_parallel() {
768        let test_spec = "
769            skel test_ta1 {
770                shared var1, var2, var3;
771                parameters n, f;
772                
773                assumptions (1) {
774                    n > 3 * f;
775                    n == 1;
776                }
777
778                locations (2) {
779                    loc1 : [0];
780                    loc2 : [1];
781                    loc3 : [2];
782                }
783
784                inits (1) {
785                    loc1 == n - f;
786                    loc2 == 0;
787                    loc3 == 0;
788                    var1 == 0;
789                    var2 == 0;
790                    var3 == 0;
791                }
792
793                rules (4) {
794                    0: loc1 -> loc2
795                        when(true)
796                        do {};
797                }
798
799                specifications (1) {
800                    test1:
801                        [](loc3 == 0)
802                }
803            }
804          ";
805
806        let (ta, spec) = ByMCParser::new().parse_ta_and_spec(test_spec).unwrap();
807
808        let mc = SMTModelChecker::new(
809            Some(SMTSolverBuilderCfg::new_z3()),
810            SMTModelCheckerOptions::new_parallel(),
811            Vec::new(),
812            ta,
813            spec.expressions().iter().cloned(),
814        )
815        .expect("Failed to create SMT model checker");
816
817        let res = mc.verify(false).expect("Failed to model check");
818        assert!(matches!(res, ModelCheckerResult::SAFE));
819    }
820
821    #[test]
822    fn test_display_initialization_error() {
823        let error = SMTModelCheckerInitializationError::ResetsOrDecrements;
824        assert_eq!(
825            format!("{error}"),
826            "Threshold automaton has decrements or resets"
827        );
828    }
829
830    #[test]
831    #[cfg(feature = "parallel")]
832    fn test_full_model_checker_reach_location_three_rules_one_guard_self_loop_with_var_constr() {
833        let test_spec = "
834            skel test_ta1 {
835                shared var1, var2, var3;
836                parameters n, f;
837                
838                assumptions (1) {
839                    n > 3 * f;
840                    n == 1;
841                    f == 0;
842                }
843
844                locations (2) {
845                    loc1 : [0];
846                    loc2 : [1];
847                    loc3 : [2];
848                }
849
850                inits (1) {
851                    loc1 == n - f;
852                    loc2 == 0;
853                    loc3 == 0;
854                    var1 == 0;
855                    var2 == 0;
856                    var3 == 0;
857                }
858
859                rules (4) {
860                    0: loc1 -> loc1
861                        when(true)
862                        do {var1' == var1 + 1};
863                    1: loc1 -> loc2
864                        when(true)
865                        do {};
866                    2: loc2 -> loc3
867                        when(var1 > 3 && var2 <= 0 && var1 < 6 )
868                        do {};
869                    
870                }
871
872                specifications (1) {
873                    test1:
874                        []((loc3 == 0) || (var1 < 5))
875                }
876            }
877            ";
878
879        let (ta, spec) = ByMCParser::new().parse_ta_and_spec(test_spec).unwrap();
880
881        let mc = SMTModelChecker::new(
882            Some(SMTSolverBuilderCfg::new_z3()),
883            SMTModelCheckerOptions::new(false),
884            Vec::new(),
885            ta.clone(),
886            spec.into_iter(),
887        );
888        let mc = mc.unwrap();
889        let res = mc.verify(true).unwrap();
890
891        // Replicate spec ta that is created for ta builder
892        let spec_ta = ta.clone();
893
894        // Replicate interval ta for path builder
895
896        let path = PathBuilder::new(spec_ta)
897            .add_parameter_assignment(HashMap::from([
898                (Parameter::new("n"), 1),
899                (Parameter::new("f"), 0),
900            ]))
901            .unwrap()
902            .add_configuration(Configuration::new(
903                HashMap::from([
904                    (Variable::new("var1"), 0),
905                    (Variable::new("var2"), 0),
906                    (Variable::new("var3"), 0),
907                ]),
908                HashMap::from([
909                    (Location::new("loc1"), 1),
910                    (Location::new("loc2"), 0),
911                    (Location::new("loc3"), 0),
912                ]),
913            ))
914            .unwrap()
915            .add_transition(Transition::new(
916                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc1"))
917                    .with_action(Action::new_with_update(
918                        Variable::new("var1"),
919                        UpdateExpression::Inc(1),
920                    ))
921                    .build(),
922                5,
923            ))
924            .unwrap()
925            .add_configuration(Configuration::new(
926                HashMap::from([
927                    (Variable::new("var1"), 5),
928                    (Variable::new("var2"), 0),
929                    (Variable::new("var3"), 0),
930                ]),
931                HashMap::from([
932                    (Location::new("loc1"), 1),
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("loc2")).build(),
940                1,
941            ))
942            .unwrap()
943            .add_configuration(Configuration::new(
944                HashMap::from([
945                    (Variable::new("var1"), 5),
946                    (Variable::new("var2"), 0),
947                    (Variable::new("var3"), 0),
948                ]),
949                HashMap::from([
950                    (Location::new("loc1"), 0),
951                    (Location::new("loc2"), 1),
952                    (Location::new("loc3"), 0),
953                ]),
954            ))
955            .unwrap()
956            .add_transition(Transition::new(
957                RuleBuilder::new(2, Location::new("loc2"), Location::new("loc3"))
958                    .with_guard(
959                        BooleanExpression::ComparisonExpression(
960                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
961                            ComparisonOp::Gt,
962                            Box::new(IntegerExpression::Const(3)),
963                        ) & BooleanExpression::ComparisonExpression(
964                            Box::new(IntegerExpression::Atom(Variable::new("var2"))),
965                            ComparisonOp::Leq,
966                            Box::new(IntegerExpression::Const(0)),
967                        ) & BooleanExpression::ComparisonExpression(
968                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
969                            ComparisonOp::Lt,
970                            Box::new(IntegerExpression::Const(6)),
971                        ),
972                    )
973                    .build(),
974                1,
975            ))
976            .unwrap()
977            .add_configuration(Configuration::new(
978                HashMap::from([
979                    (Variable::new("var1"), 5),
980                    (Variable::new("var2"), 0),
981                    (Variable::new("var3"), 0),
982                ]),
983                HashMap::from([
984                    (Location::new("loc1"), 0),
985                    (Location::new("loc2"), 0),
986                    (Location::new("loc3"), 1),
987                ]),
988            ))
989            .unwrap()
990            .build()
991            .unwrap();
992
993        let res = match res {
994            ModelCheckerResult::SAFE => unreachable!("checked above"),
995            ModelCheckerResult::UNSAFE { violations: v, .. } => {
996                assert_eq!(v.len(), 1);
997                *v[0].1.clone()
998            }
999            ModelCheckerResult::UNKNOWN(_) => todo!(),
1000        };
1001
1002        assert_eq!(
1003            res,
1004            path.clone(),
1005            "Got:\n{}\n\nExpected:\n{}\n\n",
1006            res,
1007            path
1008        );
1009    }
1010
1011    /// Automaton for the tests on how results are reported for each property
1012    ///
1013    /// Initially one process is in `loc1`, which can move to `loc2`
1014    fn reporting_test_spec(specs: &str) -> String {
1015        format!(
1016            "
1017            skel test_ta1 {{
1018                shared var1;
1019                parameters n, f;
1020
1021                assumptions (1) {{
1022                    n > 3 * f;
1023                    n == 1;
1024                }}
1025
1026                locations (2) {{
1027                    loc1 : [0];
1028                    loc2 : [1];
1029                    loc3 : [2];
1030                }}
1031
1032                inits (1) {{
1033                    loc1 == n - f;
1034                    loc2 == 0;
1035                    loc3 == 0;
1036                    var1 == 0;
1037                }}
1038
1039                rules (4) {{
1040                    0: loc1 -> loc2
1041                        when(true)
1042                        do {{}};
1043                }}
1044
1045                specifications (1) {{
1046                    {specs}
1047                }}
1048            }}
1049            "
1050        )
1051    }
1052
1053    fn run_reporting_test(specs: &str) -> ModelCheckerResult {
1054        let (ta, spec) = ByMCParser::new()
1055            .parse_ta_and_spec(&reporting_test_spec(specs))
1056            .unwrap();
1057
1058        SMTModelChecker::new(
1059            Some(SMTSolverBuilderCfg::new_z3()),
1060            SMTModelCheckerOptions::default(),
1061            Vec::new(),
1062            ta,
1063            spec.expressions().iter().cloned(),
1064        )
1065        .expect("Failed to create SMT model checker")
1066        .verify(false)
1067        .expect("Failed to model check")
1068    }
1069
1070    #[test]
1071    fn test_violations_reported_by_property_name() {
1072        let res = run_reporting_test(
1073            "
1074            holds: [](loc3 == 0);
1075            reach_violated: [](loc2 == 0);
1076            init_violated: loc1 == 0;
1077            untranslatable: [](<>(loc1 == 0 || [](loc2 == 0)));
1078            ",
1079        );
1080
1081        let ModelCheckerResult::UNSAFE {
1082            violations,
1083            unknown,
1084        } = res
1085        else {
1086            panic!("Expected UNSAFE, got {res:?}");
1087        };
1088        assert_eq!(unknown, vec!["untranslatable"]);
1089        let mut names = violations
1090            .iter()
1091            .map(|(n, _)| n.as_str())
1092            .collect::<Vec<_>>();
1093        names.sort();
1094        assert_eq!(names, vec!["init_violated", "reach_violated"]);
1095    }
1096
1097    #[test]
1098    fn test_unsupported_properties_reported_unknown() {
1099        let res = run_reporting_test(
1100            "
1101            holds: [](loc3 == 0);
1102            liveness: <>(loc2 != 0);
1103            untranslatable: [](<>(loc1 == 0 || [](loc2 == 0)));
1104            ",
1105        );
1106
1107        let ModelCheckerResult::UNKNOWN(mut unknown) = res else {
1108            panic!("Expected UNKNOWN, got {res:?}");
1109        };
1110        unknown.sort();
1111        assert_eq!(unknown, vec!["liveness", "untranslatable"]);
1112    }
1113
1114    #[test]
1115    fn test_init_only_property_holds() {
1116        let res = run_reporting_test("init_holds: loc2 == 0;");
1117        assert_eq!(res, ModelCheckerResult::SAFE);
1118    }
1119}
taco_smt_model_checker/lib.rs

taco_smt_model_checker/
lib.rs
