Trait ModelChecker 

pub trait ModelChecker: Sized {
    type ModelCheckerContext: ModelCheckerContext;
    type ModelCheckerOptions;
    type SpecType: SpecificationTrait<Self::ModelCheckerContext>;
    type ThresholdAutomatonType: TATrait<ContextOf<Self>, InternalSpecOf<Self>>;
    type InitializationError: Error;
    type ModelCheckingError: Error;

    // Required methods
    fn initialize(
        opts: Self::ModelCheckerOptions,
        ta_spec: TASpecOf<Self>,
        unknown: Vec<String>,
        ctx: Self::ModelCheckerContext,
    ) -> Result<Self, Self::InitializationError>;
    fn verify(
        self,
        abort_on_violation: bool,
    ) -> Result<ModelCheckerResult, Self::ModelCheckingError>;

    // Provided method
    fn new(
        ctx_opts: Option<ContextOptionsOf<Self>>,
        mc_opts: Self::ModelCheckerOptions,
        preprocessors: Vec<PreprocessorOf<Self>>,
        ta: GeneralThresholdAutomaton,
        spec: impl Iterator<Item = (String, ELTLExpression)>,
    ) -> Result<Self, ModelCheckerSetupError<Self>> { ... }
}

The ModelChecker trait defines the interface for all model checkers in TACO.

Required Associated Types

type ModelCheckerContext: ModelCheckerContext

Context for the model checker which for example includes interfaces to create solvers or BDD libraries

type ModelCheckerOptions

Options for the model checker

type SpecType: SpecificationTrait<Self::ModelCheckerContext>

Internal specification representation the model checker uses

type ThresholdAutomatonType: TATrait<ContextOf<Self>, InternalSpecOf<Self>>

Internal representation of a threshold automaton the model checker works on

type InitializationError: Error

Error type for errors that can occur during initialization of the model checker

type ModelCheckingError: Error

Error type for errors that can occur during the run of the model checker

Required Methods

fn initialize( opts: Self::ModelCheckerOptions, ta_spec: TASpecOf<Self>, unknown: Vec<String>, ctx: Self::ModelCheckerContext, ) -> Result<Self, Self::InitializationError>

Initialize the model checker with the internal threshold automaton and specification representation

This function needs to be implemented by all model checkers and should setup the model checker with the appropriate options, system and specification representation, as well as the context containing backend functionality like SMT solver configurations.

unknown contains the names of properties that could not be translated into the internal specification. They must be reported as unknown by the model checker.

fn verify( self, abort_on_violation: bool, ) -> Result<ModelCheckerResult, Self::ModelCheckingError>

Start the model checker

This function starts the actual model checking process. The flag abort_on_violation specifies whether a model checker should continue after finding the first violation or continue

Provided Methods

fn new( ctx_opts: Option<ContextOptionsOf<Self>>, mc_opts: Self::ModelCheckerOptions, preprocessors: Vec<PreprocessorOf<Self>>, ta: GeneralThresholdAutomaton, spec: impl Iterator<Item = (String, ELTLExpression)>, ) -> Result<Self, ModelCheckerSetupError<Self>>

Construct a new instance of the model checker

This function will first try to construct the model checker context, then try to transform the threshold automaton into the internal type of the model checker, after which it will attempt to convert the specification into the internal type of the model checker.

If any of these steps fail, or are not possible a ModelCheckerSetupError will be returned that contains the error of the stage it occurred.

If the function returns an Ok, the model checker has been initialized with the threshold automaton and specification and is ready to be checked.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors