apalachex

# 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.1.0 supports
execution on POSIX systems only.

## Installation

Add `apalachex` to the dependencies in `mix.exs`:

```elixir
def deps do
  [
    {:apalachex, "~> 0.1.0"}
  ]
end
```

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

## Usage

```elixir
{: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)
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.

## Supported boundary

- Elixir `~> 1.18`
- Apalache exactly `0.58.3` or `v0.58.3`
- POSIX execution only; Windows is rejected after strict option validation and
  before executable discovery, version probing, run-directory allocation,
  manifest creation, or process execution
- synchronous execution without a shell
- no timeout, cancellation, supervision, cleanup, or ITF interpretation

## Development

```sh
mix check
mix test --include apalache test/apalachex/real_apalache_test.exs
mix docs --warnings-as-errors
scripts/audit_package.sh
scripts/consumer_smoke.sh
```

## License

MIT. See [LICENSE](LICENSE).