🥮 mooncakes.io

quickcheck_statemachine

moon add moonbit-community/quickcheck_statemachine@0.0.1
Download zip
Version
0.0.1
License
Apache-2.0
Last updated
2 months ago
Downloads
108

Dependencies

README

#moonbit-community/quickcheck_statemachine

quickcheck_statemachine is a MoonBit library for testing stateful programs with model-based properties. A test generates a whole program of commands, executes it against a mutable system, and checks every response against a pure model.

This library is useful when:

  • valid operations depend on earlier operations;
  • a bug only appears after a sequence of commands;
  • the implementation has handles, ids, files, queues, counters, or other mutable state that is awkward to test with single examples.

#Example: Mutable References

As a first example, consider a tiny mutable-reference system. A program can create a reference, read it, write it, and increment it. The implementation below also has an optional logic bug: writing a value in 5..=10 stores value + 1 for that write.

#Commands And Responses

Generated programs cannot contain real references before execution starts. Commands use Ref[RefId]: symbolic references during generation, and concrete references when the program is executed.

///|
struct RefId {
  id : Int
} derive(Eq, Debug)

///|
enum Command {
  Create
  Read(@quickcheck_statemachine.Ref[RefId])
  Write(@quickcheck_statemachine.Ref[RefId], Int)
  Increment(@quickcheck_statemachine.Ref[RefId])
} derive(Eq, Debug)

///|
enum Response {
  Created(@quickcheck_statemachine.Ref[RefId])
  ReadValue(Int)
  Written
  Incremented
} derive(Eq, Debug)

Create returns a reference. Its response may introduce a new symbolic variable. Later commands can mention that variable. During execution it will be looked up in the environment and replaced by the concrete RefId.

#The System Under Test

The implementation stores references in a mutable array. The Bug parameter is there only to demonstrate that the property can find a bad implementation.

///|
enum Bug {
  NoBug
  LogicBug
} derive(Eq, Debug)

///|
struct SystemEntry {
  id : Int
  value : Int
} derive(Eq, Debug)

///|
struct ReferenceSystem {
  refs : Array[SystemEntry]
  mut next_id : Int
} derive(Eq, Debug)

The helper functions are ordinary system operations. They only deal with concrete ids.

///|
fn reference_id(reference : @quickcheck_statemachine.Ref[RefId]) -> Int? {
  match reference {
    Concrete(ref_id) => Some(ref_id.id)
    Symbolic(_) => None
  }
}

///|
fn system_lookup(system : ReferenceSystem, id : Int) -> Int? {
  for entry in system.refs {
    if entry.id == id {
      return Some(entry.value)
    }
  }
  None
}

///|
fn system_update(system : ReferenceSystem, id : Int, value : Int) -> Unit {
  for index = 0; index < system.refs.length(); {
    if system.refs[index].id == id {
      system.refs[index] = { id, value }
      return
    }
    continue index + 1
  }
}

semantics is the real command interpreter. In a larger test this is where you would call a database, file system, service, or mutable data structure.

///|
fn semantics(
  bug : Bug,
  command : Command,
  system : ReferenceSystem,
) -> Response {
  match command {
    Create => {
      let id = system.next_id
      system.next_id  1
      system.refs.push({ id, value: 0 })
      Created(Concrete({ id, }))
    }
    Read(reference) =>
      match reference_id(reference) {
        Some(id) =>
          match system_lookup(system, id) {
            Some(value) => ReadValue(value)
            None => ReadValue(0)
          }
        None => ReadValue(0)
      }
    Write(reference, value) =>
      match reference_id(reference) {
        Some(id) => {
          let stored = if bug == LogicBug && 5 <= value && value <= 10 {
            value + 1
          } else {
            value
          }
          system_update(system, id, stored)
          Written
        }
        None => Written
      }
    Increment(reference) =>
      match reference_id(reference) {
        Some(id) => {
          match system_lookup(system, id) {
            Some(value) => system_update(system, id, value + 1)
            None => ()
          }
          Incremented
        }
        None => Incremented
      }
  }
}

#The Model

The model is pure data. It says which references exist and what value each reference should contain.

///|
struct ModelEntry {
  reference : @quickcheck_statemachine.Ref[RefId]
  value : Int
} derive(Eq, Debug)

///|
struct Model {
  refs : Array[ModelEntry]
} derive(Eq, Debug)

///|
fn model_empty() -> Model {
  { refs: [] }
}

The model helpers are deliberately simple. They are not the implementation under test; they are the specification used to check it.

///|
fn model_lookup(
  model : Model,
  reference : @quickcheck_statemachine.Ref[RefId],
) -> Int? {
  for entry in model.refs {
    if entry.reference == reference {
      return Some(entry.value)
    }
  }
  None
}

///|
fn model_member(
  model : Model,
  reference : @quickcheck_statemachine.Ref[RefId],
) -> Bool {
  model_lookup(model, reference) is Some(_)
}

///|
fn model_update(
  model : Model,
  reference : @quickcheck_statemachine.Ref[RefId],
  value : Int,
) -> Model {
  let refs = model.refs.copy()
  for index = 0; index < refs.length(); {
    if refs[index].reference == reference {
      refs[index] = { reference, value }
      return { refs, }
    }
    continue index + 1
  }
  refs.push({ reference, value })
  { refs, }
}

#Preconditions And Transitions

The precondition is the client contract. Create is always valid. Reads, writes, and increments are valid only for references that are already present in the model.

///|
fn precondition(
  model : Model,
  command : Command,
) -> @quickcheck_statemachine.Logic {
  let ok = match command {
    Create => true
    Read(reference) | Write(reference, _) | Increment(reference) =>
      model_member(model, reference)
  }
  @quickcheck_statemachine.Logic::predicate(name="known reference", value=ok)
}

The transition function advances the pure model. It is used during symbolic program generation and concrete execution checking.

///|
fn transition(model : Model, command : Command, response : Response) -> Model {
  match (command, response) {
    (Create, Created(reference)) => model_update(model, reference, 0)
    (Read(_), ReadValue(_)) => model
    (Write(reference, value), Written) => model_update(model, reference, value)
    (Increment(reference), Incremented) =>
      match model_lookup(model, reference) {
        Some(value) => model_update(model, reference, value + 1)
        None => model
      }
    _ => model
  }
}

#Postconditions

Postconditions compare the concrete system response with the model. A Read must return the current modeled value. A Create must create a reference whose initial modeled value is zero.

///|
fn postcondition(
  model : Model,
  command : Command,
  response : Response,
) -> @quickcheck_statemachine.Logic {
  match (command, response) {
    (Create, Created(reference)) => {
      let next_model = transition(model, command, response)
      @quickcheck_statemachine.Logic::predicate(
        name="Create",
        value=model_lookup(next_model, reference) == Some(0),
      )
    }
    (Read(reference), ReadValue(value)) =>
      @quickcheck_statemachine.Logic::predicate(
        name="Read",
        value=model_lookup(model, reference) == Some(value),
      )
    (Write(_, _), Written) => @quickcheck_statemachine.Logic::top()
    (Increment(_), Incremented) => @quickcheck_statemachine.Logic::top()
    _ => @quickcheck_statemachine.Logic::bot()
  }
}

#Generation And Shrinking

The generator creates commands from the current symbolic model. If there are no references yet, it must create one first. Once references exist, it can generate any valid operation over one of them.

///|
fn choose_reference(
  model : Model,
  rng : @splitmix.RandomState,
) -> @quickcheck_statemachine.Ref[RefId] {
  let index = rng.next_positive_int() % model.refs.length()
  model.refs[index].reference
}

///|
fn generator(
  model : Model,
  size : Int,
  rng : @splitmix.RandomState,
) -> Command? {
  ignore(size)
  if model.refs.length() == 0 {
    Some(Create)
  } else {
    match rng.next_positive_int() % 4 {
      0 => Some(Create)
      1 => Some(Read(choose_reference(model, rng)))
      2 =>
        Some(Write(choose_reference(model, rng), rng.next_positive_int() % 16))
      _ => Some(Increment(choose_reference(model, rng)))
    }
  }
}

The shrinker tries smaller writes. The library also performs dependency-aware command deletion and remaps symbolic variables when possible.

///|
fn shrinker(_model : Model, command : Command) -> Array[Command] {
  match command {
    Write(reference, value) =>
      if value == 0 {
        []
      } else {
        [Write(reference, 0), Write(reference, value / 2)]
      }
    _ => []
  }
}

#Symbolic Responses

mock predicts symbolic responses during generation and shrinking. For Create it allocates a fresh symbolic variable. For Read it returns the value from the model. For Write and Increment it can return simple acknowledgements.

///|
fn mock(
  model : Model,
  command : Command,
  gen_sym : @quickcheck_statemachine.GenSym,
) -> (Response, @quickcheck_statemachine.GenSym) {
  match command {
    Create => {
      let (fresh_var, next_gen_sym) = gen_sym.fresh()
      (Created(Symbolic(fresh_var)), next_gen_sym)
    }
    Read(reference) =>
      match model_lookup(model, reference) {
        Some(value) => (ReadValue(value), gen_sym)
        None => (ReadValue(0), gen_sym)
      }
    Write(_, _) => (Written, gen_sym)
    Increment(_) => (Incremented, gen_sym)
  }
}

///|
fn response_vars(response : Response) -> Array[@quickcheck_statemachine.Var] {
  match response {
    Created(Symbolic(fresh_var)) => [fresh_var]
    _ => []
  }
}

Before execution, symbolic references must be reified into concrete references using the environment built from earlier responses.

///|
fn reify_ref(
  reference : @quickcheck_statemachine.Ref[RefId],
  environment : @quickcheck_statemachine.Environment[RefId],
) -> Result[
  @quickcheck_statemachine.Ref[RefId],
  @quickcheck_statemachine.EnvError,
] {
  match reference {
    Concrete(ref_id) => Ok(Concrete(ref_id))
    Symbolic(fresh_var) =>
      match environment.lookup(fresh_var) {
        Ok(ref_id) => Ok(Concrete(ref_id))
        Err(error) => Err(error)
      }
  }
}

///|
fn reify_command(
  command : Command,
  environment : @quickcheck_statemachine.Environment[RefId],
) -> Result[Command, @quickcheck_statemachine.EnvError] {
  match command {
    Create => Ok(Create)
    Read(reference) =>
      match reify_ref(reference, environment) {
        Ok(concrete) => Ok(Read(concrete))
        Err(error) => Err(error)
      }
    Write(reference, value) =>
      match reify_ref(reference, environment) {
        Ok(concrete) => Ok(Write(concrete, value))
        Err(error) => Err(error)
      }
    Increment(reference) =>
      match reify_ref(reference, environment) {
        Ok(concrete) => Ok(Increment(concrete))
        Err(error) => Err(error)
      }
  }
}

After execution, a symbolic Created response must be bound to the concrete reference returned by the system.

///|
fn bind_response(
  symbolic : Response,
  concrete : Response,
  environment : @quickcheck_statemachine.Environment[RefId],
) -> Result[
  @quickcheck_statemachine.Environment[RefId],
  @quickcheck_statemachine.BindError,
] {
  match (symbolic, concrete) {
    (Created(Symbolic(fresh_var)), Created(Concrete(ref_id))) =>
      Ok(environment.insert(fresh_var, ref_id))
    (Created(Symbolic(_)), _) => Err(BindMessage("expected concrete reference"))
    _ => Ok(environment)
  }
}

When shrinking removes commands, references may need to be rewritten. Returning None means a candidate command is no longer valid because it depends on a reference that disappeared.

///|
fn remap_ref(
  reference : @quickcheck_statemachine.Ref[RefId],
  scope : Map[@quickcheck_statemachine.Var, @quickcheck_statemachine.Var],
) -> @quickcheck_statemachine.Ref[RefId]? {
  match reference {
    Concrete(ref_id) => Some(Concrete(ref_id))
    Symbolic(fresh_var) =>
      match scope.get(fresh_var) {
        Some(next_var) => Some(Symbolic(next_var))
        None => None
      }
  }
}

///|
fn remap_command(
  command : Command,
  scope : Map[@quickcheck_statemachine.Var, @quickcheck_statemachine.Var],
) -> Command? {
  match command {
    Create => Some(Create)
    Read(reference) =>
      match remap_ref(reference, scope) {
        Some(next_reference) => Some(Read(next_reference))
        None => None
      }
    Write(reference, value) =>
      match remap_ref(reference, scope) {
        Some(next_reference) => Some(Write(next_reference, value))
        None => None
      }
    Increment(reference) =>
      match remap_ref(reference, scope) {
        Some(next_reference) => Some(Increment(next_reference))
        None => None
      }
  }
}

#Assembling The State Machine

All callbacks are packed into a StateMachine. The optional script parameter below is just a test convenience: it lets the examples run a fixed command program.

///|
fn command_name(command : Command) -> String {
  match command {
    Create => "create"
    Read(_) => "read"
    Write(_, _) => "write"
    Increment(_) => "increment"
  }
}

///|
fn config(
  max_commands~ : Int,
  seed? : UInt64 = 11,
  cases? : Int = 1,
  shrink? : Bool = true,
) -> @quickcheck_statemachine.RunConfig {
  {
    seed,
    cases,
    max_commands,
    size: max_commands,
    max_tries: 20,
    shrink,
    max_shrinks: 20,
    max_shrink_rounds: 10,
    required_labels: [],
    required_command_names: [],
  }
}

///|
fn sm(
  bug : Bug,
  script? : Array[Command]? = None,
) -> @quickcheck_statemachine.StateMachine[
  Model,
  Model,
  Command,
  Command,
  Response,
  Response,
  RefId,
  ReferenceSystem,
] {
  let cursor : Array[Int] = [0]
  @quickcheck_statemachine.StateMachine::new(
    init_symbolic_model=model_empty,
    init_concrete_model=model_empty,
    init_system=() => { refs: [], next_id: 0 },
    generator=(model, size, rng) => {
      match script {
        Some(commands) => {
          ignore(model)
          ignore(size)
          ignore(rng)
          let index = cursor[0]
          if index < commands.length() {
            cursor[0] = index + 1
            Some(commands[index])
          } else {
            None
          }
        }
        None => generator(model, size, rng)
      }
    },
    mock~,
    transition_symbolic=transition,
    transition_concrete=transition,
    precondition~,
    postcondition~,
    response_vars~,
    shrinker~,
    remap_command~,
    reify_command~,
    run_command=(command, system) => semantics(bug, command, system),
    bind_response~,
    command_name~,
  )
}

#Running The Property

With the faithful implementation, the command program below passes.

///|
test "sequential property passes without the bug" {
  let reference : @quickcheck_statemachine.Ref[RefId] = Symbolic(@quickcheck_statemachine.Var::{
    id: 0,
  })
  let commands : Array[Command] = [
    Create,
    Write(reference, 4),
    Increment(reference),
    Read(reference),
  ]
  let report = @quickcheck_statemachine.assert_check(
    sm(NoBug, script=Some(commands)),
    config=config(max_commands=commands.length()),
  )
  assert_eq(report.commands_run, 4)
}

With the logic bug enabled, the same machinery finds a small counterexample: create a reference, write 5, then read it. The implementation returns 6, and the model expects 5.

///|
test "random generation shrinks the logic bug" {
  let result = @quickcheck_statemachine.check(
    sm(LogicBug),
    config=config(seed=37, cases=100, max_commands=8),
  )
  guard result
    is Err(
      PostconditionFailed(
        step_index~,
        response~,
        commands~,
        shrinks~,
        logic~,
        ..
      )
    ) else {
    fail("expected a shrunk postcondition failure")
  }
  assert_eq(step_index, 2)
  assert_true(response is ReadValue(6))
  assert_eq(commands.length(), 3)
  assert_true(shrinks > 0)
  assert_true(!logic.eval())
}

The returned failure carries the minimized symbolic command program, the concrete invocation/response history, and the failed logical predicate. The formatting helpers are intentionally small so a test suite can print or save the parts that are useful for its domain.

///|
test "diagnostics expose commands history and predicate names" {
  let result = @quickcheck_statemachine.check(
    sm(LogicBug),
    config=config(seed=37, cases=100, max_commands=8),
  )
  guard result is Err(PostconditionFailed(commands~, history~, logic~, ..)) else {
    fail("expected a postcondition failure")
  }
  // symbolic commands
  inspect(
    @quickcheck_statemachine.format_commands(commands),
    content=(
      #|0: Create -> Created(Symbolic({ id: 0 }))
      #|1: Write(Symbolic({ id: 0 }), 5) -> Written
      #|2: Read(Symbolic({ id: 0 })) -> ReadValue(5)
      #|
    ),
  )
  // concrete history
  inspect(
    @quickcheck_statemachine.format_history(history),
    content=(
      #|Invocation(pid={ id: 0 }, command=Create)
      #|Response(pid={ id: 0 }, response=Created(Concrete({ id: 0 })))
      #|Invocation(pid={ id: 1 }, command=Write(Concrete({ id: 0 }), 5))
      #|Response(pid={ id: 1 }, response=Written)
      #|Invocation(pid={ id: 2 }, command=Read(Concrete({ id: 0 })))
      #|Response(pid={ id: 2 }, response=ReadValue(6))
      #|
    ),
  )
  // failed predicate
  inspect(
    @quickcheck_statemachine.format_counterexample(logic.counterexample()),
    content="Read",
  )
}

#How It Works

A state-machine test has these pieces:

  • Command: operations that can be generated.
  • Response: observable results returned by the system.
  • Model: a pure description of what should be true after each command.
  • precondition: when a generated command is valid.
  • transition: how the model changes after a command and response.
  • postcondition: what must hold after running a command.
  • generator and shrinker: how command programs are generated and minimized.
  • mock: symbolic responses used during generation and shrinking.
  • reify_command and bind_response: how symbolic references become concrete values during execution.
  • run_command: the real implementation under test.

The sequential property first builds a complete symbolic command program:

  1. Start with the initial symbolic model and a fresh symbolic-variable supply.
  2. Ask the generator for a command and keep retrying until the precondition accepts it, or the retry budget is exhausted.
  3. Ask mock for the symbolic response and record any variables introduced by that response.
  4. Advance the symbolic model with the symbolic transition.
  5. Repeat until max_commands is reached or the generator stops.

The generated program is then replayed against the concrete system:

  1. Start with the initial concrete model, initial system, empty environment, and empty history.
  2. Reify symbolic references into concrete references using the environment.
  3. Execute the command against the system and record invocation/response history.
  4. Check the postcondition against the pre-state model and observed response.
  5. Bind any new concrete references returned by the response.
  6. Advance the concrete model, check the invariant, and collect labels.
  7. After the program finishes, run cleanup and coverage checks.

When check finds a semantic failure and shrink is enabled, it shrinks the generated command program and reports a smaller counterexample. Direct run_commands and replay calls execute the supplied program as-is.

#More Examples

The repository contains smaller focused examples:

  • counter shows the smallest counter-style state machine.
  • queue checks a mutable circular queue against a pure FIFO model.
  • filesystem shows symbolic handles and label coverage diagnostics.
  • jug uses a state machine as a search problem for the water-jug puzzle.

Replay is exposed through replay, assert_replay, and run_saved_commands; the examples in this README use scripted generation with assert_check.

This MoonBit package currently exposes generate_parallel_commands, ParallelCommands, and run_parallel_commands. The current runner deterministically linearises commands as prefix, then left, then right. The root package is not a concurrent linearizability checker.

Async parallel checking is available from the native-only moonbit-community/quickcheck_statemachine/async_parallel package. It provides AsyncStateMachine, AsyncStateMachine::from_sync, run_parallel_commands_async, check_parallel_async, and assert_check_parallel_async.

AsyncStateMachine mirrors StateMachine: pure model, generation, reification, binding, shrinking, naming, and labelling callbacks keep the same shape. init_system, run_command, and cleanup are async. from_sync supports reuse of an existing synchronous spec. Commands without an async suspension point still behave atomically under MoonBit's cooperative async runtime.

run_parallel_commands_async executes the prefix sequentially, runs left and right as async tasks, records the concrete invocation/response history, and searches for a sequential linearization that respects real-time order. Async-only failures use AsyncRunFailure: a linearizability bug is reported as LinearizationFailed, branch environment conflicts are reported as BranchEnvironmentMergeFailed, and replay/config/generation failures wrap the existing synchronous RunFailure inside ReplayFailed.

Async failures keep the original ParallelCommands as the canonical counterexample. The flattened Commands value exists for reports, coverage, and compatibility with existing formatting helpers. The first async implementation does not shrink parallel failures. shrinks and shrink_rounds are 0. Manual parallel chunks with more than six branch operations fail before system initialization with LinearizationBudgetExceeded. This bounds the DFS linearization search.

#
BindError

source
pub(all) enum BindError {
  BindMessage(String)
  BindVarCountMismatch(Int, Int)
} derive(Eq, 
Debug)

Errors raised while binding a real response back into the execution environment.

#
Command

source
pub(all) struct Command[CSym, RSym] {
  command : CSym
  response : RSym
  vars : Array[Var]
} derive(Eq, 
Debug)

One generated symbolic command, its symbolic response, and fresh variables.

command is the action the generator chose. response is the mocked symbolic response used to advance the symbolic model before the real system has run. vars records which variables were introduced by that response so shrink validation can remap dependencies later.

#
Commands

source
pub(all) struct Commands[CSym, RSym] {
  commands : Array[Command[CSym, RSym]]
} derive(Eq, 
Debug)

A symbolic command program.

This is the stable artifact that can be shrunk, formatted, saved, loaded, and replayed. It intentionally stores symbolic responses, not concrete responses, because those are what make the program self-contained before execution.

#
Commands::append

source
fn[CSym, RSym] Commands::append(self : Commands[CSym, RSym], command : Command[CSym, RSym]) -> Commands[CSym, RSym]

Appends one command while preserving the original program.

#
Commands::concat

source
fn[CSym, RSym] Commands::concat(left : Commands[CSym, RSym], right : Commands[CSym, RSym]) -> Commands[CSym, RSym]

Concatenates two command programs.

#
Commands::empty

source
fn[CSym, RSym] Commands::empty() -> Commands[CSym, RSym]

Constructs an empty command program.

#
Commands::length

source
fn[CSym, RSym] Commands::length(self : Commands[CSym, RSym]) -> Int

Returns the number of generated commands.

#
Counterexample

source
pub(all) struct Counterexample {
  messages : Array[String]
} derive(Eq, 
Debug)

Human-readable explanation collected from a failed logical condition.

Preconditions, postconditions, and invariants use Logic instead of plain Bool so that a failing command can report which model predicate failed, much like QSM's annotated counterexamples.

#
EnvError

source
pub(all) enum EnvError {
  MissingVar(Var)
  DuplicateVar(Var)
} derive(Eq, 
Debug)

Errors raised while reifying symbolic commands into concrete commands.

#
Environment

source
pub(all) struct Environment[V] {
  bindings : Map[Var, V]
} derive(
Debug)

Runtime map from symbolic variables to concrete values.

During generation, commands only carry Vars. During replay, each concrete response can extend this environment; later commands call reify_command to look up the concrete values corresponding to those variables.

#
Environment::contains

source
fn[V] Environment::contains(self : Environment[V], variable : Var) -> Bool

Checks whether a symbolic variable is already bound.

#
Environment::empty

source
fn[V] Environment::empty() -> Environment[V]

Creates an empty execution environment.

#
Environment::get

source
fn[V] Environment::get(self : Environment[V], variable : Var) -> V?

Looks up a concrete value without constructing an EnvError.

#
Environment::insert

source
fn[V] Environment::insert(self : Environment[V], variable : Var, value : V) -> Environment[V]

Returns a copy of the environment with one additional binding.

This helper is intentionally permissive and overwrites an existing binding. Use merge when duplicate detection is part of the operation contract.

#
Environment::length

source
fn[V] Environment::length(self : Environment[V]) -> Int

Returns the number of symbolic variables with concrete bindings.

#
Environment::lookup

source
fn[V] Environment::lookup(self : Environment[V], variable : Var) -> Result[V, EnvError]

Looks up a concrete value or reports a state-machine reification error.

#
Environment::merge

source
fn[V] Environment::merge(self : Environment[V], other : Environment[V]) -> Result[Environment[V], EnvError]

Combines two environments when their symbolic-variable domains are disjoint.

This is useful for future parallel checking, where independent command branches may produce bindings that must be joined before a later command can be reified.

#
Event

source
pub(all) struct Event[Model, Command, Response] {
  before_model : Model
  command : Command
  response : Response
  after_model : Model
} derive(Eq, 
Debug)

Model transition event passed to coverage labelers.

The standalone Labeler helper receives both the model before the command and the model after the transition. The StateMachine.label callback used by replay is lighter weight: it receives the concrete model before the command, the concrete command, and the concrete response.

#
GenSym

source
pub(all) struct GenSym {
  next : Int
} derive(Eq, 
Debug)

Deterministic source of fresh symbolic variables for mock responses.

GenSym is threaded through generation and shrink validation so that a regenerated prefix allocates the same sequence of symbolic variables. That determinism is what makes command dependencies shrink safely.

#
GenSym::fresh

source
fn GenSym::fresh(self : GenSym) -> (Var, GenSym)

Allocates one variable and returns the advanced supply.

#
GenSym::new

source
fn GenSym::new() -> GenSym

Creates a fresh symbolic-variable supply starting at v0.

#
GenerationFailure

source
pub(all) enum GenerationFailure[MSym, CSym, RSym] {
  InvalidGenerationConfig(String)
  Deadlock(Int, MSym, Commands[CSym, RSym], Logic?)
} derive(Eq, 
Debug)

Failures that can occur while generating a symbolic command program.

#
History

source
pub(all) struct History[C, R] {
  events : Array[HistoryEvent[C, R]]
} derive(Eq, 
Debug)

Ordered trace of command invocations, responses, and exceptions.

The history is kept in the same representation used by state-machine testing literature: it records observable calls rather than only final results, which is the information needed for counterexamples and future linearizability checks.

#
History::empty

source
fn[C, R] History::empty() -> History[C, R]

Creates an empty execution trace.

#
History::push

source
fn[C, R] History::push(self : History[C, R], event : HistoryEvent[C, R]) -> History[C, R]

Returns a copy of the trace with one more event appended.

#
HistoryEvent

source
pub(all) enum HistoryEvent[C, R] {
  Invocation(Pid, C)
  Response(Pid, R)
  Exception(Pid, String)
} derive(Eq, 
Debug)

One event in an execution trace.

A complete operation normally appears as an Invocation followed later by a Response. If the system under test raises, the matching terminal event is an Exception instead.

#
Labeler

source
pub(all) struct Labeler[Model, Command, Response] {
  classify : (Event[Model, Command, Response]) -> Array[String]
}

Callback wrapper for classifying a state-machine event.

#
Logic

source
pub(all) enum Logic {
  Top
  Bot
  Boolean(Bool)
  Predicate(String, Bool)
  And(Logic, Logic)
  Or(Logic, Logic)
  Implies(Logic, Logic)
  Not(Logic)
  Annotate(String, Logic)
} derive(Eq, 
Debug)

Boolean logic tree used by model predicates.

Logic is deliberately small: it can be evaluated as a Boolean, but it also retains predicate names and annotations for counterexample formatting. Use it for preconditions, postconditions, invariants, and any helper predicate whose failure should remain visible after shrinking.

#
Logic::annotate

source
fn Logic::annotate(self : Logic, message : String) -> Logic

Adds a diagnostic frame around an existing condition.

#
Logic::boolean

source
fn Logic::boolean(value : Bool) -> Logic

Lifts a plain Boolean into Logic.

#
Logic::bot

source
fn Logic::bot() -> Logic

Constructor for an always-false condition.

#
Logic::check

source
fn Logic::check(self : Logic) -> LogicValue

Evaluates the condition and preserves diagnostics on failure.

#
Logic::counterexample

source
fn Logic::counterexample(self : Logic) -> Counterexample

Converts a failed condition into a structured counterexample.

#
Logic::eval

source
fn Logic::eval(self : Logic) -> Bool

Evaluates the condition as a Boolean, discarding diagnostic information.

#
Logic::predicate

source
fn Logic::predicate(name~ : String, value~ : Bool) -> Logic

Builds a named predicate whose name appears in counterexamples when false.

#
Logic::top

source
fn Logic::top() -> Logic

Constructor for an always-true condition.

#
LogicValue

source
pub(all) enum LogicValue {
  Holds
  Fails(Counterexample)
} derive(Eq, 
Debug)

Result of evaluating a logical condition with diagnostics preserved.

#
NParallelCommands

source
pub(all) struct NParallelCommands[CSym, RSym] {
  prefix : Commands[CSym, RSym]
  suffixes : Array[Commands[CSym, RSym]]
} derive(Eq, 
Debug)

Generalized representation for more than two parallel suffixes.

This mirrors the structure described by QSM: a sequential prefix followed by one or more groups of commands whose operations may overlap.

#
Operation

source
pub(all) struct Operation[C, R] {
  pid : Pid
  command : C
  response : R?
  exception : String?
} derive(Eq, 
Debug)

Invocation paired with its eventual response or exception.

This derived view is easier to inspect and format than the raw event stream.

#
ParallelCommands

source
pub(all) struct ParallelCommands[CSym, RSym] {
  prefix : Commands[CSym, RSym]
  left : Commands[CSym, RSym]
  right : Commands[CSym, RSym]
} derive(Eq, 
Debug)

A two-branch parallel command program.

The prefix is executed first to set up shared state. left and right represent commands that should be considered concurrent. The current runner linearizes them deterministically; the shape is kept explicit so a future implementation can replace that with real concurrent execution and linearizability search.

#
Pid

source
pub(all) struct Pid {
  id : Int
} derive(Eq, Hash, 
Debug)

Logical process id used to pair an invocation with its response.

Sequential runs use the step index as the pid. Parallel checking can assign different ids to operations that overlap in time and then search for a valid linearization of those operations.

#
Ref

source
pub(all) enum Ref[V] {
  Symbolic(Var)
  Concrete(V)
} derive(Eq, 
Debug)

A reference that is either symbolic during generation/shrinking or concrete during execution.

This mirrors the quickcheck-state-machine split between symbolic references used in generated programs and concrete references returned by the implementation under test. User command types usually contain Ref[V] whenever a command needs to point at a resource created by an earlier command.

#
RunConfig

source
pub(all) struct RunConfig {
  seed : UInt64
  cases : Int
  max_commands : Int
  size : Int
  max_tries : Int
  shrink : Bool
  max_shrinks : Int
  max_shrink_rounds : Int
  required_labels : Array[String]
  required_command_names : Array[String]
} derive(Eq, 
Debug)

Configuration shared by generation, execution, coverage checks, and shrinking.

#
RunConfig::default

source
fn RunConfig::default() -> RunConfig

Conservative defaults suitable for examples and small model tests.

#
RunFailure

source
pub(all) enum RunFailure[MSym, MCon, CSym, CCon, RSym, RCon] {
  InvalidConfig(String)
  GenerationFailed(GenerationFailure[MSym, CSym, RSym], Int, Int)
  InitFailed(Commands[CSym, RSym], String, Int, Int)
  ReifyFailed(Int, CSym, EnvError, Commands[CSym, RSym], History[CCon, RCon], Int, Int)
  ExecutionFailed(Int, CCon, CSym, MCon, Commands[CSym, RSym], History[CCon, RCon], String, Int, Int)
  BindFailed(Int, RSym, RCon, BindError, Commands[CSym, RSym], History[CCon, RCon], Int, Int)
  PostconditionFailed(Int, CCon, CSym, RCon, MCon, MCon, Logic, Commands[CSym, RSym], History[CCon, RCon], Int, Int)
  InvariantBroken(Int, MCon, Logic, Commands[CSym, RSym], History[CCon, RCon], Int, Int)
  CleanupFailed(Commands[CSym, RSym], History[CCon, RCon], String, Int, Int)
  CoverageFailed(Commands[CSym, RSym], History[CCon, RCon], Array[String], Array[String], Int, Int)
} derive(Eq, 
Debug)

Failures that can occur while generating, replaying, checking, or shrinking.

Each failure stores the symbolic program and concrete history whenever they are available, so a user can inspect the minimized counterexample in the same style as QSM's sequential property output.

#
RunReport

source
pub(all) struct RunReport[CSym, RSym, CCon, RCon] {
  seed : UInt64
  cases_run : Int
  commands_run : Int
  commands : Commands[CSym, RSym]
  history : History[CCon, RCon]
  labels : Array[String]
  command_distribution : Array[(String, Int)]
  shrinks : Int
  shrink_rounds : Int
} derive(Eq, 
Debug)

Summary of a successful generation or replay.

Reports keep both the symbolic command program and the concrete history. The symbolic program is what should be saved or shrunk; the history is what the system actually did while replaying that program.

#
ShrinkStats

source
pub(all) struct ShrinkStats {
  shrinks : Int
  rounds : Int
} derive(Eq, 
Debug)

Number of successful shrink steps and rounds used to minimize a failure.

#
StateMachine

source
pub struct StateMachine[MSym, MCon, CSym, CCon, RSym, RCon, V, S] {
  init_symbolic_model : () -> MSym
  init_concrete_model : () -> MCon
  init_system : () -> S raise
  generator : (MSym, Int, 
RandomState) -> CSym?
  mock : (MSym, CSym, GenSym) -> (RSym, GenSym)
  response_vars : (RSym) -> Array[Var]
  transition_symbolic : (MSym, CSym, RSym) -> MSym
  transition_concrete : (MCon, CCon, RCon) -> MCon
  precondition : (MSym, CSym) -> Logic
  postcondition : (MCon, CCon, RCon) -> Logic
  invariant : (MCon) -> Logic
  shrinker : (MSym, CSym) -> Array[CSym]
  remap_command : (CSym, Map[Var, Var]) -> CSym?
  reify_command : (CSym, Environment[V]) -> Result[CCon, EnvError]
  run_command : (CCon, S) -> RCon raise
  bind_response : (RSym, RCon, Environment[V]) -> Result[Environment[V], BindError]
  cleanup : (MCon, S) -> Unit raise
  command_name : (CSym) -> String
  label : (MCon, CCon, RCon) -> Array[String]
}

Complete state-machine specification.

This record is the MoonBit counterpart of QSM's StateMachine: users supply the pure model operations, symbolic/reference plumbing, and real semantics; the library supplies generation, replay, shrinking, and reporting.

The type separates symbolic and concrete model/command/response types: symbolic callbacks run before the system exists, while concrete callbacks run against the implementation under test.

#
StateMachine::new

source
fn[MSym, MCon, CSym, CCon, RSym, RCon, V, S] StateMachine::new(init_symbolic_model~ : () -> MSym, init_concrete_model~ : () -> MCon, init_system~ : () -> S raise, generator~ : (MSym, Int, 
RandomState) -> CSym?, mock~ : (MSym, CSym, GenSym) -> (RSym, GenSym), transition_symbolic~ : (MSym, CSym, RSym) -> MSym, transition_concrete~ : (MCon, CCon, RCon) -> MCon, reify_command~ : (CSym, Environment[V]) -> Result[CCon, EnvError], run_command~ : (CCon, S) -> RCon raise, bind_response~ : (RSym, RCon, Environment[V]) -> Result[Environment[V], BindError], postcondition? : (MCon, CCon, RCon) -> Logic, precondition? : (MSym, CSym) -> Logic, invariant? : (MCon) -> Logic, response_vars? : (RSym) -> Array[Var], shrinker? : (MSym, CSym) -> Array[CSym], remap_command? : (CSym, Map[Var, Var]) -> CSym?, cleanup? : (MCon, S) -> Unit raise, command_name? : (CSym) -> String, label? : (MCon, CCon, RCon) -> Array[String]) -> StateMachine[MSym, MCon, CSym, CCon, RSym, RCon, V, S]

Builds a StateMachine with conservative defaults for optional callbacks.

Required callbacks describe the core state-machine loop: initialize models and system, generate symbolic commands, mock responses, transition models, reify commands, run the system, and bind newly produced concrete values. Optional callbacks default to permissive behavior so small examples can start with only the essential pieces.

#
Var

source
pub(all) struct Var {
  id : Int
} derive(Eq, Hash, 
Debug)

A symbolic variable that names a value produced by an earlier command.

Generated command programs are built before the real system is executed, so they cannot contain concrete handles, ids, references, file descriptors, or other runtime values. Var is the stable placeholder that lets later symbolic commands refer to a value that will only be known after replay.

#
Var::to_string

source
fn Var::to_string(self : Var) -> String

Formats a symbolic variable using the short form that appears in generated command traces.

#
assert_check

source
fn[MSym : 
Debug, MCon : 
Debug, CSym : 
Debug, CCon : 
Debug, RSym : 
Debug, RCon : 
Debug, V, S] assert_check(spec : StateMachine[MSym, MCon, CSym, CCon, RSym, RCon, V, S], config? : RunConfig) -> RunReport[CSym, RSym, CCon, RCon] raise

Runs check and raises on failure.

This is convenient inside MoonBit tests where a failing property should fail the test immediately.

#
assert_replay

source
fn[MSym : 
Debug, MCon : 
Debug, CSym : 
Debug, CCon : 
Debug, RSym : 
Debug, RCon : 
Debug, V, S] assert_replay(spec : StateMachine[MSym, MCon, CSym, CCon, RSym, RCon, V, S], commands : Commands[CSym, RSym], config? : RunConfig) -> RunReport[CSym, RSym, CCon, RCon] raise

Runs replay and raises on failure.

Use this for checked-in regression programs or minimized counterexamples.

#
check

source
fn[MSym, MCon, CSym, CCon, RSym, RCon, V, S] check(spec : StateMachine[MSym, MCon, CSym, CCon, RSym, RCon, V, S], config? : RunConfig) -> Result[RunReport[CSym, RSym, CCon, RCon], RunFailure[MSym, MCon, CSym, CCon, RSym, RCon]]

Generates and executes many state-machine programs.

Each case uses a deterministic seed derived from config.seed. On the first semantic failure, check optionally shrinks the generated program and then returns the minimized failure. Coverage failures are not shrunk because they mean a successful run did not include required scenarios, not that a smaller counterexample should be found.

#
classify

source
fn[Model, Command, Response] classify(labeler : Labeler[Model, Command, Response], event : Event[Model, Command, Response]) -> Array[String]

Applies a labeler to one event.

#
collect_labels

source
fn collect_labels(labels : Array[String]) -> Array[String]

Deduplicates labels while preserving first-seen order.

The report only needs to show whether a scenario occurred at least once, but preserving order keeps the output stable for tests and saved diagnostics.

#
command_names

source
fn[CSym, RSym] command_names(commands : Commands[CSym, RSym], name : (CSym) -> String) -> Array[(String, Int)]

Counts how often each command name appears in a generated program.

command_name coverage is a coarse audit that generation is exploring every operation family expected by the test.

#
command_names_in_order

source
fn[CSym, RSym] command_names_in_order(commands : Commands[CSym, RSym], name : (CSym) -> String) -> Array[String]

Lists command names in first-seen order without counts.

#
cover_command_names

source
fn cover_command_names(seen : Array[(String, Int)], required : Array[String]) -> Array[String]

Returns the required command names that did not appear in a run.

#
first_failing_candidate

source
fn[MSym, MCon, CSym, CCon, RSym, RCon, V, S] first_failing_candidate(spec : StateMachine[MSym, MCon, CSym, CCon, RSym, RCon, V, S], candidates : Array[Commands[CSym, RSym]], config : RunConfig) -> Commands[CSym, RSym]?

Returns the first candidate that still reproduces the failure.

This keeps the shrinking loop simple and deterministic: each round accepts one smaller failing program, then restarts from that program.

#
format_commands

source
fn[CSym : 
Debug, RSym : 
Debug] format_commands(commands : Commands[CSym, RSym]) -> String

Formats a symbolic command program for display in a counterexample.

This deliberately prints the symbolic command and its mocked symbolic response, because that is the stable program users can save and replay.

#
format_counterexample

source
fn format_counterexample(counterexample : Counterexample) -> String

Formats predicate diagnostics, one message per line.

#
format_failure

source

Default failure formatter.

The failure type already stores the generated program, concrete history, model state, and shrink statistics. This helper keeps formatting simple and lets callers replace it with domain-specific pretty printing later.

#
format_history

source
fn[C : 
Debug, R : 
Debug] format_history(history : History[C, R]) -> String

Formats the concrete execution history collected while replaying commands.

#
generate_commands

source
fn[MSym, MCon, CSym, CCon, RSym, RCon, V, S] generate_commands(spec : StateMachine[MSym, MCon, CSym, CCon, RSym, RCon, V, S], config? : RunConfig) -> Result[Commands[CSym, RSym], GenerationFailure[MSym, CSym, RSym]]

Generates one symbolic command program using config.seed.

#
generate_commands_with_seed

source
fn[MSym, MCon, CSym, CCon, RSym, RCon, V, S] generate_commands_with_seed(spec : StateMachine[MSym, MCon, CSym, CCon, RSym, RCon, V, S], config? : RunConfig, seed? : UInt64) -> Result[Commands[CSym, RSym], GenerationFailure[MSym, CSym, RSym]]

Generates one symbolic command program using an explicit seed.

Generation follows the QSM symbolic loop: select a precondition-valid command, ask mock for the symbolic response, record response variables, advance the symbolic model, and repeat until max_commands or generator termination.

#
generate_parallel_commands

source
fn[MSym, MCon, CSym, CCon, RSym, RCon, V, S] generate_parallel_commands(spec : StateMachine[MSym, MCon, CSym, CCon, RSym, RCon, V, S], config? : RunConfig) -> Result[ParallelCommands[CSym, RSym], GenerationFailure[MSym, CSym, RSym]]

Generates a sequential program and splits it into prefix, left, and right.

QSM's parallel property generates commands from one symbolic model and then runs a prefix before exploring concurrent suffixes. This helper preserves the same command-program shape even though execution is currently reduced to a deterministic linearization.

#
linearise

source
fn[CSym, RSym] linearise(commands : ParallelCommands[CSym, RSym]) -> Commands[CSym, RSym]?

Produces the sequential order currently used to replay a parallel program.

A complete linearizability checker would search all histories that respect invocation/response ordering. Until that exists, this function makes the chosen order explicit and testable.

#
load_commands

source
fn[CSym, RSym] load_commands(input : String, decode : (String) -> Result[Commands[CSym, RSym], String]) -> Result[Commands[CSym, RSym], String]

Decodes a command program with a caller-provided parser.

#
logic_and

source
fn logic_and(left : Logic, right : Logic) -> Logic

Infix-friendly constructor for conjunction.

#
logic_implies

source
fn logic_implies(left : Logic, right : Logic) -> Logic

Infix-friendly constructor for implication.

#
logic_not

source
fn logic_not(logic : Logic) -> Logic

Infix-friendly constructor for negation.

#
logic_or

source
fn logic_or(left : Logic, right : Logic) -> Logic

Infix-friendly constructor for disjunction.

#
make_operations

source
fn[C, R] make_operations(history : History[C, R]) -> Array[Operation[C, R]]

Groups a raw history into operations by matching events with the same pid.

Responses are matched with the most recent unfinished invocation for the pid. This supports traces where operations from several pids are interleaved.

#
replay

source
fn[MSym, MCon, CSym, CCon, RSym, RCon, V, S] replay(spec : StateMachine[MSym, MCon, CSym, CCon, RSym, RCon, V, S], commands : Commands[CSym, RSym], config? : RunConfig) -> Result[RunReport[CSym, RSym, CCon, RCon], RunFailure[MSym, MCon, CSym, CCon, RSym, RCon]]

Alias for replaying a previously generated symbolic command program.

#
run_commands

source
fn[MSym, MCon, CSym, CCon, RSym, RCon, V, S] run_commands(spec : StateMachine[MSym, MCon, CSym, CCon, RSym, RCon, V, S], commands : Commands[CSym, RSym], config? : RunConfig) -> Result[RunReport[CSym, RSym, CCon, RCon], RunFailure[MSym, MCon, CSym, CCon, RSym, RCon]]

Replays a symbolic command program against the concrete system.

This is the sequential property loop from QSM:

  1. initialize the system, concrete model, environment, and history;
  2. reify each symbolic command through the environment;
  3. execute the concrete command and record invocation/response history;
  4. check the postcondition against the pre-state model;
  5. bind newly returned concrete references into the environment;
  6. advance/check the concrete model and collect coverage labels.

The generated program already satisfied symbolic preconditions; replay does not re-check them because its job is to compare the implementation with the concrete model.

#
run_parallel_commands

source
fn[MSym, MCon, CSym, CCon, RSym, RCon, V, S] run_parallel_commands(spec : StateMachine[MSym, MCon, CSym, CCon, RSym, RCon, V, S], commands : ParallelCommands[CSym, RSym], config? : RunConfig) -> Result[RunReport[CSym, RSym, CCon, RCon], RunFailure[MSym, MCon, CSym, CCon, RSym, RCon]]

Runs a parallel-shaped program through the current linearization path.

This gives users a stable API for parallel properties while the internal implementation remains conservative. Any future concurrent runner can keep this entry point and strengthen the semantics behind it.

#
run_saved_commands

source
fn[MSym, MCon, CSym, CCon, RSym, RCon, V, S] run_saved_commands(spec : StateMachine[MSym, MCon, CSym, CCon, RSym, RCon, V, S], input : String, decode : (String) -> Result[Commands[CSym, RSym], String], config? : RunConfig) -> Result[RunReport[CSym, RSym, CCon, RCon], RunFailure[MSym, MCon, CSym, CCon, RSym, RCon]]

Decodes and replays a saved symbolic command program.

This is the MoonBit equivalent of rerunning a minimized QSM counterexample: generation is skipped, but reification, execution, postconditions, binding, invariants, labels, and cleanup still run normally.

#
save_commands

source
fn[CSym, RSym] save_commands(commands : Commands[CSym, RSym], encode : (Commands[CSym, RSym]) -> String) -> String

Encodes a command program with a caller-provided serializer.

The library does not prescribe a wire format because user command and response types are application-specific.

#
shrink_and_validate

source
fn[MSym, MCon, CSym, CCon, RSym, RCon, V, S] shrink_and_validate(spec : StateMachine[MSym, MCon, CSym, CCon, RSym, RCon, V, S], commands : Commands[CSym, RSym]) -> Commands[CSym, RSym]?

Rebuilds a candidate program and rejects it if symbolic dependencies break.

This is the dependency-aware part of shrinking. Removing or replacing a command can invalidate later references. Instead of trusting the edited program, we replay generation over the symbolic model:

  • remap each command through the current old-to-new variable scope;
  • re-check the precondition against the rebuilt symbolic model;
  • regenerate the mock response and fresh variables deterministically;
  • advance the symbolic model with transition_symbolic.

If any step fails, the candidate is discarded. If all steps succeed, the returned program has a consistent symbolic environment and can be executed.

#
shrink_commands_once

source
fn[MSym, MCon, CSym, CCon, RSym, RCon, V, S] shrink_commands_once(spec : StateMachine[MSym, MCon, CSym, CCon, RSym, RCon, V, S], commands : Commands[CSym, RSym]) -> Array[Commands[CSym, RSym]]

Produces one round of smaller, dependency-valid command programs.

The candidates are generated in two phases: first try deleting each command, then try command-specific replacements supplied by shrinker. Every edited program is sent through shrink_and_validate before it is returned, so later replay does not waste time on candidates with dangling symbolic variables.

Source Files

Powered by MoonBit

Site sourceReport issuePackagesBuild queueSkillsStatistics

© 2026 mooncakes.io