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

taco_model_checker/
lib.rs
