Apalachex

Safe, deterministic Apalache execution and artifact management for Elixir.

Apalachex validates TLA+ inputs, constructs shell-free Apalache plans, runs exactly Apalache 0.58.3, and returns ordered paths to retained ITF files. It does not open, decode, or interpret ITF contents. Version 0.2.0 supports building and execution on POSIX systems only.

Installation

Add apalachex to the dependencies in mix.exs:

def deps do
  [
    {:apalachex, "~> 0.2.0"}
  ]
end

Apalachex is POSIX-only. Its production dependencies require system make and a POSIX C compiler.

Apalache 0.58.3 must be available as apalache-mc on PATH, or supplied with the :executable option.

Usage

{:ok, spec} =
  Apalachex.Spec.new(
    source: "Counter.tla",
    config: "Counter.cfg"
  )

run_directory =
  Apalachex.RunDirectory.build(
    spec,
    generated_at: DateTime.utc_now(),
    suffix: "a1b2c3"
  )

plan =
  Apalachex.Plan.new(
    spec,
    mode: :simulate,
    length: 10,
    max_run: 5,
    run_directory: run_directory
  )

{:ok, result} = Apalachex.run(plan, timeout: 30_000)
result.itf_paths

Every reserved run directory is retained. Its apalachex-run.json manifest records the running and completed lifecycle. A successful result always has at least one absolute top-level regular .itf.json path, sorted lexically.

Timeout values are milliseconds. The default is :infinity. A finite timeout bounds only the wait for the main Apalache command, not the total duration of run/2. Execution remains synchronous. The version probe has a fixed 5,000 ms timeout and creates no run directory or manifest if it times out.

A timed-out run retains its run directory and partial files, does not classify partial ITFs, and records the existing completed/failed manifest outcome. Caller-death cleanup belongs to the internal process manager. A retained running manifest means that no terminal Apalachex outcome was committed.

Supported boundary

• Elixir ~> 1.18
• Apalache exactly 0.58.3 or v0.58.3
• POSIX build and execution only
• synchronous execution without a shell
• no cancellation API, asynchronous API, recovery, or ITF interpretation

Development

asdf plugin add just https://github.com/olofvndrhr/asdf-just.git
asdf install just 1.54.0
just setup
just test
just check
just docs
just package-audit
just consumer-smoke
just test-apalache

just setup requires asdf 0.16.5, system make, and a POSIX C compiler. Set CC to select the compiler; when CC is unset, cc is used. These native host prerequisites are not managed by .tool-versions. After it checks them, just setup installs the pinned tools from .tool-versions. The consumer and real-Apalache checks require Apalache 0.58.3; the latter is installed by the owned asdf plugin and selected by the repository toolchain.

Maintainer release

Update the version in mix.exs and add its dated changelog section. Commit and push the prepared main, ensure CI is green, then run just release.

The command publishes the prepared version to Hex and creates its GitHub tag and release. It does not prepare, edit, commit, or push main.

License

MIT. See LICENSE.