defmodule QuintConnect.Driver do
  @moduledoc """
  Behaviour for replaying a Quint trace step on your implementation.

  A driver is an imperative shell around your implementation. `step/2` receives
  a decoded `QuintConnect.Step` and returns the next implementation state.
  """

  @type step :: QuintConnect.Step.t()

  @doc """
  Optional one-time setup before first `step/2`.
  """
  @callback init(opts :: keyword()) :: {:ok, impl_state :: term()} | {:error, term()}

  @doc """
  Apply one specification step to the implementation.
  """
  @callback step(impl_state :: term(), step :: step()) :: {:ok, term()} | {:error, term()}

  @doc """
  Optional default config for this driver.
  """
  @callback config() :: QuintConnect.Config.t()

  @optional_callbacks init: 1, config: 0
end