tla_connect

TLA+/Apalache integration for model-based testing in Elixir.

Overview

tla_connect provides tools for integrating TLA+ and Apalache model checking into Elixir test suites. It enables:

• Trace validation: Verify that your implementation matches TLA+ specifications
• Model-based testing: Generate test cases from TLA+ models
• Counterexample replay: Automatically reproduce bugs found by model checkers

Architecture

flowchart TB
    subgraph TLA["TLA+ Specification"]
        Spec[MySpec.tla]
        TraceSpec[TraceSpec.tla]
    end

    subgraph Apalache["Apalache Model Checker"]
        CLI[apalache-mc CLI]
        RPC[JSON-RPC Server]
    end

    subgraph Elixir["Elixir Implementation"]
        Driver[Driver behaviour]
        Emitter[StateEmitter]
    end

    subgraph Traces["Trace Formats"]
        ITF[ITF Traces]
        NDJSON[NDJSON Trace]
    end

    %% Approach 1: Batch Replay
    Spec -->|"generate_traces()"| CLI
    CLI -->|produces| ITF
    ITF -->|"replay_traces()"| Driver

    %% Approach 2: Interactive RPC
    Spec -->|"interactive_test()"| RPC
    RPC <-->|step-by-step| Driver

    %% Approach 3: Post-hoc Validation
    Driver -->|records| Emitter
    Emitter -->|writes| NDJSON
    NDJSON -->|"validate_trace()"| CLI
    CLI -->|checks against| TraceSpec

    classDef tla fill:#e1f5fe,stroke:#01579b
    classDef apalache fill:#fff3e0,stroke:#e65100
    classDef elixir fill:#f3e5f5,stroke:#6a1b9a
    classDef trace fill:#fce4ec,stroke:#880e4f

    class Spec,TraceSpec tla
    class CLI,RPC apalache
    class Driver,Emitter elixir
    class ITF,NDJSON trace

Features

• ITF (Informal Trace Format) parsing and validation
• Apalache CLI integration for trace generation
• Apalache JSON-RPC client for interactive symbolic testing
• Trace generation from TLA+ specifications
• State comparison and diff output for debugging mismatches
• Support for both file-based and RPC-based workflows
• Parallel trace replay via Task.async_stream

Installation

Add tla_connect to your list of dependencies in mix.exs:

def deps do
  [
    {:tla_connect, "~> 0.1.0"}
  ]
end

Quick Start

Approach 1: Batch Trace Replay

Generate traces with Apalache, then replay against your implementation:

defmodule CounterDriver do
  @behaviour TlaConnect.Driver

  @impl true
  def init, do: %{counter: 0}

  @impl true
  def step(_state, %{action: "init"}), do: {:ok, %{counter: 0}}
  def step(state, %{action: "increment"}), do: {:ok, %{counter: state.counter + 1}}
  def step(state, %{action: "decrement"}), do: {:ok, %{counter: state.counter - 1}}
  def step(_state, %{action: action}), do: {:error, "unknown action: #{action}"}

  @impl true
  def extract_state(state), do: %{"counter" => state.counter}
end

# Generate traces from TLA+ spec
{:ok, %{traces: traces}} = TlaConnect.generate_traces(%{
  spec: "specs/Counter.tla",
  inv: "TraceComplete"
})

# Replay all traces against the driver
TlaConnect.replay_traces(CounterDriver, traces)

Approach 2: Interactive Symbolic Testing

Step-by-step symbolic execution via Apalache's explorer server:

client = TlaConnect.Rpc.Client.new("http://localhost:8822")

config = %{
  spec: "specs/Counter.tla",
  init: "Init",
  next: "Next",
  num_runs: 100,
  max_steps: 50,
  seed: 42  # Reproducible runs
}

{:ok, stats, _client} = TlaConnect.interactive_test(CounterDriver, client, config)

IO.puts("Completed #{stats.runs_completed} runs, #{stats.total_steps} steps")

Approach 3: Post-hoc Trace Validation

Record your implementation's execution, then validate against the spec:

alias TlaConnect.Emitter

# Record execution trace
emitter = Emitter.new("trace.ndjson")
emitter = Emitter.emit(emitter, "init", %{"counter" => 0})
emitter = Emitter.emit(emitter, "increment", %{"counter" => 1})
emitter = Emitter.emit(emitter, "increment", %{"counter" => 2})
{_count, _emitter} = Emitter.finish(emitter)

# Validate against TLA+ spec
config = %{
  trace_spec: "specs/CounterTrace.tla",
  init: "Init",
  next: "Next",
  inv: "Inv"
}

{:ok, result} = TlaConnect.validate_trace(config, "trace.ndjson")

case result do
  %{valid: true} -> IO.puts("Trace is valid!")
  %{valid: false, reason: reason} -> IO.puts("Invalid: #{reason}")
end

The Driver Behaviour

The TlaConnect.Driver behaviour connects your Elixir code to TLA+ specs. It defines three callbacks:

@callback init() :: term()
@callback step(driver_state :: term(), step :: step()) ::
            {:ok, new_state :: term()} | {:error, term()}
@callback extract_state(driver_state :: term()) :: map()

Key design decisions:

• Functional state threading -- driver state is passed in and returned, not mutated
• Pattern matching for dispatch -- use Elixir's native pattern matching instead of a switch macro
• Projection-based comparison -- only keys returned by extract_state/1 are compared against the spec, so you can track a subset of spec variables
• String keys -- extract_state/1 should return string keys matching TLA+ variable names

ITF Value Decoding

Apalache ITF traces use special encodings that are automatically decoded:

Parallel Replay

For large trace sets, use parallel replay:

TlaConnect.replay_traces_parallel(CounterDriver, traces,
  max_concurrency: System.schedulers_online()
)

Requirements

• Elixir 1.15 or later
• Apalache (if using trace generation or validation features)

License

MIT License. See LICENSE for details.