The TLA Toolbox is an IDE for the TLA+ tools. You can use it to:
- Run the PlusCal translator, with the locations of translation errors marked in the PlusCal code.
- View the pretty-printed versions of your modules.
- Run the TLC model checker. You do this by creating one or more models, which specify the information TLC needs to check the spec: what the spec is, what properties to check, the values to substitute for constant parameters, etc. Among the features the Toolbox provides is an error trace viewer and explorer that allows you to:
- Explore a structured view of the states.
- See exactly what parts of the state are changed in each step.
- Evaluate arbitrary state and action formulas at each step in the trace.
- Run TLAPS, the TLA+ Proof System.
The Toolbox was not released very long ago. We expect many problems remain to be discovered, and we intend to fix them as fast as we can when they are. Check this page or the download page for your system frequently for new releases.
Important Note: The Toolbox supports TLA+2, the new version of the TLA+ language. Essentially all existing TLA+ specifications are legal TLA+2 specs. Click here for a description of TLA+2.
To install the Toolbox, you will need a Java runtime. Please make sure to get a recent version for your operating system. The Toolbox has been developed and tested with various JREs. We recommend using a modern Java 6 Runtime. In order to use the integrated pretty-printer, LaTeX and the Acrobat Reader (or other PDF Viewer) must be installed.
Download the .zip file for your system by clicking on the appropriate link below and unzip it in a convenient location. This will install a directory containing an executable file named toolbox (or toolbox.exe on Windows). To run the Toolbox, just execute that file. However, before doing that, check below to see if there are specific installation instructions for your system.
The instructions that appear on the welcome screen tell you what to do next: namely, read the indicated help page. For now, the help pages are the only user manual that exists for the Toolbox. Read it. Even after using the Toolbox for a while, you’re unlikely to have discovered all its features. Read all the help pages.You never know what you might find in them.
The help pages tell you how to use the Toolbox, and they tell you most of what you need to know about the tools–especially the TLC model checker and the pretty-printer. However, they don’t describe the TLA+ and PlusCal languages. To learn about them, see the Learning page.
The Toolbox works well for us. However, there are a number of minor bugs that haven’t yet been fixed. Moreover, it hasn’t been extensively tested, especially on non-Windows systems. See the Bugs page for instructions on how to see the list of known bugs and how to report a new bug.
Implementing the Toolbox has involved a lot of work — mainly by Simon Zambrovski and Dan Ricketts. They were able to build a sophisticated tool in a short time by using Eclipse. However, this required compromises, and there are some annoying (but not serious) inconveniences in the Toolbox because they either didn’t have the time or the Eclipse expertise to fix them. They have also not had time to do extensive testing, which is hard and time-consuming for this type of graphical interface program. So, please try to be helpful instead of angry if something doesn’t work right. Report the problem if it’s not already in the bug list, and help us fix it if you can. Thanks.
Here are the links to the download pages for different systems. You might want to bookmark the one for your system so you can easily check for new versions.
The Toolbox has been tested on various versions of Microsoft Windows (Windows XP, Windows Vista, Windows 7).
Linux (Gnome, KDE)
The Toolbox has been tested on various versions of Linux using different window manager.
The Toolbox has been tested on different versions of Mac OS X (Leopard, Snow Leopard) using Cocoa Shell.
Important Note: Make sure to have the correct version (32-bit/64-bit) of JVM installed.
Version 1.4.3.a of 17 April 2012
This is an intermediate version containing a minor bug fix.
It is available only by updating. (Select
Check for Updates on the Toolbox’s
Version 1.4.3 of 10 April 2012
- Adds a “Cardinality of largest enumerable set” TLC parameter.
- Fixed the order of definitions and declarations in the MC.tla file.
- Includes TLC version 2.05 of 7 April 2012, which adds the TLCEval operator to the TLC module.
- Includes PlusCal Verion 1.8 of 30 March 2012.
Version 1.4.2 of 17 February 2012
- Selecting a location in an error report and control-clicking jumps to its source in PlusCal code.
- Supports library folders (directories) for modules used in multiple specs.
- Provides a built-in pdf viewer that can be used for viewing pretty-printed modules.
Version 1.4.1 of 19 January 2012
Adds a command for finding the PlusCal code that generates a region of an algorithm’s TLA+ translation.
Adds other editor commands, including one for parenthesis matching.
Fixes some bugs, including ones that occurred when TLC checked large models.
Version 1.4.0 of 16 September 2011
Includes a method for obtaining new releases from inside the Toolbox.
Includes PlusCal Version 1.6, which:
— Slightly changes the syntax for specifying fairness.
— Permits using previously declared macros in a macro definition.
Added the Forget Specification command.
Includes a first release of the distributed version of TLC.
Includes a fix to SANY to support binary, octal, and hex numbers.
Added default overriding of definitions like
Foo == CHOOSE v : v \notin S.
Definition overriding section of advanced model page now opens if there are overrides.
Fixed a TLC bug in overriding instantiated definitions.
Displays timeout as a reason for prover failure.
Version 1.3.1 of 5 April 2011
Includes PlusCal Version 1.5, which adds:
— Fairness specifications
— A somewhat simpler TLA+ translation.
Contains some minor bug fixes.
Version 1.2.1 of 2 October 2010
Added a sophisticated interface for running the TLAPS proof checker.
Added a command for displaying all globally defined symbols.
Added commands for displaying all uses of a symbol.
The Goto Declaration command now works for locally defined symbols.
Added commands for formatting boxed comments.
Made some additional minor changes.
Version 1.1.2 of 6 May 2010
Added trace Explorer, which evaluates expressions on an error trace.
Added folding of proofs to permit reading them hierarchically.
Added TLA Proof Manager menu item that currently does nothing.
Version 1.1.1 of 22 Mar 2010
Fixes TLC bug that made restarting from a checkpoint not work,
plus minor fixes.
Version 1.1.0 of 4 February 2010
The initial public release.