Interface StateMachine

fendermint/testing/src/smt.rs:7–57

State machine tests inspired by [ScalaCheck](https://github.com/typelevel/scalacheck/blob/main/doc/UserGuide.md#stateful-testing) and [quickcheck-state-machine](https://hackage.haskell.org/package/quickcheck-state-machine).

/// State machine tests inspired by [ScalaCheck](https://github.com/typelevel/scalacheck/blob/main/doc/UserGuide.md#stateful-testing)
/// and [quickcheck-state-machine](https://hackage.haskell.org/package/quickcheck-state-machine).
pub trait StateMachine {
    /// System Under Test.
    type System;
    /// The idealised reference state we are testing aginst.
    type State: Clone;
    /// The random commands we can apply on the state in each step.
    type Command;
    /// The return result from command application.
    type Result;

    /// Generate a random initial state.
    fn gen_state(&self, u: &mut Unstructured) -> arbitrary::Result<Self::State>;

    /// Create a new System Under Test reflecting the given initial state.
    ///
    /// The [System] should free all of its resources when it goes out of scope.
    fn new_system(&self, state: &Self::State) -> Self::System;

    /// Generate a random command given the latest state.
    fn gen_command(
        &self,
        u: &mut Unstructured,
        state: &Self::State,
    ) -> arbitrary::Result<Self::Command>;

    /// Apply a command on the System Under Test.
    fn run_command(&self, system: &mut Self::System, cmd: &Self::Command) -> Self::Result;

    /// Use assertions to check that the result returned by the System Under Test
    /// was correct, given the model pre-state.
    fn check_result(&self, cmd: &Self::Command, pre_state: &Self::State, result: Self::Result);

    /// Apply a command on the model state.
    ///
    /// We could use `Cow` here if we wanted to preserve the history of state and
    /// also avoid cloning when there's no change.
    fn next_state(&self, cmd: &Self::Command, state: Self::State) -> Self::State;

    /// Use assertions to check that the state transition on the System Under Test
    /// was correct, by comparing to the model post-state.
    ///
    /// This can be used to check invariants which should always be true.
    ///
    /// Returns a flag indicating whether we should continue testing this system.
    fn check_system(
        &self,
        cmd: &Self::Command,
        post_state: &Self::State,
        post_system: &Self::System,
    ) -> bool;
}

/// Run a state machine test by generating `max_steps` commands.
///