taco_model_checker/
lib.rs

1//! This module contains the different model checkers that are available in
2//! TACO.
3//! Every model checker needs to implement the [`ModelChecker`] trait.
4
5use core::fmt;
6use std::{error, fmt::Display};
7
8use eltl::ELTLExpression;
9use log::trace;
10use taco_bdd::{BDDManager, BDDManagerConfig};
11use taco_smt_encoder::{
12    ProvidesSMTSolverBuilder, SMTSolverBuilder, SMTSolverBuilderCfg, SMTSolverBuilderError,
13};
14use taco_threshold_automaton::{
15    ModifiableThresholdAutomaton, ThresholdAutomaton,
16    expressions::Location,
17    general_threshold_automaton::GeneralThresholdAutomaton,
18    lia_threshold_automaton::{
19        LIAThresholdAutomaton, LIATransformationError, LIAVariableConstraint,
20    },
21    path::Path,
22};
23
24use crate::preprocessing::Preprocessor;
25
26pub mod eltl;
27pub mod preprocessing;
28pub mod reachability_specification;
29
30/// The [`ModelChecker`] trait defines the interface for all model checkers in
31/// TACO.
32pub trait ModelChecker: Sized {
33    /// Context for the model checker which for example includes interfaces to
34    /// create solvers or BDD libraries
35    type ModelCheckerContext: ModelCheckerContext;
36
37    /// Options for the model checker
38    type ModelCheckerOptions;
39
40    /// Internal specification representation the model checker uses
41    type SpecType: SpecificationTrait<Self::ModelCheckerContext>;
42    /// Internal representation of a threshold automaton the model checker works
43    /// on
44    type ThresholdAutomatonType: TATrait<
45            Self::ModelCheckerContext,
46            <Self::SpecType as SpecificationTrait<Self::ModelCheckerContext>>::InternalSpecType,
47        >;
48
49    /// Error type for errors that can occur during initialization of the model
50    /// checker
51    type InitializationError: error::Error;
52    /// Error type for errors that can occur during the run of the model checker
53    type ModelCheckingError: error::Error;
54
55    /// Initialize the model checker with the internal threshold automaton and
56    /// specification representation
57    ///
58    /// This function needs to be implemented by all model checkers and should
59    /// setup the model checker with the appropriate options, system and
60    /// specification representation, as well as the context containing backend
61    /// functionality like SMT solver configurations.
62    #[allow(clippy::type_complexity)]
63    fn initialize(
64        opts: Self::ModelCheckerOptions,
65        ta_spec: Vec<
66            (
67                <<Self as ModelChecker>::SpecType as SpecificationTrait<
68                    Self::ModelCheckerContext,
69                >>::InternalSpecType,
70                Vec<Self::ThresholdAutomatonType>,
71            ),
72        >,
73        ctx: Self::ModelCheckerContext,
74    ) -> Result<Self, Self::InitializationError>;
75
76    /// Construct a new instance of the model checker
77    ///
78    /// This function will first try to construct the model checker context,
79    /// then try to transform the threshold automaton into the internal type of
80    /// the model checker, after which it will attempt to convert the
81    /// specification into the internal type of the model checker.
82    ///
83    /// If any of these steps fail, or are not possible a
84    /// `ModelCheckerSetupError` will be returned that contains the error of the
85    /// stage it occurred.
86    ///
87    /// If the function returns an `Ok`, the model checker has been initialized
88    /// with the threshold automaton and specification and is ready to be
89    /// checked.
90    #[allow(clippy::type_complexity)]
91    fn new(
92        ctx_opts: Option<
93            <<Self as ModelChecker>::ModelCheckerContext as ModelCheckerContext>::ContextOptions,
94        >,
95        mc_opts: Self::ModelCheckerOptions,
96        preprocessors: Vec<Box<dyn Preprocessor<GeneralThresholdAutomaton, <Self::SpecType as SpecificationTrait<Self::ModelCheckerContext>>::InternalSpecType, Self::ModelCheckerContext>>>,
97        ta: GeneralThresholdAutomaton,
98        spec: impl Iterator<Item = (String, ELTLExpression)>,
99    ) -> Result<
100        Self,
101        ModelCheckerSetupError<
102            <<Self as ModelChecker>::ThresholdAutomatonType as TATrait<
103                Self::ModelCheckerContext, <Self::SpecType as SpecificationTrait<Self::ModelCheckerContext>>::InternalSpecType,
104            >>::TransformationError,
105            <<Self as ModelChecker>::SpecType as SpecificationTrait<
106                Self::ModelCheckerContext,
107            >>::TransformationError,
108            <<Self as ModelChecker>::ModelCheckerContext as ModelCheckerContext>::CreationError,
109            Self::InitializationError,
110        >,
111    >{
112        let ctx = Self::ModelCheckerContext::try_new(ctx_opts);
113        if let Err(ctx_err) = ctx {
114            return Err(ModelCheckerSetupError::ErrorContextSetup(ctx_err));
115        }
116        let ctx = ctx.unwrap();
117
118        let spec = Self::SpecType::try_from_eltl(spec, &ctx);
119        if let Err(spec_err) = spec {
120            return Err(ModelCheckerSetupError::ErrorTransformingSpec(spec_err));
121        }
122        let spec = spec.unwrap();
123
124        // Combine the specification with the threshold automaton
125        let ta_spec = Self::SpecType::transform_threshold_automaton(ta, spec, &ctx);
126
127        let ta_spec = ta_spec
128            .into_iter()
129            .map(|(spec, mut ta)| {
130                // Preprocessing on tas with information from the specification
131                for processor in preprocessors.iter() {
132                    processor.process(&mut ta, &spec, &ctx);
133                }
134
135                trace!("Threshold automaton for property {spec} after preprocessing: {ta}");
136
137                let ta = Self::ThresholdAutomatonType::try_from_general_ta(ta, &ctx, &spec)?;
138
139                Ok((spec, ta))
140            })
141            .collect::<Result<Vec<_>, _>>();
142        if let Err(ta_err) = ta_spec {
143            return Err(ModelCheckerSetupError::ErrorTransformingTA(ta_err));
144        }
145        let ta_spec = ta_spec.unwrap();
146
147        let mc = Self::initialize(mc_opts, ta_spec, ctx.clone());
148        if let Err(mc_err) = mc {
149            return Err(ModelCheckerSetupError::ErrorInitializingModelChecker(
150                mc_err,
151            ));
152        }
153
154        Ok(mc.unwrap())
155    }
156
157    /// Start the model checker
158    ///
159    /// This function starts the actual model checking process. The flag
160    /// `abort_on_violation` specifies whether a model checker should continue
161    /// after finding the first violation or continue
162    fn verify(
163        self,
164        abort_on_violation: bool,
165    ) -> Result<ModelCheckerResult, Self::ModelCheckingError>;
166}
167
168/// Result type for initialization of a model checker
169#[derive(Debug, Clone, PartialEq)]
170pub enum ModelCheckerSetupError<
171    TE: error::Error,
172    SE: error::Error,
173    CE: error::Error,
174    IE: error::Error,
175> {
176    /// Could not initialize model checker because transformation of threshold
177    /// automaton failed
178    ErrorTransformingTA(TE),
179    /// Could not initialize model checker because transformation of
180    /// specification failed
181    ErrorTransformingSpec(SE),
182    /// Could not initialize model checker because context could not be initialized
183    ErrorContextSetup(CE),
184    /// Error that can occur during initialization
185    ErrorInitializingModelChecker(IE),
186}
187
188impl<TE, SE, CE, IE> fmt::Display for ModelCheckerSetupError<TE, SE, CE, IE>
189where
190    TE: error::Error,
191    SE: error::Error,
192    CE: error::Error,
193    IE: error::Error,
194{
195    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
196        match self {
197            ModelCheckerSetupError::ErrorTransformingTA(e) => write!(
198                f,
199                "Failed to transform threshold automaton into required form for the model checker. Error: {e}"
200            ),
201            ModelCheckerSetupError::ErrorTransformingSpec(e) => write!(
202                f,
203                "Failed to transform specification into the required form for model checking. Error: {e}"
204            ),
205            ModelCheckerSetupError::ErrorContextSetup(e) => {
206                write!(f, "Failed to setup model checking context. Error: {e}")
207            }
208            ModelCheckerSetupError::ErrorInitializingModelChecker(e) => {
209                write!(f, "Failed to initialize the model checker. Error: {e}")
210            }
211        }
212    }
213}
214
215impl<TE, SE, CE, IE> error::Error for ModelCheckerSetupError<TE, SE, CE, IE>
216where
217    TE: error::Error,
218    SE: error::Error,
219    CE: error::Error,
220    IE: error::Error,
221{
222}
223
224/// Result type for a model checking run
225#[derive(Debug, Clone, PartialEq)]
226pub enum ModelCheckerResult {
227    /// Threshold automaton fulfills all specifications
228    SAFE,
229    /// Threshold automaton does not fulfill the specification
230    ///
231    /// The string contains the name of the violated specification and the path
232    /// is a concrete error path that serves as an example for the violation
233    UNSAFE(Vec<(String, Box<Path>)>),
234    /// Model checker could not determine if the specification holds or not
235    ///
236    /// The vector contains the names of the specifications for which the result
237    /// could not be determined.
238    UNKNOWN(Vec<String>),
239}
240
241impl ModelCheckerResult {
242    /// Check whether the model checker returned safe
243    pub fn is_safe(&self) -> bool {
244        matches!(self, ModelCheckerResult::SAFE)
245    }
246}
247
248/// Trait that needs to be implemented by an internal specification
249/// representation
250pub trait SpecificationTrait<C: ModelCheckerContext>: Sized + fmt::Debug {
251    /// Error occurring when transformation from ELTL specification fails
252    type TransformationError: error::Error + Sized;
253    /// Internal specification type the model checker works on
254    type InternalSpecType: Sized + TargetSpec;
255
256    /// Try to derive the specification type from ELTL specification
257    fn try_from_eltl(
258        spec: impl Iterator<Item = (String, ELTLExpression)>,
259        ctx: &C,
260    ) -> Result<Vec<Self>, Self::TransformationError>;
261
262    /// Create threshold automata to check
263    ///
264    /// This function allows to pair a specification with a threshold automaton
265    fn transform_threshold_automaton<TA: ThresholdAutomaton + ModifiableThresholdAutomaton>(
266        ta: TA,
267        specs: Vec<Self>,
268        ctx: &C,
269    ) -> Vec<(Self::InternalSpecType, TA)>;
270}
271
272/// Common trait implemented by types that specify a target configuration
273/// in model checking
274///
275/// This trait is mostly used in preprocessing to ensure target locations are not
276/// removed by accident
277pub trait TargetSpec: Display {
278    /// Get the locations that appear in the target
279    ///
280    /// This function can be used in the preprocessing to ensure no locations
281    /// from the specification are removed
282    fn get_locations_in_target(&self) -> impl IntoIterator<Item = &Location>;
283
284    /// Get the variable constraints that appear in target
285    ///
286    /// This function can be used to get the interval constraints of variables
287    /// in the target specification.
288    fn get_variable_constraint(&self) -> impl IntoIterator<Item = &LIAVariableConstraint>;
289}
290
291/// Trait that needs to be implemented by an internal threshold automaton
292/// representation
293pub trait TATrait<MC: ModelCheckerContext, SC>: ThresholdAutomaton + Sized + fmt::Debug {
294    /// Error type that can occur when trying to convert from threshold automaton
295    type TransformationError: error::Error;
296
297    /// Try to derive the internal threshold automaton representation from a
298    /// general threshold automaton
299    fn try_from_general_ta(
300        ta: GeneralThresholdAutomaton,
301        ctx: &MC,
302        spec_ctx: &SC,
303    ) -> Result<Vec<Self>, Self::TransformationError>;
304}
305
306/// Trait of contexts for model checker
307///
308/// A context to a model checker supplies backend functionality such as, for
309/// example an SMT solver to the model checker
310pub trait ModelCheckerContext: Sized + Clone + fmt::Debug {
311    /// Possible error that can occur during creation of the context
312    type CreationError: error::Error;
313    /// Options for the model checker context
314    type ContextOptions;
315
316    /// Create a new model checking context
317    ///
318    /// Tries to create a new context with the given options
319    fn try_new(opt: Option<Self::ContextOptions>) -> Result<Self, Self::CreationError>;
320}
321
322/// Implement ModelCheckerContext for the SMT solver builder
323impl ModelCheckerContext for SMTSolverBuilder {
324    type CreationError = SMTSolverBuilderError;
325    type ContextOptions = SMTSolverBuilderCfg;
326
327    fn try_new(opt: Option<Self::ContextOptions>) -> Result<Self, Self::CreationError> {
328        if let Some(cfg) = opt {
329            return SMTSolverBuilder::new(&cfg);
330        }
331        SMTSolverBuilder::new_automatic_selection()
332    }
333}
334
335/// Simple context for model checkers containing SMT solver and BDD manager
336#[derive(Clone, Debug)]
337pub struct SMTBddContext {
338    /// Builder to construct new SMT solvers.
339    smt_solver_builder: SMTSolverBuilder,
340    /// The BDD manager to use for the model checking.
341    bdd_manager: BDDManager,
342}
343impl SMTBddContext {
344    /// returns the smt_solver_builder
345    pub fn smt_solver_builder(&self) -> &SMTSolverBuilder {
346        &self.smt_solver_builder
347    }
348    /// returns the bdd_manager
349    pub fn bdd_manager(&self) -> &BDDManager {
350        &self.bdd_manager
351    }
352}
353
354impl ProvidesSMTSolverBuilder for SMTBddContext {
355    fn get_solver_builder(&self) -> SMTSolverBuilder {
356        self.smt_solver_builder.clone()
357    }
358}
359
360impl ModelCheckerContext for SMTBddContext {
361    type CreationError = SMTSolverBuilderError;
362
363    type ContextOptions = (Option<SMTSolverBuilderCfg>, Option<BDDManagerConfig>);
364
365    fn try_new(opt: Option<Self::ContextOptions>) -> Result<Self, Self::CreationError> {
366        let (smt_cfg, bdd_cfg) = opt.unwrap_or((None, None));
367
368        let bdd_mgr = bdd_cfg
369            .map(|cfg| cfg.mgr_from_config())
370            .unwrap_or_else(BDDManager::default);
371
372        let smt_solver_builder = smt_cfg
373            .map(|cfg| SMTSolverBuilder::new(&cfg))
374            .unwrap_or_else(SMTSolverBuilder::new_automatic_selection)?;
375
376        Ok(Self {
377            smt_solver_builder,
378            bdd_manager: bdd_mgr,
379        })
380    }
381}
382
383impl<C: ModelCheckerContext, SC> TATrait<C, SC> for GeneralThresholdAutomaton {
384    type TransformationError = DummyError;
385
386    fn try_from_general_ta(
387        ta: GeneralThresholdAutomaton,
388        _ctx: &C,
389        _spec_ctx: &SC,
390    ) -> Result<Vec<Self>, Self::TransformationError> {
391        Ok(vec![ta])
392    }
393}
394
395impl<C: ModelCheckerContext, SC> TATrait<C, SC> for LIAThresholdAutomaton {
396    type TransformationError = LIATransformationError;
397
398    fn try_from_general_ta(
399        ta: GeneralThresholdAutomaton,
400        _ctx: &C,
401        _spec_ctx: &SC,
402    ) -> Result<Vec<Self>, Self::TransformationError> {
403        let lta = LIAThresholdAutomaton::try_from(ta)?;
404
405        Ok(vec![lta])
406    }
407}
408
409/// Error that should never be built
410#[derive(Debug)]
411pub struct DummyError {}
412
413impl fmt::Display for DummyError {
414    fn fmt(&self, _f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
415        unreachable!("This error should never have been built")
416    }
417}
418
419impl error::Error for DummyError {}
420
421#[cfg(test)]
422mod tests {
423    use taco_smt_encoder::{SMTSolverBuilder, SMTSolverBuilderCfg};
424    use taco_threshold_automaton::{
425        BooleanVarConstraint, LocationConstraint, ParameterConstraint,
426        expressions::{ComparisonOp, IntegerExpression, IntegerOp, Location, Parameter, Variable},
427        general_threshold_automaton::{
428            Action, GeneralThresholdAutomaton,
429            builder::{GeneralThresholdAutomatonBuilder, RuleBuilder},
430        },
431        lia_threshold_automaton::LIAThresholdAutomaton,
432    };
433
434    use crate::TATrait;
435
436    #[test]
437    fn test_try_from_for_general_gta() {
438        let ta = GeneralThresholdAutomatonBuilder::new("test_ta1")
439            .with_parameters(vec![
440                Parameter::new("n"),
441                Parameter::new("t"),
442                Parameter::new("f"),
443            ])
444            .unwrap()
445            .with_variables(vec![
446                Variable::new("var1"),
447                Variable::new("var2"),
448                Variable::new("var3"),
449            ])
450            .unwrap()
451            .with_locations(vec![
452                Location::new("loc1"),
453                Location::new("loc2"),
454                Location::new("loc3"),
455            ])
456            .unwrap()
457            .initialize()
458            .with_initial_variable_constraints(vec![BooleanVarConstraint::ComparisonExpression(
459                Box::new(IntegerExpression::Atom(Variable::new("var1"))),
460                ComparisonOp::Eq,
461                Box::new(IntegerExpression::Const(1)),
462            )])
463            .unwrap()
464            .with_initial_location_constraints(vec![
465                LocationConstraint::ComparisonExpression(
466                    Box::new(IntegerExpression::Atom(Location::new("loc1"))),
467                    ComparisonOp::Eq,
468                    Box::new(
469                        IntegerExpression::Param(Parameter::new("n"))
470                            - IntegerExpression::Param(Parameter::new("f")),
471                    ),
472                ) | LocationConstraint::ComparisonExpression(
473                    Box::new(IntegerExpression::Atom(Location::new("loc2"))),
474                    ComparisonOp::Eq,
475                    Box::new(IntegerExpression::Const(0)),
476                ),
477            ])
478            .unwrap()
479            .with_resilience_conditions(vec![ParameterConstraint::ComparisonExpression(
480                Box::new(IntegerExpression::Atom(Parameter::new("n"))),
481                ComparisonOp::Gt,
482                Box::new(IntegerExpression::BinaryExpr(
483                    Box::new(IntegerExpression::Const(3)),
484                    IntegerOp::Mul,
485                    Box::new(IntegerExpression::Atom(Parameter::new("f"))),
486                )),
487            )])
488            .unwrap()
489            .with_rules(vec![
490                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc2"))
491                    .with_actions(vec![
492                        Action::new(
493                            Variable::new("var1"),
494                            IntegerExpression::Atom(Variable::new("var1")),
495                        )
496                        .unwrap(),
497                    ])
498                    .build(),
499                RuleBuilder::new(1, Location::new("loc2"), Location::new("loc3"))
500                    .with_guard(
501                        BooleanVarConstraint::ComparisonExpression(
502                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
503                            ComparisonOp::Eq,
504                            Box::new(IntegerExpression::Const(1)),
505                        ) & BooleanVarConstraint::ComparisonExpression(
506                            Box::new(IntegerExpression::Atom(Variable::new("var2"))),
507                            ComparisonOp::Eq,
508                            Box::new(IntegerExpression::Param(Parameter::new("n"))),
509                        ),
510                    )
511                    .with_actions(vec![
512                        Action::new(Variable::new("var3"), IntegerExpression::Const(0)).unwrap(),
513                        Action::new(
514                            Variable::new("var1"),
515                            IntegerExpression::BinaryExpr(
516                                Box::new(IntegerExpression::Atom(Variable::new("var1"))),
517                                IntegerOp::Add,
518                                Box::new(IntegerExpression::Const(1)),
519                            ),
520                        )
521                        .unwrap(),
522                    ])
523                    .build(),
524            ])
525            .unwrap()
526            .build();
527
528        let ctx = SMTSolverBuilder::new(&SMTSolverBuilderCfg::new_z3()).unwrap();
529        let got_ta = GeneralThresholdAutomaton::try_from_general_ta(ta.clone(), &ctx, &()).unwrap();
530
531        assert_eq!(got_ta, vec![ta])
532    }
533
534    #[test]
535    fn test_try_from_for_general_lta() {
536        let ta = GeneralThresholdAutomatonBuilder::new("test_ta1")
537            .with_parameters(vec![
538                Parameter::new("n"),
539                Parameter::new("t"),
540                Parameter::new("f"),
541            ])
542            .unwrap()
543            .with_variables(vec![
544                Variable::new("var1"),
545                Variable::new("var2"),
546                Variable::new("var3"),
547            ])
548            .unwrap()
549            .with_locations(vec![
550                Location::new("loc1"),
551                Location::new("loc2"),
552                Location::new("loc3"),
553            ])
554            .unwrap()
555            .initialize()
556            .with_initial_variable_constraints(vec![BooleanVarConstraint::ComparisonExpression(
557                Box::new(IntegerExpression::Atom(Variable::new("var1"))),
558                ComparisonOp::Eq,
559                Box::new(IntegerExpression::Const(1)),
560            )])
561            .unwrap()
562            .with_initial_location_constraints(vec![
563                LocationConstraint::ComparisonExpression(
564                    Box::new(IntegerExpression::Atom(Location::new("loc1"))),
565                    ComparisonOp::Eq,
566                    Box::new(
567                        IntegerExpression::Param(Parameter::new("n"))
568                            - IntegerExpression::Param(Parameter::new("f")),
569                    ),
570                ) | LocationConstraint::ComparisonExpression(
571                    Box::new(IntegerExpression::Atom(Location::new("loc2"))),
572                    ComparisonOp::Eq,
573                    Box::new(IntegerExpression::Const(0)),
574                ),
575            ])
576            .unwrap()
577            .with_resilience_conditions(vec![ParameterConstraint::ComparisonExpression(
578                Box::new(IntegerExpression::Atom(Parameter::new("n"))),
579                ComparisonOp::Gt,
580                Box::new(IntegerExpression::BinaryExpr(
581                    Box::new(IntegerExpression::Const(3)),
582                    IntegerOp::Mul,
583                    Box::new(IntegerExpression::Atom(Parameter::new("f"))),
584                )),
585            )])
586            .unwrap()
587            .with_rules(vec![
588                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc2"))
589                    .with_actions(vec![
590                        Action::new(
591                            Variable::new("var1"),
592                            IntegerExpression::Atom(Variable::new("var1")),
593                        )
594                        .unwrap(),
595                    ])
596                    .build(),
597                RuleBuilder::new(1, Location::new("loc2"), Location::new("loc3"))
598                    .with_guard(
599                        BooleanVarConstraint::ComparisonExpression(
600                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
601                            ComparisonOp::Eq,
602                            Box::new(IntegerExpression::Const(1)),
603                        ) & BooleanVarConstraint::ComparisonExpression(
604                            Box::new(IntegerExpression::Atom(Variable::new("var2"))),
605                            ComparisonOp::Eq,
606                            Box::new(IntegerExpression::Param(Parameter::new("n"))),
607                        ),
608                    )
609                    .with_actions(vec![
610                        Action::new(Variable::new("var3"), IntegerExpression::Const(0)).unwrap(),
611                        Action::new(
612                            Variable::new("var1"),
613                            IntegerExpression::BinaryExpr(
614                                Box::new(IntegerExpression::Atom(Variable::new("var1"))),
615                                IntegerOp::Add,
616                                Box::new(IntegerExpression::Const(1)),
617                            ),
618                        )
619                        .unwrap(),
620                    ])
621                    .build(),
622            ])
623            .unwrap()
624            .build();
625
626        let ctx = SMTSolverBuilder::new(&SMTSolverBuilderCfg::new_z3()).unwrap();
627        let got_ta = LIAThresholdAutomaton::try_from_general_ta(ta.clone(), &ctx, &()).unwrap();
628
629        let lta = ta.try_into().unwrap();
630
631        assert_eq!(got_ta, vec![lta])
632    }
633}
taco_model_checker/lib.rs

taco_model_checker/
lib.rs
