Overview
This repository hosts the core TLA⁺ command line interface (CLI) Tools and the Toolbox integrated development environment (IDE).
Its development is managed by the TLA⁺ Foundation.
See http://tlapl.us for more information about TLA⁺ itself.
For the TLA⁺ proof manager, see http://proofs.tlapl.us.
Versioned releases can be found on the Releases page.
Currently, every commit to the master branch is built & uploaded to the 1.8.0 Clarke pre-release.
If you want the latest fixes & features you can use that pre-release.
If you want to consume the TLA⁺ tools as a Java dependency in your software project, Maven packages are periodically published to oss.sonatype.org.
Use
The TLA⁺ tools require Java 11+ to run.
The tla2tools.jar file contains multiple TLA⁺ tools.
They can be used as follows:
java -cp tla2tools.jar tla2sany.SANY -help # The TLA⁺ parser
java -cp tla2tools.jar tlc2.TLC -help # The TLA⁺ model checker
java -cp tla2tools.jar tlc2.REPL # Enter the TLA⁺ REPL
java -cp tla2tools.jar pcal.trans -help # The PlusCal-to-TLA⁺ translator
java -cp tla2tools.jar tla2tex.TLA -help # The TLA⁺-to-LaTeX translator
If you add tla2tools.jar to your CLASSPATH environment variable then you can skip the -cp tla2tools.jar parameter.
Running java -jar tla2tools.jar is aliased to java -cp tla2tools.jar tlc2.TLC.
Developing & Contributing
The TLA⁺ Tools and Toolbox IDE are both written in Java.
The TLA⁺ Tools source code is in tlatools/org.lamport.tlatools.
The Toolbox IDE is based on Eclipse Platform and is in the toolbox directory.
For instructions on building & testing these as well as setting up a development environment, see DEVELOPING.md.
We welcome your contributions to this open source project!
TLA⁺ is used in safety-critical systems, so we have a contribution process in place to ensure quality is maintained; read CONTRIBUTING.md before beginning work.
License & Copyright
Copyright © 199? HP Corporation
Copyright © 2003 Microsoft Corporation
Copyright © 2023 Linux Foundation
Licensed under the MIT License.