tlaplus

开源

TLC 是一种用于 TLA+ 编写的规范的模型检查器。TLA+ 工具箱是一个用于 TLA+ 的 IDE。

3.0K stars0 点赞0 次浏览

工具介绍

TLC 是一种用于 TLA+ 编写的规范的模型检查器。TLA+ 工具箱是一个用于 TLA+ 的 IDE。

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 central.sonatype.org.

Use

The TLA⁺ tools require Java 11+ to run.

To use TLA⁺ from a graphical interface, see the TLA⁺ VS Code extension. The Eclipse-based TLA⁺ Toolbox GUI is also available from this repository, but it is currently unmaintained.

Get tla2tools.jar from the releases to use the tools from the command line. The tla2tools.jar file contains multiple TLA⁺ tools; after adding tla2tools.jar to your CLASSPATH, the tools can be used as follows:

bash

EXPORT CLASSPATH=tla2tools.jar
java tla2sany.SANY -help  # The TLA⁺ parser
java tlc2.TLC -help       # The TLA⁺ model checker
java tlc2.REPL            # Enter the TLA⁺ REPL
java pcal.trans -help     # The PlusCal-to-TLA⁺ translator
java tla2tex.TLA -help    # The TLA⁺-to-LaTeX translator
java tla2sany.xml.XMLExporter -help # Export TLA⁺ parse tree as XML

Running java -jar tla2tools.jar is aliased to run tlc2.TLC.

For more information on using & consuming the TLA⁺ tools, see USE.md.

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.