Skip to content

StatefulProperty[S: S, M: M, Cmd: Stringable val]

[Source]

A stateful property test with interleaved command generation and execution.

S is the system under test (ref or val capability). M is the reference model (ref or val). Cmd is a union of val command classes, each Stringable.

Each sample creates fresh state via initial_sut() and initial_model(), draws a step count uniformly from [1, max_steps()], then for each step calls step to generate and execute a command, followed by invariant to check model-SUT agreement. After all steps, final_check runs once. On failure, the choice sequence is replayed with shrunken candidates.

Factory methods must be deterministic: given the same starting point, they produce equivalent state. They are called once per sample and once per shrink replay. Non-deterministic factories cause the shrinker to accept or reject candidates incorrectly.

h.fail() flags the property as failed but does not abort the current step. Execution continues so that later assertions are still evaluated. The h.assert_* methods return Bool — false on failure — which can be used for local failure tracking.

All mutable per-sample state belongs in ctx.sut and ctx.model, not on self. The runner reuses the property instance across samples, so fields on the implementing class persist between samples and shrink replays.

A property with no invariant override and no in-step assertions only verifies that step does not error.

PropertyParams.async is not supported for stateful properties.

trait ref StatefulProperty[S: S, M: M, Cmd: Stringable val]

Public Functions

name

[Source]

Appears in test output.

fun box name()
: String val

Returns

params

[Source]

Parameters controlling sample count, seed, shrink budget, and timeout.

fun box params()
: PropertyParams val

Returns

max_steps

[Source]

Maximum number of steps per sample. The actual count for each sample is drawn uniformly from [1, max_steps()].

fun box max_steps()
: USize val

Returns

initial_sut

[Source]

Create a fresh system under test. Called once per sample and once per shrink replay. Must be deterministic.

fun box initial_sut()
: S^

Returns

  • S^

initial_model

[Source]

Create a fresh reference model. Called once per sample and once per shrink replay. Must be deterministic.

fun box initial_model()
: M^

Returns

  • M^

step

[Source]

Generate and execute one step. Draw a command from rnd, apply it to ctx.sut and ctx.model, and return the command object.

Errors when no valid command exists in the current state. During initial recording the runner skips the sample; during shrink replay the candidate is rejected.

Reserve error for the case where no valid command exists. For operations that should never fail, use try/else with h.fail(). For match arms that should be structurally unreachable, use _Unreachable().

Do not call rnd.start_span or rnd.end_span inside step.

fun ref step(
  ctx: StatefulContext[S, M] ref,
  rnd: Randomness ref,
  h: PropertyHelper val)
: Cmd ?

Parameters

Returns

  • Cmd ?

invariant

[Source]

Check that model and SUT agree after every step. The context is box (read-only).

The runner uses the return value for step-level failure attribution. Return the assertion result directly:

fun invariant(ctx: ..., h: PropertyHelper): Bool =>
  h.assert_eq[USize](ctx.model.size(), ctx.sut.size())

For multiple assertions, chain with and:

fun invariant(ctx: ..., h: PropertyHelper): Bool =>
  h.assert_eq[USize](ctx.model.size(), ctx.sut.size()) and
    h.assert_true(ctx.sut.size() <= ctx.sut.capacity())

Default returns true (no failure).

fun box invariant(
  ctx: StatefulContext[S, M] box,
  h: PropertyHelper val)
: Bool val

Parameters

Returns

final_check

[Source]

End-of-sequence check after all steps complete. The context is box (read-only). Default returns true (no failure).

fun box final_check(
  ctx: StatefulContext[S, M] box,
  h: PropertyHelper val)
: Bool val

Parameters

Returns