tla_connect

defmodule TlaConnect.StepError do
  @moduledoc """
  Error raised when a single step fails (state mismatch).
  Carries context about where in the test the failure occurred.
  """
  defexception [:message, :context, :action, :expected, :actual, :diff]

  @type replay_context :: %{kind: :replay, trace: non_neg_integer(), state: non_neg_integer()}
  @type rpc_context :: %{kind: :rpc, run: non_neg_integer(), step: non_neg_integer()}
  @type context :: replay_context() | rpc_context()

  @type t :: %__MODULE__{
          message: String.t(),
          context: context(),
          action: String.t(),
          expected: map(),
          actual: map(),
          diff: String.t()
        }
end

defmodule TlaConnect.TraceGenError do
  @moduledoc "Error raised when Apalache trace generation fails."
  defexception [:message, :exit_code, :stdout, :stderr]

  @type t :: %__MODULE__{
          message: String.t(),
          exit_code: integer() | nil,
          stdout: String.t() | nil,
          stderr: String.t() | nil
        }
end

defmodule TlaConnect.ValidationError do
  @moduledoc "Error raised when trace validation fails."
  defexception [:message, :reason]

  @type t :: %__MODULE__{
          message: String.t(),
          reason: String.t() | nil
        }
end

defmodule TlaConnect.RpcError do
  @moduledoc "Error raised for JSON-RPC communication failures."
  defexception [:message, :code]

  @type t :: %__MODULE__{
          message: String.t(),
          code: integer() | nil
        }
end