Struct Framework

pub struct Framework<M: FullMachine> { /* private fields */ }

Three-valued abstraction refinement framework.

Implementations

impl<M: FullMachine> Framework<M>

pub fn new(abstract_system: M::Abstr, strategy: Strategy) -> Self

Constructs the framework with a given system and strategy.

pub fn verify(&mut self, property: &PreparedProperty) -> Result<bool, ExecError>

pub fn step_verification( &mut self, property: &PreparedProperty, ) -> ControlFlow<Result<bool, ExecError>>

pub fn regenerate(&mut self, from_node_id: NodeId) -> bool

Regenerates the state space from a given node, keeping its other parts. Returns whether the state space changed.

pub fn check_property_with_labelling( &self, property: &PreparedProperty, ) -> Result<(Conclusion, BTreeMap<StateId, ThreeValued>), ExecError>

pub fn find_panic_string(&mut self) -> Option<&'static str>

pub fn reset(&mut self)

pub fn info(&mut self) -> ExecStats

pub fn space(&self) -> &StateSpace<M>

pub fn make_compact(&mut self)