Struct ZCSModelChecker 

pub struct ZCSModelChecker {
    pub(crate) ctx: SMTBddContext,
    pub(crate) ta_spec: Vec<(DisjunctionTargetConfig, Vec<IntervalThresholdAutomaton>)>,
    pub(crate) heuristics: ZCSModelCheckerHeuristics,
}

This struct defines a symbolic model checker (ZCS model checker) It can be used to check reachability and coverability specifications Depending on the chosen search heuristics:

• it can verify extended threshold automata with a semi-decision procedure
• it can verify canonical threshold automata with a decision procedure

Fields

ctx: SMTBddContext

model checker context

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

specifications to be checked

heuristics: ZCSModelCheckerHeuristics

symbolic model checker heuristics

Implementations

impl ZCSModelChecker

pub(crate) fn compute_zcs<'a>( &'a self, ta: &'a IntervalThresholdAutomaton, ) -> ZCS<'a>

constructs the symbolic 01-CS (ZCS) and initializes the bdd var manager

pub(crate) fn compute_enabled_shared_variable_states( cs: &ZCS<'_>, ta: &IntervalThresholdAutomaton, target_config: &TargetConfig, ) -> ZCSStates

construct the symbolic shared variable state that satisfies the interval constraint of a target configuration

pub(crate) fn compute_error_states( cs: &ZCS<'_>, ta: &IntervalThresholdAutomaton, specification: &DisjunctionTargetConfig, ) -> Result<ZCSStates, ZCSModelCheckerError>

constructs the set of error states for a given spec and 01-CS (ZCS)

pub(crate) fn compute_symbolic_error_graph<'a>( &'a self, ta: &'a IntervalThresholdAutomaton, spec: &DisjunctionTargetConfig, ) -> ZCSErrorGraph<'a>

constructs the symbolic error graph (ZCS error graph) for the underlying 01-CS (ZCS)

impl ZCSModelChecker

pub fn new_mc(ctx: SMTBddContext) -> Self

new symbolic model checker with default settings

Trait Implementations

impl Clone for ZCSModelChecker

fn clone(&self) -> ZCSModelChecker

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ZCSModelChecker

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

Formats the value using the given formatter.

impl Default for ZCSModelChecker

fn default() -> Self

Returns the “default value” for a type.

impl ModelChecker for ZCSModelChecker

type ModelCheckerContext = SMTBddContext

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

type ModelCheckerOptions = Option<ZCSModelCheckerHeuristics>

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 = ZCSModelCheckerInitializationError

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

type ModelCheckingError = ZCSModelCheckerError

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