pub struct ModelChecker<T: Float + Debug + Send + Sync + 'static> { /* private fields */ }Expand description
Bounded invariant model checker.
Implementations§
Source§impl<T: Float + Debug + Send + Sync + 'static> ModelChecker<T>
impl<T: Float + Debug + Send + Sync + 'static> ModelChecker<T>
Sourcepub fn set_state_bound(&mut self, state_bound: usize) -> Result<()>
pub fn set_state_bound(&mut self, state_bound: usize) -> Result<()>
Replace the exploration bound.
Sourcepub fn model_mut(&mut self) -> &mut SystemModel<T>
pub fn model_mut(&mut self) -> &mut SystemModel<T>
Mutable access to the system model.
Sourcepub fn add_property(&mut self, property: SystemProperty) -> Result<()>
pub fn add_property(&mut self, property: SystemProperty) -> Result<()>
Register a property to check.
The specification is parsed immediately, so an unsupported property is rejected at registration rather than silently passing later.
Sourcepub fn property_count(&self) -> usize
pub fn property_count(&self) -> usize
Number of registered properties.
Sourcepub fn check_property(
&self,
property: &SystemProperty,
) -> Result<ModelCheckOutcome>
pub fn check_property( &self, property: &SystemProperty, ) -> Result<ModelCheckOutcome>
Check one property.
Sourcepub fn check_all(&self) -> Result<Vec<ModelCheckOutcome>>
pub fn check_all(&self) -> Result<Vec<ModelCheckOutcome>>
Check every registered property.
An empty property set is an error: “zero properties checked” is not the same claim as “the system is correct”.
Trait Implementations§
Auto Trait Implementations§
impl<T> !RefUnwindSafe for ModelChecker<T>
impl<T> !UnwindSafe for ModelChecker<T>
impl<T> Freeze for ModelChecker<T>
impl<T> Send for ModelChecker<T>
impl<T> Sync for ModelChecker<T>
impl<T> Unpin for ModelChecker<T>where
T: Unpin,
impl<T> UnsafeUnpin for ModelChecker<T>
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
impl<ST, DT> CastableFrom<ST, Initialized, Initialized> for DT
impl<ST, DT> CastableFrom<ST, Uninit, Uninit> for DT
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 moreSource§impl<T> Pointable for T
impl<T> Pointable for T
impl<T> Read<Exclusive, BecauseExclusive> for Twhere
T: ?Sized,
Source§impl<SS, SP> SupersetOf<SS> for SPwhere
SS: SubsetOf<SP>,
impl<SS, SP> SupersetOf<SS> for SPwhere
SS: SubsetOf<SP>,
Source§fn to_subset(&self) -> Option<SS>
fn to_subset(&self) -> Option<SS>
The inverse inclusion map: attempts to construct
self from the equivalent element of its
superset. Read moreSource§fn is_in_subset(&self) -> bool
fn is_in_subset(&self) -> bool
Checks if
self is actually part of its subset T (and can be converted to it).Source§fn to_subset_unchecked(&self) -> SS
fn to_subset_unchecked(&self) -> SS
Use with care! Same as
self.to_subset but without any property checks. Always succeeds.Source§fn from_subset(element: &SS) -> SP
fn from_subset(element: &SS) -> SP
The inclusion map: converts
self to the equivalent element of its superset.