metamon/stateful

Run a sequence of Command(model, real) against an initial (model, real) pair, asserting that every command’s precondition holds against the model and that run against the real returns Ok(Nil).

This is the minimum surface needed for model-based testing. It intentionally does not generate command sequences: callers construct the list themselves (or with metamon.forall_with over a list-of-commands generator). Shrinking command sequences and scheduler-based parallelism are out of scope for this minimum; the explicit list-driven flow is enough to catch model/real drift in straightforward state machines.

Types

Outcome

</>

Outcome of running a command sequence.

pub type Outcome(model) {
  Passed(final_model: model, ran: Int, skipped: Int)
  Failed(
    index: Int,
    command_name: String,
    reason: String,
    model_at_failure: model,
  )
}

Constructors

```
Passed(final_model: model, ran: Int, skipped: Int)
```
All commands whose preconditions held passed against the real world. The final model state is reported for inspection.
```
Failed(
  index: Int,
  command_name: String,
  reason: String,
  model_at_failure: model,
)
```
The i-th command (zero-indexed) failed: either its real-side run returned Error or no command of the original list had a satisfied precondition (in which case index = -1).

Values

assert_passed

</>

pub fn assert_passed(outcome: Outcome(model)) -> Nil

Convenience: assert that the outcome is Passed. On Failed, panic with a structured message that mirrors the regular failure report style.

names_of

</>

pub fn names_of(
  commands: List(command.Command(model, real)),
) -> List(String)

Names of all commands in the sequence, in order. Useful for the stateful test’s own failure messages.

run

</>

pub fn run(
  initial_model: model,
  initial_real: real,
  commands: List(command.Command(model, real)),
) -> Outcome(model)

Run commands left-to-right starting from initial_model and initial_real. Commands whose preconditions fail are skipped (counted but not run). The first real-side Error(_) halts the sequence and is returned as Failed.