Trait ModelState

pub trait ModelState:
    Clone
    + Debug
    + Default {
    type Operation: Clone + Debug;
    type RunContext;
    type OperationStrategy: Strategy<Value = Self::Operation>;

    // Required methods
    fn op_generators(&self) -> Vec<Self::OperationStrategy>;
    fn preconditions_met(&self, op: &Self::Operation) -> bool;
    fn next_state(&mut self, op: &Self::Operation);
    fn init_test_run<'life0, 'async_trait>(
        &'life0 self,
    ) -> Pin<Box<dyn Future<Output = Self::RunContext> + 'async_trait>>
       where Self: 'async_trait,
             'life0: 'async_trait;
    fn run_op<'life0, 'life1, 'life2, 'async_trait>(
        &'life0 self,
        op: &'life1 Self::Operation,
        ctxt: &'life2 mut Self::RunContext,
    ) -> Pin<Box<dyn Future<Output = ()> + 'async_trait>>
       where Self: 'async_trait,
             'life0: 'async_trait,
             'life1: 'async_trait,
             'life2: 'async_trait;
    fn check_postconditions<'life0, 'life1, 'async_trait>(
        &'life0 self,
        ctxt: &'life1 mut Self::RunContext,
    ) -> Pin<Box<dyn Future<Output = ()> + 'async_trait>>
       where Self: 'async_trait,
             'life0: 'async_trait,
             'life1: 'async_trait;
    fn clean_up_test_run<'life0, 'life1, 'async_trait>(
        &'life0 self,
        ctxt: &'life1 mut Self::RunContext,
    ) -> Pin<Box<dyn Future<Output = ()> + 'async_trait>>
       where Self: 'async_trait,
             'life0: 'async_trait,
             'life1: 'async_trait;
}

A trait for defining stateful property tests.

The ModelState trait includes callbacks that enable generating, shrinking, and running test cases. Note that the same value is intended to be used both for planning test cases and executing them; the ModelState::next_state callback is used during all three of test case generation, execution, and shrinking, since all three of those processes require modeling the state of the system under test in order to determine whether a given sequence of operations is valid (in generation and shrinking) and to check postconditions (during test execution).

Note that the trait as it is currently implemented uses async callbacks. We may want to make a non-async version of this at some point, but all the tests we’ve written so far are async, so I’m leaving this as a TODO item.

Required Associated Types

type Operation: Clone + Debug

A type used to specify a single operation in the sequence of operations that constitute a test case.

type RunContext

A type used to hold on to any state that is only needed at runtime for executing cases (as opposed to the state held directly in an implementor of ModelState, which is used for generation and shrinking).

type OperationStrategy: Strategy<Value = Self::Operation>

The type for proptest strategies used to generate Self::Operation values.

Note that this type should no longer need to be explicitly named in this way once return_position_impl_trait_in_trait is stable.

Required Methods

fn op_generators(&self) -> Vec<Self::OperationStrategy>

Returns a Vec of Strategys for generating Self::Operation values.

The proptest-stateful code will pseudo-randomly pick a strategy based off of the random seed from the proptest TestRunner, and generate a single Self::Operation value from the selected Strategy.

fn preconditions_met(&self, op: &Self::Operation) -> bool

Determines whether preconditions have been met for an operation, based on the current model state.

fn next_state(&mut self, op: &Self::Operation)

Updates the internal model state based on the modeled result of executing of op.

fn init_test_run<'life0, 'async_trait>( &'life0 self, ) -> Pin<Box<dyn Future<Output = Self::RunContext> + 'async_trait>>

where Self: 'async_trait, 'life0: 'async_trait,

Called once at the beginning of each test case’s execution.

After performing any necessary initialization work, the implementation returns a value of type Self::RunContext which is subsequently passed back into calls to run_op, check_postconditions, and clean_up_test_run.

fn run_op<'life0, 'life1, 'life2, 'async_trait>( &'life0 self, op: &'life1 Self::Operation, ctxt: &'life2 mut Self::RunContext, ) -> Pin<Box<dyn Future<Output = ()> + 'async_trait>>

where Self: 'async_trait, 'life0: 'async_trait, 'life1: 'async_trait, 'life2: 'async_trait,

Called to execute op during a test run.

fn check_postconditions<'life0, 'life1, 'async_trait>( &'life0 self, ctxt: &'life1 mut Self::RunContext, ) -> Pin<Box<dyn Future<Output = ()> + 'async_trait>>

where Self: 'async_trait, 'life0: 'async_trait, 'life1: 'async_trait,

Called after each execution of run_op to check any postconditions that are expected to be upheld during the test run.

Since the return type is (), postcondition failures must trigger a panic.

fn clean_up_test_run<'life0, 'life1, 'async_trait>( &'life0 self, ctxt: &'life1 mut Self::RunContext, ) -> Pin<Box<dyn Future<Output = ()> + 'async_trait>>

where Self: 'async_trait, 'life0: 'async_trait, 'life1: 'async_trait,

Called at the end of each test run to allow any necessary cleanup work to be done.

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