Packages

tla_connect

0.1.0
0.1.0

Model-based testing with Apalache TLA+ model checker for Elixir.

HexDocs

Current section

Files

Jump to
Readme
1 Version
2 Dependencies
Dependants
Files
Activity
tla_connect lib tla_connect.ex
Raw

lib/tla_connect.ex 

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