tla_connect

defmodule TlaConnect.Driver do
  @moduledoc """
  Behaviour for implementations under test.

  A driver bridges TLA+ spec states and your Elixir implementation.
  It receives steps (action + state) and returns its current state
  for comparison against the spec.

  ## Example

      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: action}), do: {:error, "unknown action: \#{action}"}

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

  @type step :: %{
          action: String.t(),
          state: map(),
          index: non_neg_integer(),
          nondet_picks: map() | nil
        }

  @doc "Create the initial driver state."
  @callback init() :: term()

  @doc "Execute a single TLA+ action on the implementation."
  @callback step(driver_state :: term(), step :: step()) ::
              {:ok, new_state :: term()} | {:error, term()}

  @doc "Extract a comparable state map from the driver. Keys should be strings matching TLA+ variable names."
  @callback extract_state(driver_state :: term()) :: map()
end