Modules
The primary API for verifying one fixed formal trace.
Runs a validated Apalache plan and materializes every generated ITF trace.
A structured Apalache execution or trace-materialization failure.
Describes a pure, non-executing Apalache invocation plan.
Complete context returned after successful Apalache trace materialization.
Builds deterministic, caller-owned Apalache run directory paths.
ExUnit assertion helpers for Victoria conformance verification.
Loads Victoria's intentionally limited subset of the Informal Trace Format.
A structured ITF read, decode, or validation error.
Defines the implementation lifecycle used while replaying a trace.
Sequentially replays a validated trace through a Victoria.Model lifecycle.
Structured failure returned by fixed-trace replay.
Summary returned after a successful fixed-trace replay.
Identifies the source and optional configuration files for a TLA+ specification.
Describes a filesystem validation failure for a Victoria specification.
A normalized formal state and the transition that produced it.
A validated, normalized formal trace.
The semantic mismatch returned directly by Victoria.Verifier.verify/2.
Compares expected and observed states using exact Elixir equality (===).
Runs Apalache and verifies every materialized trace against one model.
A contextual conformance-workflow failure.
Complete result of a successful conformance workflow.
Associates one generated trace with its successful verification report.