# tla_connect

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

## Overview

`tla_connect` provides tools for integrating [TLA+](https://lamport.azurewebsites.net/tla/tla.html) and [Apalache](https://apalache.informal.systems/) 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

```mermaid
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
```

| Approach | Direction | Catches |
|----------|-----------|---------|
| 1. Batch Replay | Spec -> Implementation | Implementation doesn't handle a case the spec allows |
| 2. Interactive RPC | Spec <-> Implementation | Implementation doesn't handle a case the spec allows |
| 3. Post-hoc Validation | Implementation -> Spec | Implementation does something the spec doesn't allow |

## 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`:

```elixir
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:

```elixir
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:

```elixir
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:

```elixir
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:

```elixir
@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:

| ITF Encoding | Elixir Type |
|---|---|
| `{"#bigint": "42"}` | integer |
| `{"#set": [...]}` | `MapSet` |
| `{"#tup": [...]}` | list |
| `{"#map": [[k, v], ...]}` | `Map` |

## Parallel Replay

For large trace sets, use parallel replay:

```elixir
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](LICENSE) for details.