Struct ACSModelChecker 

pub struct ACSModelChecker {
    pub(crate) ta_spec: Vec<(DisjunctionTargetConfig, Vec<IntervalThresholdAutomaton>)>,
    pub(crate) ctx: SMTSolverBuilder,
}

Counter system based model checker

This crate implements a counter system based model checker as described in the paper “Parameterized Verification of Round-based Distributed Algorithms via Extended Threshold Automata”. This model checker will construct the explicit counter system (ACS in the paper), starting from potential error states and checking whether an initial state is reachable. If a path is found, the SMT checker will be used to check whether the path is spurious.

Note that this model checker does not support “reachability” specifications, i.e. specifications, that require a location to be not covered by any process.

Fields

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

Threshold automata and specifications to check

ctx: SMTSolverBuilder

SMT solver builder used for spurious checks

Trait Implementations

impl Clone for ACSModelChecker

fn clone(&self) -> ACSModelChecker

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ACSModelChecker

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

Formats the value using the given formatter.

impl ModelChecker for ACSModelChecker

type ModelCheckerContext = SMTSolverBuilder

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

type ModelCheckerOptions = Option<()>

Options for the model checker

type SpecType = ReachabilityProperty

Internal specification representation the model checker uses

type ThresholdAutomatonType = IntervalThresholdAutomaton

Internal representation of a threshold automaton the model checker works on

type InitializationError = ACSModelCheckerInitializationError

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

type ModelCheckingError = DummyError

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

fn initialize( _mode: 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

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