# Victoria v0.1.0 - Table of Contents

> Formal-model-driven conformance testing for Elixir implementations using TLA+ traces generated by Apalache.

## Pages

- [Victoria](readme.md)
- [Changelog](changelog.md)
- [Glossary](context.md)

## Modules

- Core verification
  - [Victoria](Victoria.md): The primary API for verifying one fixed formal trace.
  - [Victoria.ITF](Victoria.ITF.md): Loads Victoria's intentionally limited subset of the Informal Trace Format.
  - [Victoria.Model](Victoria.Model.md): Defines the implementation lifecycle used while replaying a trace.
  - [Victoria.Runner](Victoria.Runner.md): Sequentially replays a validated trace through a `Victoria.Model` lifecycle.
  - [Victoria.Step](Victoria.Step.md): A normalized formal state and the transition that produced it.
  - [Victoria.Trace](Victoria.Trace.md): A validated, normalized formal trace.
  - [Victoria.Verifier](Victoria.Verifier.md): Compares expected and observed states using exact Elixir equality (`===`).

- Apalache integration
  - [Victoria.Apalache](Victoria.Apalache.md): Runs a validated Apalache plan and materializes every generated ITF trace.
  - [Victoria.Apalache.Plan](Victoria.Apalache.Plan.md): Describes a pure, non-executing Apalache invocation plan.
  - [Victoria.Apalache.Result](Victoria.Apalache.Result.md): Complete context returned after successful Apalache trace materialization.
  - [Victoria.Apalache.RunDirectory](Victoria.Apalache.RunDirectory.md): Builds deterministic, caller-owned Apalache run directory paths.
  - [Victoria.Spec](Victoria.Spec.md): Identifies the source and optional configuration files for a TLA+ specification.

- Workflow orchestration
  - [Victoria.Workflow](Victoria.Workflow.md): Runs Apalache and verifies every materialized trace against one model.
  - [Victoria.Workflow.Result](Victoria.Workflow.Result.md): Complete result of a successful conformance workflow.
  - [Victoria.Workflow.Verification](Victoria.Workflow.Verification.md): Associates one generated trace with its successful verification report.

- ExUnit integration
  - [Victoria.ExUnit](Victoria.ExUnit.md): ExUnit assertion helpers for Victoria conformance verification.

- Errors
  - [Victoria.Apalache.Error](Victoria.Apalache.Error.md): A structured Apalache execution or trace-materialization failure.
  - [Victoria.ITF.Error](Victoria.ITF.Error.md): A structured ITF read, decode, or validation error.
  - [Victoria.Runner.Failure](Victoria.Runner.Failure.md): Structured failure returned by fixed-trace replay.
  - [Victoria.Spec.Error](Victoria.Spec.Error.md): Describes a filesystem validation failure for a Victoria specification.
  - [Victoria.VerificationFailure](Victoria.VerificationFailure.md): The semantic mismatch returned directly by `Victoria.Verifier.verify/2`.
  - [Victoria.Workflow.Error](Victoria.Workflow.Error.md): A contextual conformance-workflow failure.

- Reports
  - [Victoria.Runner.Report](Victoria.Runner.Report.md): Summary returned after a successful fixed-trace replay.

