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.

step() returns StepResult[Cmd]. Return the command on success, StepReject when the command is invalid for the current state (the sample is discarded), or StepFail when the system under test breaks (triggers shrinking).

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.

All mutable per-sample state belongs in ctx.sut and ctx.model, not on self. Fields on the implementing class persist between samples and shrink replays.

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

Public Functions

name

[Source]

The test name.

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]

The initial system under test.

fun box initial_sut()
: S^

Returns

  • S^

initial_model

[Source]

The initial model state.

fun box initial_model()
: M^

Returns

  • M^

step

[Source]

Generate and apply a command to ctx.sut and ctx.model.

Return the command on success, StepReject when the command is invalid for the current state, or StepFail when the system under test breaks. StepReject discards the sample and retries. StepFail records the step and triggers shrinking.

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

Parameters

Returns

invariant

[Source]

Checked after each step. Return false to fail the property.

The context is box (read-only). Use h.assert_* methods and 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. Not called when step() returns StepFail. 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