Behaviour for models in stateful property-based testing.

A model ties together all the components needed for testing: which commands can be generated, which projections track state and assertions, and the test lifecycle hooks.

Required Callbacks

• commands/0 - List of command modules (optionally weighted)
• command_sequence_projection/0 - Projection module used for command generation

Optional Callbacks

• assertion_projections/0 - Projections that verify invariants
• injectable_events/0 - Events that can arrive from Adapter.Injector modules
• setup_once/1 - Setup that runs once at the start (not during shrinking)
• setup_each/1 - Setup that runs before each execution (including shrink attempts)
• teardown_each/1 - Cleanup after each execution
• teardown_once/1 - Final cleanup after all shrinking complete
• terminate?/3 - Control when command generation should stop

Command Sequence Generation

The framework generates command sequences through this loop:

1. State Check: Get current state from command_sequence_projection/0
2. Filter Commands: Evaluate each command's when: precondition against state
3. Select Command: Choose from valid commands based on weight:
4. Generate Instance: Call the selected command's with: generator with state
5. Simulate Execution: Call simulate/2 to predict resulting events
6. Update State: Apply predicted events to the projection
7. Repeat: Go to step 2 until sequence length reached

During execution, real events replace simulated predictions, and assertion projections verify invariants.

command_sequence_projection.init()
  → filter commands by `when:` predicate
  → select command (weighted random)
  → generate command data (module generator + `with:` overrides)
  → simulator.simulate(command, state)
  → synthetic events
  → command_sequence_projection.apply(events)
  → updated state
  → repeat until max_commands or terminate?/3 returns true

Example

defmodule MyTest.OrderModel do
  @behaviour PropertyDamage.Model

  alias MyTest.Commands.{CreateOrder, ViewOrder, CancelOrder}
  alias MyTest.Projections.{ModelState, OrderBalances}

  @impl true
  def commands, do: [CreateOrder, ViewOrder, CancelOrder]

  @impl true
  def command_sequence_projection, do: ModelState

  # Optional: projections that verify invariants
  @impl true
  def assertion_projections, do: [OrderBalances]

  # Terminate when order is deleted
  @impl true
  def terminate?(_state, %DeleteOrder{}, _events), do: true
  def terminate?(_state, _command, _events), do: false
end

Command Specification

Commands are specified with options controlling weight, preconditions, and parameterization:

def commands do
  [
    # Simple: just module (weight 1, always enabled, no overrides)
    CreateOrder,

    # Weighted: {module, weight: n}
    {ViewOrder, weight: 2},

    # Full options: {module, keyword_list}
    {CancelOrder,
      weight: 1,
      when: fn state -> map_size(state.orders) > 0 end,
      with: fn state -> %{order_ref: StreamData.member_of(Map.keys(state.orders))} end}
  ]
end

Options

• :weight - Relative selection frequency (default: 1)
• :when - Precondition function (state -> boolean) (default: always true)
• :with - Override function (state -> map) for command generation (default: %{})

Weights express relative frequency among valid commands. If CreateOrder has weight 3 and CancelOrder has weight 1, and both pass their when: predicates, CreateOrder will be selected ~75% of the time.

Simulator

Models can define a Simulator module that predicts expected events for each command. See PropertyDamage.Model.Simulator for the behaviour definition.

defmodule MySimulator do
  @behaviour PropertyDamage.Model.Simulator

  @impl true
  def simulate(%CreateOrder{name: name}, _state) do
    [%OrderCreated{name: name, order_ref: nil}]
  end

  def simulate(%ViewOrder{order_ref: ref}, state) do
    if Map.has_key?(state.orders, ref) do
      [%OrderViewed{order_ref: ref}]
    else
      [%OrderNotFound{order_ref: ref}]
    end
  end
end

Then reference it in the model:

def simulator, do: MySimulator

For inline implementation, have the model implement both behaviours:

defmodule MyModel do
  @behaviour PropertyDamage.Model
  @behaviour PropertyDamage.Model.Simulator

  def simulator, do: __MODULE__

  @impl PropertyDamage.Model.Simulator
  def simulate(%CreateOrder{name: name}, _state), do: [%OrderCreated{name: name}]
  def simulate(_command, _state), do: []
end

This enables symbolic execution during sequence generation.

Lifecycle Diagram

┌─────────────────────────────────────────────────────────────┐
│                     Property Test Run                       │
│                                                             │
│  setup_once/1 ─────────────────────────────────────────┐    │
│                                                        │    │
│  ┌─ Run 1 ──────────────────────────────────────┐      │    │
│  │ setup_each/1                                 │      │    │
│  │ [execute commands against SUT]               │      │    │
│  │ teardown_each/1                              │      │    │
│  └──────────────────────────────────────────────┘      │    │
│                                                        │    │
│  ┌─ Run 2 ──────────────────────────────────────┐      │    │
│  │ setup_each/1                                 │      │    │
│  │ [execute commands against SUT]               │      │    │
│  │ teardown_each/1                              │      │    │
│  └──────────────────────────────────────────────┘      │    │
│                       ...                              │    │
│                                                        │    │
│  ┌─ If failure, shrinking ─────────────────────┐       │    │
│  │ ┌─ Shrink attempt ────────────────────┐     │       │    │
│  │ │ setup_each/1                        │     │       │    │
│  │ │ [execute shrunk sequence]           │     │       │    │
│  │ │ teardown_each/1                     │     │       │    │
│  │ └─────────────────────────────────────┘     │       │    │
│  │                   ...                       │       │    │
│  └─────────────────────────────────────────────┘       │    │
│                                                        │    │
│  teardown_once/1 ◀─────────────────────────────────────┘    │
│                                                             │
└─────────────────────────────────────────────────────────────┘

Terminal States

The terminate?/3 callback controls when command generation should stop. This is more flexible than command-level attributes because the same command may or may not be terminal depending on the test scenario.

Arguments:

• state - The current state after applying events from this command
• command - The command that just executed
• events - The events produced by that command

Examples:

• Terminate on specific command: def terminate?(_state, %Shutdown{}, _events), do: true
• Terminate on state: def terminate?(state, _, _), do: map_size(state.pending) == 0
• Terminate on event: def terminate?(_, _, events), do: Enum.any?(events, &is_complete?/1)

If not implemented, the framework runs until max_commands is reached.