Struct ModelChecker 

pub struct ModelChecker { /* private fields */ }

Main class of (and entrypoint to) the model checking testing technique.

Implementations

impl ModelChecker

pub fn new(sys: &System) -> Self

Creates a new model checker with the specified strategy and initial state equal to the current state of the system.

pub fn run<S: Strategy>(&mut self, strategy_config: StrategyConfig) -> McResult

Runs model checking and returns the result on completion.

pub fn run_with_change<S>( &mut self, strategy_config: StrategyConfig, preliminary_callback: impl FnOnce(&mut McSystem), ) -> McResult

where S: Strategy,

Runs model checking after applying callback.

pub fn run_from_states<S: Strategy>( &mut self, strategy_config: StrategyConfig, states: HashSet<McState>, ) -> McResult

Runs model checking from a set of initial states.

pub fn run_from_states_with_change<S>( &mut self, strategy_config: StrategyConfig, states: HashSet<McState>, preliminary_callback: impl Fn(&mut McSystem), ) -> McResult

where S: Strategy,

Runs model checking from a set of initial states after applying callback.