TLA Toolbox
What is the Toolbox?
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.
The Toolbox has just recently been released to the world at large. We expect many problems to be reported, and we intend to fix them as fast as we can. 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.
Installing and Running the Toolbox
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.
If You Find a Problem
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.
Downloading the Toolbox
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.
Windows-Family
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.
Important Note: Some buttons don’t work properly on Linux systems that use GTK+ version 2.18 (the latest version). Clicking on the button causes it to appear to be pressed, but nothing else happens. The workaround is to execute the command
set GDK_NATIVE_WINDOWS=true
in a shell and then to launch the Toolbox from that shell. The problem is caused by a change in GTK+ that broke many applications. It should be fixed with the release of Eclipse Platform version 3.5.2, scheduled for late February of 2010.
Mac OS X
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.
Release History
Version 1.1.0 of 4 February 2010
The initial public release.
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.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.
