Trait machine_check::Machine

pub trait Machine: Sized {
    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.

This function must be pure.

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

Creates next state from current state, given the input.

This function must be pure.

Object Safety

This trait is not object safe.

Implementors