Struct SMTModelChecker 

pub struct SMTModelChecker {
    pub(crate) _opts: SMTModelCheckerOptions,
    pub(crate) solver_builder: SMTSolverBuilder,
    pub(crate) ta_spec: Vec<(DisjunctionTargetConfig, Vec<GeneralThresholdAutomaton>)>,
}

Fields

_opts: SMTModelCheckerOptions

solver_builder: SMTSolverBuilder

ta_spec: Vec<(DisjunctionTargetConfig, Vec<GeneralThresholdAutomaton>)>

Implementations

impl SMTModelChecker

pub(crate) fn model_check_non_concurrent( self, abort_on_violation: bool, ) -> Result<ModelCheckerResult, ContextMgrError>

Execute the model checker sequentially

pub(crate) fn model_check_concurrent( self, abort_on_violation: bool, ) -> Result<ModelCheckerResult, ContextMgrError>

Verify all properties concurrently

This method will build a multi-threaded runtime and will attempt to check each property concurrently to attempt to reduce the overall runtime.

TODO: The setup is still very rudimentary and could be fine tuned in the future

pub(crate) async fn wait_for_mc_results( futures: FuturesUnordered<JoinHandle<Result<ModelCheckerResult, ContextMgrError>>>, abort_on_violation: bool, completed_map: HashMap<String, (usize, Arc<AtomicUsize>)>, ) -> Result<ModelCheckerResult, ContextMgrError>

Helper method to collect the results and abort early if desired

pub(crate) async fn check_single_target( ta: GeneralThresholdAutomaton, target: DisjunctionTargetConfig, solver_builder: SMTSolverBuilder, safe_counter: Arc<AtomicUsize>, ) -> Result<ModelCheckerResult, ContextMgrError>

Check reachability of a single [DisjunctionTargetConfig]

impl SMTModelChecker

pub fn new_mc() -> Self

pub fn new_mc_with_opts(opts: SMTModelCheckerOptions) -> Self

Trait Implementations

impl Clone for SMTModelChecker

fn clone(&self) -> SMTModelChecker

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for SMTModelChecker

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for SMTModelChecker

fn default() -> Self

Returns the “default value” for a type.

impl ModelChecker for SMTModelChecker

type ModelCheckerContext = SMTSolverBuilder

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

type ModelCheckerOptions = SMTModelCheckerOptions

Options for the model checker

type SpecType = ReachabilityProperty

Internal specification representation the model checker uses

type ThresholdAutomatonType = GeneralThresholdAutomaton

Internal representation of a threshold automaton the model checker works on

type InitializationError = SMTModelCheckerInitializationError

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

type ModelCheckingError = ContextMgrError

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

fn initialize( opts: Self::ModelCheckerOptions, ta_spec: Vec<(DisjunctionTargetConfig, Vec<Self::ThresholdAutomatonType>)>, ctx: Self::ModelCheckerContext, ) -> Result<Self, Self::InitializationError>

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

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

Start the model checker

fn new( ctx_opts: Option<<Self::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::ThresholdAutomatonType as TATrait<Self::ModelCheckerContext, <Self::SpecType as SpecificationTrait<Self::ModelCheckerContext>>::InternalSpecType>>::TransformationError, <Self::SpecType as SpecificationTrait<Self::ModelCheckerContext>>::TransformationError, <Self::ModelCheckerContext as ModelCheckerContext>::CreationError, Self::InitializationError>>

Construct a new instance of the model checker