# 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.1.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

  alias QuintConnect.Step

  def init(_opts), do: {:ok, %{"counter" => nil}}
  def step(_state, %Step{action_taken: "init"}), do: {:ok, %{"counter" => 0}}

  def step(state, %Step{action_taken: "inc"} = step) do
    with {:ok, amount} <- Step.nondet(step, :amount) do
      {:ok, Map.update!(state, "counter", &(&1 + amount))}
    end
  end

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

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`. |
| `: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"`. |
| `: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"`. |

Environment variables:

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

## 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).