Function run

pub fn run<M: FullMachine>(system: M) -> ExecResult

Executes machine-check with system environment arguments.

Is supposed to be used for simple systems that do not take arguments.

The system must implement Machine. The system structures and Input, State, and Machine implementations must be enclosed within the machine_description macro, which processes them to enable fast and efficient formal verification.