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 the specification
228    SAFE,
229    /// Threshold automaton does not fulfill the specification
230    /// The string contains the name of the violated specification and the path
231    /// is a concrete error path that serves as an example for the violation
232    UNSAFE(Vec<(String, Box<Path>)>),
233    /// The model checker could not determine if the specification holds or not.
234    /// The vector contains the names of the specifications that are unknown
235    UNKNOWN(Vec<String>),
236}
237
238impl ModelCheckerResult {
239    /// Check whether the model checker returned safe
240    pub fn is_safe(&self) -> bool {
241        matches!(self, ModelCheckerResult::SAFE)
242    }
243}
244
245/// Trait that needs to be implemented by an internal specification
246/// representation
247pub trait SpecificationTrait<C: ModelCheckerContext>: Sized + fmt::Debug {
248    /// Error occurring when transformation from ELTL specification fails
249    type TransformationError: error::Error + Sized;
250    /// Internal specification type the model checker works on
251    type InternalSpecType: Sized + TargetSpec;
252
253    /// Try to derive the specification type from ELTL specification
254    fn try_from_eltl(
255        spec: impl Iterator<Item = (String, ELTLExpression)>,
256        ctx: &C,
257    ) -> Result<Vec<Self>, Self::TransformationError>;
258
259    /// Create threshold automata to check
260    ///
261    /// This function allows to pair a specification with a threshold automaton
262    fn transform_threshold_automaton<TA: ThresholdAutomaton + ModifiableThresholdAutomaton>(
263        ta: TA,
264        specs: Vec<Self>,
265        ctx: &C,
266    ) -> Vec<(Self::InternalSpecType, TA)>;
267}
268
269/// Common trait implemented by types that specify a target configuration
270/// in model checking
271///
272/// This trait is mostly used in preprocessing to ensure target locations are not
273/// removed by accident
274pub trait TargetSpec: Display {
275    /// Get the locations that appear in the target
276    ///
277    /// This function can be used in the preprocessing to ensure no locations
278    /// from the specification are removed
279    fn get_locations_in_target(&self) -> impl IntoIterator<Item = &Location>;
280
281    /// Get the variable constraints that appear in target
282    ///
283    /// This function can be used to get the interval constraints of variables
284    /// in the target specification.
285    fn get_variable_constraint(&self) -> impl IntoIterator<Item = &LIAVariableConstraint>;
286}
287
288/// Trait that needs to be implemented by an internal threshold automaton
289/// representation
290pub trait TATrait<MC: ModelCheckerContext, SC>: ThresholdAutomaton + Sized + fmt::Debug {
291    /// Error type that can occur when trying to convert from threshold automaton
292    type TransformationError: error::Error;
293
294    /// Try to derive the internal threshold automaton representation from a
295    /// general threshold automaton
296    fn try_from_general_ta(
297        ta: GeneralThresholdAutomaton,
298        ctx: &MC,
299        spec_ctx: &SC,
300    ) -> Result<Vec<Self>, Self::TransformationError>;
301}
302
303/// Trait of contexts for model checker
304///
305/// A context to a model checker supplies backend functionality such as, for
306/// example an SMT solver to the model checker
307pub trait ModelCheckerContext: Sized + Clone + fmt::Debug {
308    /// Possible error that can occur during creation of the context
309    type CreationError: error::Error;
310    /// Options for the model checker context
311    type ContextOptions;
312
313    /// Create a new model checking context
314    ///
315    /// Tries to create a new context with the given options
316    fn try_new(opt: Option<Self::ContextOptions>) -> Result<Self, Self::CreationError>;
317}
318
319/// Implement ModelCheckerContext for the SMT solver builder
320impl ModelCheckerContext for SMTSolverBuilder {
321    type CreationError = SMTSolverBuilderError;
322    type ContextOptions = SMTSolverBuilderCfg;
323
324    fn try_new(opt: Option<Self::ContextOptions>) -> Result<Self, Self::CreationError> {
325        if let Some(cfg) = opt {
326            return SMTSolverBuilder::new(&cfg);
327        }
328        SMTSolverBuilder::new_automatic_selection()
329    }
330}
331
332/// Simple context for model checkers containing SMT solver and BDD manager
333#[derive(Clone, Debug)]
334pub struct SMTBddContext {
335    /// Builder to construct new SMT solvers.
336    smt_solver_builder: SMTSolverBuilder,
337    /// The BDD manager to use for the model checking.
338    bdd_manager: BDDManager,
339}
340impl SMTBddContext {
341    /// returns the smt_solver_builder
342    pub fn smt_solver_builder(&self) -> &SMTSolverBuilder {
343        &self.smt_solver_builder
344    }
345    /// returns the bdd_manager
346    pub fn bdd_manager(&self) -> &BDDManager {
347        &self.bdd_manager
348    }
349}
350
351impl ProvidesSMTSolverBuilder for SMTBddContext {
352    fn get_solver_builder(&self) -> SMTSolverBuilder {
353        self.smt_solver_builder.clone()
354    }
355}
356
357impl ModelCheckerContext for SMTBddContext {
358    type CreationError = SMTSolverBuilderError;
359
360    type ContextOptions = (Option<SMTSolverBuilderCfg>, Option<BDDManagerConfig>);
361
362    fn try_new(opt: Option<Self::ContextOptions>) -> Result<Self, Self::CreationError> {
363        let (smt_cfg, bdd_cfg) = opt.unwrap_or((None, None));
364
365        let bdd_mgr = bdd_cfg
366            .map(|cfg| cfg.mgr_from_config())
367            .unwrap_or_else(BDDManager::default);
368
369        let smt_solver_builder = smt_cfg
370            .map(|cfg| SMTSolverBuilder::new(&cfg))
371            .unwrap_or_else(SMTSolverBuilder::new_automatic_selection)?;
372
373        Ok(Self {
374            smt_solver_builder,
375            bdd_manager: bdd_mgr,
376        })
377    }
378}
379
380impl<C: ModelCheckerContext, SC> TATrait<C, SC> for GeneralThresholdAutomaton {
381    type TransformationError = DummyError;
382
383    fn try_from_general_ta(
384        ta: GeneralThresholdAutomaton,
385        _ctx: &C,
386        _spec_ctx: &SC,
387    ) -> Result<Vec<Self>, Self::TransformationError> {
388        Ok(vec![ta])
389    }
390}
391
392impl<C: ModelCheckerContext, SC> TATrait<C, SC> for LIAThresholdAutomaton {
393    type TransformationError = LIATransformationError;
394
395    fn try_from_general_ta(
396        ta: GeneralThresholdAutomaton,
397        _ctx: &C,
398        _spec_ctx: &SC,
399    ) -> Result<Vec<Self>, Self::TransformationError> {
400        let lta = LIAThresholdAutomaton::try_from(ta)?;
401
402        Ok(vec![lta])
403    }
404}
405
406/// Error that should never be built
407#[derive(Debug)]
408pub struct DummyError {}
409
410impl fmt::Display for DummyError {
411    fn fmt(&self, _f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
412        unreachable!("This error should never have been built")
413    }
414}
415
416impl error::Error for DummyError {}
417
418#[cfg(test)]
419mod tests {
420    use taco_smt_encoder::{SMTSolverBuilder, SMTSolverBuilderCfg};
421    use taco_threshold_automaton::{
422        BooleanVarConstraint, LocationConstraint, ParameterConstraint,
423        expressions::{ComparisonOp, IntegerExpression, IntegerOp, Location, Parameter, Variable},
424        general_threshold_automaton::{
425            Action, GeneralThresholdAutomaton,
426            builder::{GeneralThresholdAutomatonBuilder, RuleBuilder},
427        },
428        lia_threshold_automaton::LIAThresholdAutomaton,
429    };
430
431    use crate::TATrait;
432
433    #[test]
434    fn test_try_from_for_general_gta() {
435        let ta = GeneralThresholdAutomatonBuilder::new("test_ta1")
436            .with_parameters(vec![
437                Parameter::new("n"),
438                Parameter::new("t"),
439                Parameter::new("f"),
440            ])
441            .unwrap()
442            .with_variables(vec![
443                Variable::new("var1"),
444                Variable::new("var2"),
445                Variable::new("var3"),
446            ])
447            .unwrap()
448            .with_locations(vec![
449                Location::new("loc1"),
450                Location::new("loc2"),
451                Location::new("loc3"),
452            ])
453            .unwrap()
454            .initialize()
455            .with_initial_variable_constraints(vec![BooleanVarConstraint::ComparisonExpression(
456                Box::new(IntegerExpression::Atom(Variable::new("var1"))),
457                ComparisonOp::Eq,
458                Box::new(IntegerExpression::Const(1)),
459            )])
460            .unwrap()
461            .with_initial_location_constraints(vec![
462                LocationConstraint::ComparisonExpression(
463                    Box::new(IntegerExpression::Atom(Location::new("loc1"))),
464                    ComparisonOp::Eq,
465                    Box::new(
466                        IntegerExpression::Param(Parameter::new("n"))
467                            - IntegerExpression::Param(Parameter::new("f")),
468                    ),
469                ) | LocationConstraint::ComparisonExpression(
470                    Box::new(IntegerExpression::Atom(Location::new("loc2"))),
471                    ComparisonOp::Eq,
472                    Box::new(IntegerExpression::Const(0)),
473                ),
474            ])
475            .unwrap()
476            .with_resilience_conditions(vec![ParameterConstraint::ComparisonExpression(
477                Box::new(IntegerExpression::Atom(Parameter::new("n"))),
478                ComparisonOp::Gt,
479                Box::new(IntegerExpression::BinaryExpr(
480                    Box::new(IntegerExpression::Const(3)),
481                    IntegerOp::Mul,
482                    Box::new(IntegerExpression::Atom(Parameter::new("f"))),
483                )),
484            )])
485            .unwrap()
486            .with_rules(vec![
487                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc2"))
488                    .with_actions(vec![
489                        Action::new(
490                            Variable::new("var1"),
491                            IntegerExpression::Atom(Variable::new("var1")),
492                        )
493                        .unwrap(),
494                    ])
495                    .build(),
496                RuleBuilder::new(1, Location::new("loc2"), Location::new("loc3"))
497                    .with_guard(
498                        BooleanVarConstraint::ComparisonExpression(
499                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
500                            ComparisonOp::Eq,
501                            Box::new(IntegerExpression::Const(1)),
502                        ) & BooleanVarConstraint::ComparisonExpression(
503                            Box::new(IntegerExpression::Atom(Variable::new("var2"))),
504                            ComparisonOp::Eq,
505                            Box::new(IntegerExpression::Param(Parameter::new("n"))),
506                        ),
507                    )
508                    .with_actions(vec![
509                        Action::new(Variable::new("var3"), IntegerExpression::Const(0)).unwrap(),
510                        Action::new(
511                            Variable::new("var1"),
512                            IntegerExpression::BinaryExpr(
513                                Box::new(IntegerExpression::Atom(Variable::new("var1"))),
514                                IntegerOp::Add,
515                                Box::new(IntegerExpression::Const(1)),
516                            ),
517                        )
518                        .unwrap(),
519                    ])
520                    .build(),
521            ])
522            .unwrap()
523            .build();
524
525        let ctx = SMTSolverBuilder::new(&SMTSolverBuilderCfg::new_z3()).unwrap();
526        let got_ta = GeneralThresholdAutomaton::try_from_general_ta(ta.clone(), &ctx, &()).unwrap();
527
528        assert_eq!(got_ta, vec![ta])
529    }
530
531    #[test]
532    fn test_try_from_for_general_lta() {
533        let ta = GeneralThresholdAutomatonBuilder::new("test_ta1")
534            .with_parameters(vec![
535                Parameter::new("n"),
536                Parameter::new("t"),
537                Parameter::new("f"),
538            ])
539            .unwrap()
540            .with_variables(vec![
541                Variable::new("var1"),
542                Variable::new("var2"),
543                Variable::new("var3"),
544            ])
545            .unwrap()
546            .with_locations(vec![
547                Location::new("loc1"),
548                Location::new("loc2"),
549                Location::new("loc3"),
550            ])
551            .unwrap()
552            .initialize()
553            .with_initial_variable_constraints(vec![BooleanVarConstraint::ComparisonExpression(
554                Box::new(IntegerExpression::Atom(Variable::new("var1"))),
555                ComparisonOp::Eq,
556                Box::new(IntegerExpression::Const(1)),
557            )])
558            .unwrap()
559            .with_initial_location_constraints(vec![
560                LocationConstraint::ComparisonExpression(
561                    Box::new(IntegerExpression::Atom(Location::new("loc1"))),
562                    ComparisonOp::Eq,
563                    Box::new(
564                        IntegerExpression::Param(Parameter::new("n"))
565                            - IntegerExpression::Param(Parameter::new("f")),
566                    ),
567                ) | LocationConstraint::ComparisonExpression(
568                    Box::new(IntegerExpression::Atom(Location::new("loc2"))),
569                    ComparisonOp::Eq,
570                    Box::new(IntegerExpression::Const(0)),
571                ),
572            ])
573            .unwrap()
574            .with_resilience_conditions(vec![ParameterConstraint::ComparisonExpression(
575                Box::new(IntegerExpression::Atom(Parameter::new("n"))),
576                ComparisonOp::Gt,
577                Box::new(IntegerExpression::BinaryExpr(
578                    Box::new(IntegerExpression::Const(3)),
579                    IntegerOp::Mul,
580                    Box::new(IntegerExpression::Atom(Parameter::new("f"))),
581                )),
582            )])
583            .unwrap()
584            .with_rules(vec![
585                RuleBuilder::new(0, Location::new("loc1"), Location::new("loc2"))
586                    .with_actions(vec![
587                        Action::new(
588                            Variable::new("var1"),
589                            IntegerExpression::Atom(Variable::new("var1")),
590                        )
591                        .unwrap(),
592                    ])
593                    .build(),
594                RuleBuilder::new(1, Location::new("loc2"), Location::new("loc3"))
595                    .with_guard(
596                        BooleanVarConstraint::ComparisonExpression(
597                            Box::new(IntegerExpression::Atom(Variable::new("var1"))),
598                            ComparisonOp::Eq,
599                            Box::new(IntegerExpression::Const(1)),
600                        ) & BooleanVarConstraint::ComparisonExpression(
601                            Box::new(IntegerExpression::Atom(Variable::new("var2"))),
602                            ComparisonOp::Eq,
603                            Box::new(IntegerExpression::Param(Parameter::new("n"))),
604                        ),
605                    )
606                    .with_actions(vec![
607                        Action::new(Variable::new("var3"), IntegerExpression::Const(0)).unwrap(),
608                        Action::new(
609                            Variable::new("var1"),
610                            IntegerExpression::BinaryExpr(
611                                Box::new(IntegerExpression::Atom(Variable::new("var1"))),
612                                IntegerOp::Add,
613                                Box::new(IntegerExpression::Const(1)),
614                            ),
615                        )
616                        .unwrap(),
617                    ])
618                    .build(),
619            ])
620            .unwrap()
621            .build();
622
623        let ctx = SMTSolverBuilder::new(&SMTSolverBuilderCfg::new_z3()).unwrap();
624        let got_ta = LIAThresholdAutomaton::try_from_general_ta(ta.clone(), &ctx, &()).unwrap();
625
626        let lta = ta.try_into().unwrap();
627
628        assert_eq!(got_ta, vec![lta])
629    }
630}
taco_model_checker/lib.rs

taco_model_checker/
lib.rs
