Behaviour and DSL for defining specifications through labelled transition systems (LTSs).

A specification module describes the expected states, actions, and transitions of a system. Spex uses this information to:

• validate observed runtime behaviour,
• construct and maintain implementation models,
• check branching bisimilarity between model and specification,
• enforce transition timeout and pruning policies.

This module provides:

• behaviour callbacks that every specification must implement,
• a use macro that generates those callbacks from a concise DSL,
• def_transition/3 for declaring transitions,
• default error handling that can be overridden per specification.

Configuration Options

Pass options to use Spex.Specification, ....

:transition_timeout

Maximum time between two observed transitions for an instance.

• Default: :infinity
• Accepted values: :infinity, integer milliseconds, or %Duration{} (converted via to_timeout/1)
• Used by instance manager timeout checks.

If an instance exceeds this timeout, Spex emits %Spex.Errors.TransitionError{reason: :transition_timeout} and routes it through the specification error_handler/2.

:prune_timeout

Minimum idle time before an instance can be considered for pruning.

• Default: :infinity
• Accepted values: :infinity, integer milliseconds, or %Duration{} (converted via to_timeout/1)

Pruning eligibility also depends on :prunable_states.

:prunable_states

Controls which states are allowed to be pruned after :prune_timeout.

• Default: [] (no states are prunable)
• Accepted values:
  • :all: any current state may be pruned
  • :terminal: only terminal states may be pruned
  • explicit state list, e.g. [:done, :failed]

Terminal states are derived from transitions as states with no outgoing edge.

Transition DSL

Define transitions with def_transition(from_state, action, to_state).

Each call contributes to compile-time metadata used to generate:

• states/0
• actions/0
• transitions/0
• initial_state/0
• terminal_states/0

Duplicate states/actions/transitions are deduplicated.

The initial state is the source state of the first declared transition. If no transitions are declared, initial_state/0 returns nil.

Generated Callbacks

When you use Spex.Specification, the following callbacks are generated automatically:

• transition_timeout/0
• prune_timeout/0
• prunable_states/0
• states/0
• actions/0
• transitions/0
• initial_state/0
• terminal_states/0
• error_handler/2 (delegates to default_error_handler/2 by default)

error_handler/2 is overridable.

Error Handling Contract

error_handler/2 receives (error, caller_pid) and must return:

• :ok to swallow/accept the error condition, or
• {:error, reason} to propagate failure.

Default behaviour in default_error_handler/2:

• logs the error and caller stacktrace,
• returns :ok for:
  • %Spex.Errors.TransitionError{reason: :deviation_still_bisimilar}
  • %Spex.Errors.ImplModelError{reason: :impl_model_not_found}
• returns {:error, error} for all other errors.

Full Example

defmodule MySpec do
  use Spex.Specification,
    transition_timeout: 30_000,
    prune_timeout: %Duration{hour: 1},
    prunable_states: :terminal

  def_transition :idle, :start, :running
  def_transition :running, :complete, :done
  def_transition :running, :fail, :failed

  @impl Spex.Specification
  def error_handler(error, caller) do
    send(caller, {:spec_error, error})
    {:error, error}
  end
end