[−][src]Struct stateright::Property
A named predicate, such as "an epoch sometimes has no leader" (for which the the model checker would find an example) or "an epoch always has at most one leader" (for which the model checker would find a counterexample) or "a proposal is eventually accepted" (for which the model checker would find a counterexample path leading from the initial state through to a terminal state).
Fields
expectation: Expectation
name: &'static str
condition: fn(_: &M, _: &M::State) -> bool
Implementations
impl<M: Model> Property<M>
[src]
pub fn always(
name: &'static str,
condition: fn(_: &M, _: &M::State) -> bool
) -> Property<M>
[src]
name: &'static str,
condition: fn(_: &M, _: &M::State) -> bool
) -> Property<M>
An invariant that defines a safety property. The model checker will try to discover a counterexample.
pub fn eventually(
name: &'static str,
condition: fn(_: &M, _: &M::State) -> bool
) -> Property<M>
[src]
name: &'static str,
condition: fn(_: &M, _: &M::State) -> bool
) -> Property<M>
An invariant that defines a liveness property. The model checker will try to discover a counterexample path leading from the initial state through to a terminal state.
Note that in this implementation eventually
properties only work correctly on acyclic
paths (those that end in either states with no successors or checking boundaries). A path
ending in a cycle is not viewed as terminating in that cycle, as the checker does not
differentiate cycles from DAG joins, and so an eventually
property that has not been met
by the cycle-closing edge will ignored -- a false negative.
pub fn sometimes(
name: &'static str,
condition: fn(_: &M, _: &M::State) -> bool
) -> Property<M>
[src]
name: &'static str,
condition: fn(_: &M, _: &M::State) -> bool
) -> Property<M>
Something that should be possible in the model. The model checker will try to discover an example.
Trait Implementations
impl<M: Model> Clone for Property<M>
[src]
pub fn clone(&self) -> Self
[src]
pub fn clone_from(&mut self, source: &Self)
1.0.0[src]
Auto Trait Implementations
impl<M> RefUnwindSafe for Property<M>
[src]
impl<M> Send for Property<M>
[src]
impl<M> Sync for Property<M>
[src]
impl<M> Unpin for Property<M>
[src]
impl<M> UnwindSafe for Property<M>
[src]
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
pub fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
pub fn to_owned(&self) -> T
[src]
pub fn clone_into(&self, target: &mut T)
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
pub fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
pub fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<V, T> VZip<V> for T where
V: MultiLane<T>,
V: MultiLane<T>,