TLAP

TLAP is a portable CLI that lets you run TLA+ tools easily from anywhere. It wraps tla2tools.jar in Docker so you can use tlap without installing Java locally.

Why TLAP

• Run TLA+ from any directory (tlap on your PATH)
• Keep host setup minimal (runtime dependency is Docker)
• Use both high-level workflows (init, run, translate) and raw passthrough

Quick Start

Private repository use is assumed.

1. Open Releases: https://github.com/skoya76/tlap/releases
2. Download the latest tlap_linux_amd64 binary.
3. Place it as ~/.local/bin/tlap and make it executable.
4. Run tlap -- tlc2.TLC -help to verify installation.

Installation

Option 1: Manual Release Download (recommended)

1. Open Releases: https://github.com/skoya76/tlap/releases
2. Download tlap_linux_amd64 from the version you want (or latest).
3. Place the binary at ~/.local/bin/tlap.
4. Ensure it is executable and that ~/.local/bin is on your PATH.

Option 2: Installer Script

Run install.sh from a local clone, or set repository explicitly:

export TLA_REPOSITORY="<owner>/<repo>"
export GITHUB_TOKEN="<token-with-repo-read-access>"
./install.sh

Installer behavior:

• Downloads a release asset from GitHub Releases
• Installs it as ~/.local/bin/tlap
• For private repos, uses GITHUB_TOKEN (or GH_TOKEN) when provided

Usage

Full Passthrough

Everything after -- is passed through as-is:

tlap -- tlc2.TLC -help
tlap -- pcal.trans sample.tla

Unknown subcommands are also passed through automatically:

tlap tlc2.TLC -help

Convenience Commands

tlap init <project>

Create a new project directory with starter files (.tla, .cfg, sample.tla, .tlactl).

tlap translate <spec.tla>

Run PlusCal translation via pcal.trans.

tlap run [spec] [--cfg file] [--workers n] [--no-translate] [-- <extra tlc args>]

Run TLC, with optional auto-translation when --algorithm is found.

Example:

tlap run MySpec.tla --cfg MySpec.cfg --workers 4 -- -deadlock -cleanup

Official TLA+ Documentation

For TLA+/TLC/PlusCal language and tool semantics, use upstream documentation:

• TLA+ docs wiki: https://docs.tlapl.us/
• TLC docs: https://docs.tlapl.us/using%3Atlc%3Astart
• Official tla2tools.jar releases: https://github.com/tlaplus/tlaplus/releases
• TLA+ project home: https://dl.tlapl.us/

TLAP focuses on portability and execution ergonomics, while detailed language/tool behavior is delegated to official references.

Configuration

Environment Variables

• TLA_DOCKER_IMAGE: Docker image name (default: tlap:latest)
• TLA2TOOLS_URL: Override tla2tools.jar download URL (used when image is built)
• TLA_DOCKER_BUILD=always: Force image rebuild on every run
• TLA_REPOSITORY: Release source repository (required unless detected from local git remote)
• TLA_RELEASE_ASSET: Override asset name (default: tlap_linux_amd64)
• TLA_VERSION: Release version (default: latest)
• GITHUB_TOKEN or GH_TOKEN: token used to download assets from private releases

Installer Scope

• Installer target platform is currently linux/amd64 only.

How TLAP Works

At runtime TLAP:

1. Ensures the configured Docker image exists (or builds it)
2. Mounts your current directory into /work in the container
3. Runs java -cp /opt/tla2tools.jar <tool-class> ...

This keeps usage portable while preserving normal file-based workflows.

Release Process

This repository includes a GitHub Actions workflow that creates releases on v0.* tags.

git tag v0.1.0
git push origin v0.1.0

The workflow builds and uploads:

• tlap_linux_amd64

Contributing

Issues and pull requests are welcome.

License

Apache License 2.0. See LICENSE for the full text.