Trait ModelChecker 

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

    // Required methods
    fn initialize(
        opts: Self::ModelCheckerOptions,
        ta_spec: Vec<(<<Self as ModelChecker>::SpecType as SpecificationTrait<Self::ModelCheckerContext>>::InternalSpecType, Vec<Self::ThresholdAutomatonType>)>,
        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<<<Self as ModelChecker>::ModelCheckerContext as ModelCheckerContext>::ContextOptions>,
        mc_opts: Self::ModelCheckerOptions,
        preprocessors: Vec<Box<dyn Preprocessor<GeneralThresholdAutomaton, <Self::SpecType as SpecificationTrait<Self::ModelCheckerContext>>::InternalSpecType, Self::ModelCheckerContext>>>,
        ta: GeneralThresholdAutomaton,
        spec: impl Iterator<Item = (String, ELTLExpression)>,
    ) -> Result<Self, ModelCheckerSetupError<<<Self as ModelChecker>::ThresholdAutomatonType as TATrait<Self::ModelCheckerContext, <Self::SpecType as SpecificationTrait<Self::ModelCheckerContext>>::InternalSpecType>>::TransformationError, <<Self as ModelChecker>::SpecType as SpecificationTrait<Self::ModelCheckerContext>>::TransformationError, <<Self as ModelChecker>::ModelCheckerContext as ModelCheckerContext>::CreationError, Self::InitializationError>> { ... }
}

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<Self::ModelCheckerContext, <Self::SpecType as SpecificationTrait<Self::ModelCheckerContext>>::InternalSpecType>

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: Vec<(<<Self as ModelChecker>::SpecType as SpecificationTrait<Self::ModelCheckerContext>>::InternalSpecType, Vec<Self::ThresholdAutomatonType>)>, 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.

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<<<Self as ModelChecker>::ModelCheckerContext as ModelCheckerContext>::ContextOptions>, mc_opts: Self::ModelCheckerOptions, preprocessors: Vec<Box<dyn Preprocessor<GeneralThresholdAutomaton, <Self::SpecType as SpecificationTrait<Self::ModelCheckerContext>>::InternalSpecType, Self::ModelCheckerContext>>>, ta: GeneralThresholdAutomaton, spec: impl Iterator<Item = (String, ELTLExpression)>, ) -> Result<Self, ModelCheckerSetupError<<<Self as ModelChecker>::ThresholdAutomatonType as TATrait<Self::ModelCheckerContext, <Self::SpecType as SpecificationTrait<Self::ModelCheckerContext>>::InternalSpecType>>::TransformationError, <<Self as ModelChecker>::SpecType as SpecificationTrait<Self::ModelCheckerContext>>::TransformationError, <<Self as ModelChecker>::ModelCheckerContext as ModelCheckerContext>::CreationError, Self::InitializationError>>

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", so this trait is not object safe.

Implementors