Trait ReferenceStateMachine 

pub trait ReferenceStateMachine: 'static {
    type State: Clone + Debug;
    type Transition: Clone + Debug;

    // Required methods
    fn init_state() -> BoxedStrategy<Self::State>;
    fn transitions(state: &Self::State) -> BoxedStrategy<Self::Transition>;
    fn apply(state: Self::State, transition: &Self::Transition) -> Self::State;

    // Provided methods
    fn preconditions(state: &Self::State, transition: &Self::Transition) -> bool { ... }
    fn sequential_strategy(
        size: impl Into<SizeRange>,
    ) -> Sequential<Self::State, Self::Transition, BoxedStrategy<Self::State>, BoxedStrategy<Self::Transition>> { ... }
}

This trait is used to model system under test as an abstract state machine.

The key to how this works is that the set of next valid transitions depends on its current state (it’s not the same as generating a random sequence of transitions) and just like other prop strategies, the state machine strategy attempts to shrink the transitions to find the minimal reproducible example when it encounters a case that breaks any of the defined properties.

This is achieved with the ReferenceStateMachine::transitions that takes the current state as an argument and can be used to decide which transitions are valid from this state, together with the ReferenceStateMachine::preconditions, which are checked during generation of transitions and during shrinking.

Hence, the preconditions only needs to contain checks for invariants that depend on the current state and may be broken by shrinking and it doesn’t need to cover invariants that do not depend on the current state.

The reference state machine generation runs before the generated transitions are attempted to be executed against the SUT (the concrete state machine) as defined by crate::StateMachineTest.

Required Associated Types

type State: Clone + Debug

The reference state machine’s state type. This should contain the minimum required information needed to implement the state machine. It is used to drive the generations of transitions to decide which transitions are valid for the current state.

type Transition: Clone + Debug

The reference state machine’s transition type. This is typically an enum with its variants containing the parameters required to apply the transition, if any.

Required Methods

fn init_state() -> BoxedStrategy<Self::State>

The initial state may be generated by any strategy. For a constant initial state, use proptest::strategy::Just.

fn transitions(state: &Self::State) -> BoxedStrategy<Self::Transition>

Generate the initial transitions.

fn apply(state: Self::State, transition: &Self::Transition) -> Self::State

Apply a transition in the reference state.

Provided Methods

fn preconditions(state: &Self::State, transition: &Self::Transition) -> bool

Pre-conditions may be specified to control which transitions are valid from the current state. If not overridden, this allows any transition. The pre-conditions are checked in the generated transitions and during shrinking.

The pre-conditions checking relies on proptest global rejection filtering, which comes with some disadvantages. This means that pre-conditions that are hard to satisfy might slow down the test or even fail by exceeding the maximum rejection count.

fn sequential_strategy( size: impl Into<SizeRange>, ) -> Sequential<Self::State, Self::Transition, BoxedStrategy<Self::State>, BoxedStrategy<Self::Transition>>

A sequential strategy runs the state machine transitions generated from the reference model sequentially in a test over a concrete state, which can be implemented with the help of crate::StateMachineTest trait.

You typically never need to override this method.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors