Entry point for Spex runtime APIs and high-level integration.

Spex tracks observed runtime behaviour as implementation models and compares those models to declarative specifications (LTSs). It is designed for:

• online runtime observation (init_instance*, transition*),
• detection/reporting of behavioural deviations,
• export and offline checking of derived implementation models.

Quick Start

1. Define one or more specifications with Spex.Specification.
2. Start Spex (or an instance manager) under a supervisor.
3. Initialize instances with init_instance/4.
4. Feed observed transitions with transition/3.

Minimal usage example:

:ok = Spex.init_instance(MySpec, :order_123)
:ok = Spex.transition(:order_123, :pay, :paid)
:ok = Spex.transition(:order_123, :ship, :shipped)

How To Start Spex

There are two primary integration styles.

1) Spex As Its Own OTP Application

This is the usual setup when the dependency is started normally (runtime: true, default). Your app depends on Spex and Spex boots its own supervision tree.

2) Explicit Supervision (runtime: false)

If Spex is configured with runtime: false, add either Spex or a concrete instance manager directly to your supervision tree:

children = [
  Spex
]

or:

children = [
  {Spex.InstanceManager.SimpleInstanceManager,
   impl_models_dir: "./spex_impl_models",
   dets_dir: "./spex_dets"}
]

or:

children = [
  {Spex.InstanceManager.DistributedInstanceManager,
   distribution_factor: 8,
   impl_models_dir: "./spex_impl_models",
   dets_dir: "./spex_dets"}
]

Online Production Usage

In production, call init_instance/4 when a domain entity begins its tracked lifecycle, then call transition/3 for each observed state change.

Behavioural checks and error handling are driven by the underlying specification (error_handler/2, timeout settings, pruning rules).

ImplModel Derivation During Tests

Spex can derive implementation models from test execution and persist them as .spex files. The main purpose of this derivation flow is to run offline bisimilarity checks with the mix spex task.

Typical flow:

• call Spex.Testing.prepare_for_test_suite/1 in test setup,
• run tests while using normal Spex APIs,
• after suite completion, derived models are exported,
• run mix spex (or mix spex <path>) to validate derived models.

Example:

# test/test_helper.exs
Spex.Testing.prepare_for_test_suite(impl_models_dir: "./test_meta/impl_models/live")

# CI or local verification
# Uses configured :impl_models_dir when no path is given
mix spex

Configuration Entry Point

This module delegates to a compile-time default instance manager selected via config :spex, :instance_manager.

Accepted forms are:

• MyManagerModule
• {MyManagerModule, manager_opts}

Documentation Map

• Spex.Specification: define specifications and options.
• Spex.InstanceManager: behaviour contract for manager implementations.
• Spex.InstanceManager.SimpleInstanceManager: single-node manager setup.
• Spex.InstanceManager.DistributedInstanceManager: sharded manager setup.
• Spex.Testing: test helpers and suite-level model export.
• Spex.ImplModel / Spex.ImplModelStore: model representation and storage.
• Spex.BisimilarityChecker: bisimilarity validation internals.
• Mix.Tasks.Spex: offline bisimilarity checks over saved .spex files.