defmodule TlaConnect do
  @moduledoc """
  Model-based testing with Apalache TLA+ model checker for Elixir.

  Provides three complementary approaches:

  1. **Batch Trace Replay** (`TlaConnect.Replay`) — Generate ITF traces offline
     and replay against a `TlaConnect.Driver` implementation.

  2. **Interactive Symbolic Testing** (`TlaConnect.Interactive`) — Step-by-step
     exploration via Apalache's JSON-RPC server.

  3. **Post-hoc Trace Validation** (`TlaConnect.Emitter` + `TlaConnect.Validator`) —
     Record execution traces as NDJSON, validate against a TLA+ spec.
  """

  # ITF parsing
  defdelegate decode_value(raw), to: TlaConnect.Itf, as: :decode_value
  defdelegate parse_trace(json), to: TlaConnect.Itf, as: :parse_trace

  # File loading
  defdelegate load_trace(path), to: TlaConnect.Loader
  defdelegate load_traces_from_dir(dir), to: TlaConnect.Loader

  # Trace generation
  defdelegate generate_traces(config), to: TlaConnect.Apalache
  defdelegate generate_traces!(config), to: TlaConnect.Apalache

  # Approach 1: Batch replay
  defdelegate replay_trace(driver_mod, trace, trace_index \\ 0), to: TlaConnect.Replay
  defdelegate replay_traces(driver_mod, traces), to: TlaConnect.Replay
  defdelegate replay_traces_with_progress(driver_mod, traces, progress_fn), to: TlaConnect.Replay
  defdelegate replay_traces_parallel(driver_mod, traces, opts \\ []), to: TlaConnect.Replay
  defdelegate replay_trace_str(driver_mod, json, trace_index \\ 0), to: TlaConnect.Replay

  # Approach 2: Interactive
  defdelegate interactive_test(driver_mod, client, config), to: TlaConnect.Interactive
  defdelegate interactive_test_with_progress(driver_mod, client, config, progress_fn), to: TlaConnect.Interactive

  # Approach 3: Emitter + Validator
  defdelegate validate_trace(config, trace_path), to: TlaConnect.Validator
  defdelegate ndjson_to_tla_module(objects), to: TlaConnect.Validator

  # Comparison utilities
  defdelegate value_equals(a, b), to: TlaConnect.Compare
  defdelegate states_match(spec, impl), to: TlaConnect.Compare
  defdelegate project_state(spec, keys), to: TlaConnect.Compare

  # Diff
  defdelegate state_diff(expected, actual), to: TlaConnect.Diff
end