Trait Machine

pub trait Machine:
    Sized
    + 'static
    + Send
    + Sync {
    type Input: Input;
    type State: State;

    // Required methods
    fn init(&self, input: &Self::Input) -> Self::State;
    fn next(&self, state: &Self::State, input: &Self::Input) -> Self::State;
}

Finite-state machine intended to be verifiable by machine-check.

To actually be verifiable by machine-check, further processing must be done by enclosing the structures and Input, State, and Machine implementations within the machine_description macro.

Required Associated Types

type Input: Input

Machine input.

type State: State

Machine state.

Required Methods

fn init(&self, input: &Self::Input) -> Self::State

Creates an initial state from an initial input.

fn next(&self, state: &Self::State, input: &Self::Input) -> Self::State

Creates next state from current state, given the input.

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