Modules
Entry point for Spex runtime APIs and high-level integration.
Application entrypoint for starting the Spex supervision tree.
Compares implementation models against specifications via branching bisimilarity.
Rust NIF wrapper used to execute bisimilarity checks.
Error types used across Spex runtime and persistence boundaries.
DETS backend operation errors.
Alias type wrapper for file-system errors represented by File.Error.
ImplModel loading and lookup errors.
Instance lifecycle errors such as duplicate or missing identifiers.
Macro for defining Spex exception modules with typed reasons and context.
Transition-level error used for deviations and timeout conditions.
Represents the observed implementation model built from runtime transitions.
Loads and persists implementation models in .spex file format.
Behaviour contract plus shared helpers for Spex instance managers.
Instance manager that shards instances across multiple
Spex.InstanceManager.Server processes.
Agent storing the configured distribution factor.
Runtime representation of a specification instance and its observed history.
Abstraction layer for instance storage using DETS.
Core GenServer that manages instances and implementation-model observation.
Single-node instance manager backed by one Spex.InstanceManager.Server process.
Behaviour and DSL for defining specifications through labelled transition systems (LTSs).
Test helpers for preparing and manipulating Spex runtime state.
Mix Tasks
Mix task that checks saved implementation models for bisimilarity.