# Quint Connect for Elixir

`quint_connect` brings model-based testing with [Quint](https://quint-lang.org/) to Elixir projects. It generates ITF traces with the Quint CLI, decodes each trace, and replays the actions against an Elixir driver that wraps your implementation.

This package is an Elixir sibling of the Rust [`quint-connect`](https://github.com/quint-co/quint-connect) crate. It keeps the same Apache-2.0 license and ports the core workflow into idiomatic ExUnit.

## Installation

Add `quint_connect` to `mix.exs`:

```elixir
def deps do
  [
    {:quint_connect, "~> 0.2.0", only: :test}
  ]
end
```

Install the Quint CLI separately:

```bash
npm install --global @informalsystems/quint
```

Requirements:

- Elixir 1.19+
- Erlang/OTP 28+
- Quint available on `PATH` when running generated traces

## Quick Start

Write a driver that translates each Quint action into implementation calls:

```elixir
defmodule CounterDriver do
  @behaviour QuintConnect.Driver
  @behaviour QuintConnect.State

  import QuintConnect.Step.Switch

  def init(_opts), do: {:ok, %{"counter" => nil}}

  def step(state, step) do
    quint_switch step do
      init -> {:ok, %{"counter" => 0}}
      inc(amount) -> {:ok, Map.update!(state, "counter", &(&1 + amount))}
    end
  end

  def from_implementation(state), do: {:ok, state}
end
```

For Quint action names that are not valid Elixir identifiers, use string clauses:

```elixir
quint_switch step do
  "MoveX", [corner?, coordinate?] -> move_x(corner? || coordinate?)
  "MoveO", [coordinate] -> move_o(coordinate)
end
```

Required picks return `{:error, {:missing_nondet, name}}` when absent. Optional
picks end in `?` and bind `nil` when absent.

Use the ExUnit DSL to generate Quint traces and replay them:

```elixir
defmodule CounterMBTTest do
  use QuintConnect.Case, spec: "priv/examples/counter.qnt"

  quint_run "counter follows the model",
    driver: CounterDriver,
    max_samples: 10,
    max_steps: 20,
    seed: "1"
end
```

For Quint `test` actions:

```elixir
quint_test "counter property",
  driver: CounterDriver,
  test: "counterWorks",
  max_samples: 10,
  seed: "1"
```

## Driver Contract

The driver `init` callback creates the implementation state. `step/2` receives a `QuintConnect.Step` with:

- `action_taken`: the Quint action name.
- `nondet_picks`: decoded nondeterministic choices.
- `state`: the comparable model state after metadata is removed and `state_path` is applied.

If the driver also implements the state projection callback, replay compares the projected implementation state after every step.

## Configuration

Common options:

| Option | Purpose |
| --- | --- |
| `:seed` | Reproduce Quint traces. |
| `:max_samples` | Number of generated traces. |
| `:max_steps` | Maximum steps for `quint run`. |
| `:n_traces` | Number of generated traces when `:max_samples` is absent. |
| `:main_module` | Quint module passed as `--main`. |
| `:init_action` | Init action name for `quint run`; defaults to `"init"`. |
| `:step_action` | Step action name for `quint run`; defaults to `"step"`. |
| `:backend` | Quint backend for `run` and `test`. |
| `:n_threads` | Threads for the Quint Rust backend. |
| `:invariant` | Single invariant expression/name for `quint run`. |
| `:invariants` | Invariant names for `quint run --invariants`. |
| `:witnesses` | Witness names for `quint run --witnesses`. |
| `:hide` | Variable names hidden from terminal output. |
| `:mbt` | Enables `quint run --mbt`; defaults to `true`. |
| `:state_path` | Path into model state before comparison. |
| `:nondet_path` | Path to a custom action record when not using `--mbt`. |
| `:quint_executable` | CLI executable; defaults to `"quint"`. |
| `:verbosity` | Quint verbosity; defaults to `0` for subprocess runs. |

Environment variables:

| Variable | Purpose |
| --- | --- |
| `QUINT_VERBOSE` | Default verbosity passed to Quint. |
| `QUINT_SEED` | Default seed when no `:seed` option is provided. |

When neither `:seed` nor `QUINT_SEED` is set, `Runner` generates a seed and
passes it to Quint. Replay failures include `QUINT_SEED=...` reproduction text.

## Examples

The `priv/examples/` directory includes:

- `counter.qnt` — minimal MBT flow.
- `tictactoe.qnt` — Rust upstream-style game model using optional picks.
- `two_phase_commit.qnt` — compact protocol model with custom `nondet_path`.

## Local Development

Run the normal suite:

```bash
mix test
```

Run tests that require the Quint CLI:

```bash
mix test --include quint
```

The `:quint` suite includes self-hosted specs under `priv/specs/`. These specs replay through `QuintConnect.Case` and validate the package's own CLI and step extraction behavior.

Release checks:

```bash
mix format --check-formatted
mix test --include quint
mix docs
mix hex.build
```

## Limitations

- ITF decoding covers the value shapes emitted by current Quint traces: bigint, map, set, tuple, records, and variants.
- State comparison is exact. Drivers should project implementation state into the same shape as the Quint model.
- The package shells out to the Quint CLI; it does not embed Quint.

## License

Apache-2.0. See [LICENSE](LICENSE).