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.

A Passed outcome with ran == 0 is treated as a vacuous pass and panics:

ran == 0 && skipped == 0 — “empty commands list” (matches the panic from run([])).
ran == 0 && skipped > 0 — every command’s precondition returned False for the model the runner walked. The test never compared model and real, so silently passing would hide precondition / initial-model bugs.

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.

Passing [] is a programming error (vacuous test) and panics with a structured message — pass at least one Command, or use forall(...) for a non-stateful property.