Struct stateright::Property
source · pub struct Property<M: Model> {
pub expectation: Expectation,
pub name: &'static str,
pub condition: fn(_: &M, _: &M::State) -> bool,
}
Expand description
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§
source§impl<M: Model> Property<M>
impl<M: Model> Property<M>
sourcepub fn always(
name: &'static str,
condition: fn(_: &M, _: &M::State) -> bool
) -> Property<M>
pub fn always( 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.
sourcepub fn eventually(
name: &'static str,
condition: fn(_: &M, _: &M::State) -> bool
) -> Property<M>
pub fn eventually( 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.