pub struct Framework<M: FullMachine> { /* private fields */ }Expand description
Three-valued abstraction refinement framework.
Implementations§
Source§impl<M: FullMachine> Framework<M>
impl<M: FullMachine> Framework<M>
Sourcepub fn new(abstract_system: M::Abstr, strategy: Strategy) -> Self
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: &Property, ) -> Result<KnownConclusion, ExecError>
pub fn step_verification( &mut self, property: &Property, ) -> ControlFlow<Result<KnownConclusion, ExecError>>
pub fn check_subproperty_with_labelling( &mut self, property: &Subproperty, ) -> Result<(Conclusion, BTreeMap<StateId, ParamValuation>), 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)
Auto Trait Implementations§
impl<M> !Freeze for Framework<M>
impl<M> !RefUnwindSafe for Framework<M>
impl<M> Send for Framework<M>
impl<M> !Sync for Framework<M>
impl<M> Unpin for Framework<M>where
<M as FullMachine>::Abstr: Unpin,
<<M as FullMachine>::Refin as Machine<M>>::Input: Unpin,
<<M as FullMachine>::Refin as Machine<M>>::Param: Unpin,
<<M as FullMachine>::Refin as Machine<M>>::State: Unpin,
<<M as FullMachine>::Abstr as Machine<M>>::Input: Unpin,
<<M as FullMachine>::Abstr as Machine<M>>::Param: Unpin,
<<M as FullMachine>::Abstr as Machine<M>>::State: Unpin,
impl<M> !UnwindSafe for Framework<M>
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
Source§impl<T> IntoEither for T
impl<T> IntoEither for T
Source§fn into_either(self, into_left: bool) -> Either<Self, Self>
fn into_either(self, into_left: bool) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left is true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read moreSource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left(&self) returns true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read more