Struct stateright::Property

pub struct Property<M: Model> {
    pub expectation: Expectation,
    pub name: &'static str,
    pub condition: fn(_: &M, _: &M::State) -> bool,
}

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>

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.

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.

pub fn sometimes(
    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.