The TLA+ Toolbox

Leslie Lamport

Last modified on Thu 23 December 2021 at 18:37:52 PST by lamport -->

You'll miss a lot on this web site unless you enable Javascript in your browser.

What is the Toolbox?       [show]

The TLA Toolbox is an IDE (integrated development environment) for the TLA+ tools.  You can use it to:
  • Create and edit your specs, with the locations of parsing errors marked in the modules.

  • 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.  The Toolbox allows you to explorer an error trace produced by TLC—for example, by evaluating arbitrary formulas at each step in the trace.

  • Run the TLA+ proof system.
The Toolbox was written by Simon Zambrovski and improved by Markus Kuppe and Daniel Ricketts.

Users who would prefer a more lightweight IDE for TLA+ may want to try the Visual Studio Code extension for TLA+.  However, it lacks many of the Toolbox's features.

Obtaining the Toolbox       [show]

Downloading the Toolbox       [show]

Below is a link to a page from which you can download the versions of the Toolbox for various systems, the name of the file indicating which system it is for.  For example,  TLAToolbox-1.4.5-linux.gtk.x86_64.zip  is for 64-bit Linux.  Please thank Microsoft and HP for the open-source release of the code by reading the following agreement.

By installing, copying, or otherwise using this software, you agree to be bound by the terms of its license.   Read the license.

You can download the Toolbox from either of these sites:

       -- DOWNLOAD FROM GITHUB --        -- ALTERNATE DOWNLOAD SITE --

Put the downloaded zip file in a convenient folder.

Installing the Toolbox       [show]

Here are the instructions for the different operating systems.

Windows

Download the zip file into a convenient folder.  Extract the contents of the file by right-clicking on it in the File Explorer and selecting Extract All.  You can choose what folder to put the extracted files in; the default is a subfolder of the folder containing the zip file.  Select the Show extracted files when complete option and click on Extract.  The extracted files will be in a subfolder named toolbox  Open that subfolder.  You can run the Toolbox by double-clicking on the file called toolbox or toolbox.exe.  But before doing that, you probably want to make it easier to run the Toolbox later by doing one of the following:
  • Create a shortcut by right-clicking on the file and selecting Create shortcut, then move the shortcut to the desktop or some other convenient location.  You can run the Toolbox by double-clicking on the shortcut.
  • Right-click on the file and select Pin to Start or Pin to taskbar.  You can then run the Toolbox from the Start Menu or the taskbar.

When you first run the Toolbox, the operating system may tell you it's not safe to run and it won't let you run it.  Somewhere on the warning window, perhaps cleverly hidden, is something you can click to tell the operating system to run it anyway.  If you can't find it, look the warning up on the Web or post a cry for help on the TLA+ Google group.

Mac OS

Download the file and, if necessary, unzip it by double-clicking on it.  (Depending on how your browser and system are set up, the downloaded file may already be unzipped.)  This results in an application bundle called TLA+ Toolbox.app, which you can move to the Applications folder.  The Toolbox can be started by double-clicking that application. 

When you try to open the Toolbox for the first time, Mac OS will probably be reluctant to let you run it.  Try to control-click (right-click) on the application, choose Open from the drop-down menu, and confirm that you want to open the application in the subsequent dialog box.  If this doesn't work, look on the Web or ask for help on the TLA+ Google group.

For Homebrew users, a Toolbox Cask is available with the name tla-plus-toolbox.

Linux

Extract the contents of the zip file to a convenient directory.  Open the toolbox subdirectory.  You can then run the Toolbox by executing the toolbox file in that subdirectory. 

Installing pdflatex       [show]

You need to install pdflatex only if you want to run the TLA+ pretty-printer (with the Toolbox's Produce PDF Version command).  The pdflatex program is distributed as part of a LaTeX installation, and it will already be installed if you use TeX or LaTeX.  It may also be installed if you're running Linux.  Run the command 
    pdflatex -help
in a command shell / terminal window to see if it's already installed.  If it isn't, you can obtain it by installing LaTeX on your computer.  The LaTeX Project has links to various sources of LaTeX.  Here are ones that we recommend for different operating systems.  Whatever method you use, you should check with a command shell that it is installed.  (Open a new command shell after you install LaTeX.)

Windows

MikTeX comes with detailed installation instructions.

Mac OS

The MacTeX web page points to simple instructions for downloading the file MacTeX.pkg.  It claims that running the file provides straightforward instructions for installing LaTeX.  You can ignore instructions on how to write a LaTeX document.

If you already use a manager such as MacPorts or Homebrew for open-source software packages, you can use it to install LaTeX.  Please refer to the instructions of your package manager for details.

Linux

The provider of your Linux software should also be able to provide you with LaTeX for it.

Using the Toolbox       [show]

When you run the Toolbox, 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.

If You Find a Problem      [show]

The Toolbox works reasonably well, but there are a number of minor bugs that haven't yet been fixed.  The current bug repository, where you can look for known bugs and report new ones, is:

    The GitHub Repository tlaplus Issues page

Bugs from before 2013, including many that were considered not worth the trouble of fixing, are in:

    The Bugzilla Database

Implementing the Toolbox has involved a lot of work by few people. 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.  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.

Release History       [show]

Version 1.7.1 of 31 December 2020    [details]
- Eliminates bug in version 1.7.0 that caused some TLC error traces not to be shown.
- Eliminates a number of other bugs; see the Changelog for a list.

Version 1.7.0 of 26 April 2020    [details]
- Many features have been added to the Toolbox.
- Various features have been added for running TLC from a command line.
- Many bugs have been fixed, including a TLC bug in reporting liveness checking failure.
There have been too many new features and bug fixes to list here.  See the detailed list.

Version 1.6.0 of 11 July 2019    [details]
- Users can choose to have the Toolbox send us anonymous statistics about how
  they use TLC.  We encourage you to do so.
- The Toolbox's interface for running TLC has been redesigned to make it easier to use.
- Installing the Toolbox now automatically installs Java, so there is no need to install
  it manually.
- Features have been added to make error-trace exploration expressions more
  powerful and easier to write.  Click on ? in the menu for adding an exploration
  expression for details.
- There is now a TLC profiler to help find errors in a spec and to help optimize
  model checking.  See Profiling in the Features section of the TLC Options Page
  help page.

Version 1.5.7 of 18 July 2018    [details]
- 32-bit versions of the Toolbox are no longer available.
- Bugs in the TLC implementation of the standard Bags module have been corrected.
- An experimental standard module Randomization, described here, has been added.
- Numerous improvements have been made to TLC and the Toolbox.

Version 1.5.6 of 30 January 2018    [details]
- Corrects the TLC bug described here.
- Fixes a bug in the Toolbox's update mechanism that would cause it to make TLC
  impossible to run.
- Fixes a TLC bug that caused it to stop with an integer overflow exception after many
  hours of model checking.

Version 1.5.5 of 5 January 2018    [details]
- Provides only a partial fix of the TLC bug fixed in version 1.5.6.

Ancient Release History       [show]

Version 1.5.4 of Approximately 7 October 2017    [details]
- All known issues with Java9 and macOS High Sierra have been fixed.
- The Toolbox can now display a visual representation of a small state graph.
- TLC's error reporting has been improved.
- A number of features have been added and bugs fixed in the Toolbox and TLC.

Version 1.5.3 of 14 April 2017    [details]
- Bug fixes include eliminating incorrect error traces in TLC liveness checking.
- Execution by multiple worker threads in TLC has been speeded up.
- The Toolbox can now be set as the default program for running .tla files.
- The built-in PDF viewer is now the default on Windows and Linux.
- TLC can be run on multiple EC2 or Azure instances by button pushing.
- An apt repository is provided for Linux installations.

Version 1.5.2 of 21 December 2015    [details]
- Added a quick access dialog for showing and selecting models and modules.
- The toolbox now maintains backups of previous versions of modules.
- Models now have a field for free-form comments.
- Only one Toolbox instance can now be run at a time.
- A -userFile parameter allows redirecting Print/PrintT output to a file.
- Not all states of very long error traces are displayed initially.
- Ended support for 32-bit Toolbox releases on Mac OSX.
- Several optimizations and bug fixes were made.

Version 1.5.1 of 1 June 2015    [details]
- Fixes several bugs in TLC and a bug in the Toolbox's trace explorer

Version 1.5.0 of 11 May 2015    [details]
- Distributed TLC in the Cloud--significantly improves distributed TLC.
- Significantly speeds ups TLC's liveness checking.
- Improvements to the Decompose Proof Command.
- Improvements to the TLC Errors view, including ability to show trace
   in reverse order.
- Has some changes to the way the Toolbox handles its subwindows.
- Fixes all known bugs in TLC's liveness checking.
- Fixes TLC bug of infinite looping if a recursively defined operator is used
   as an operator argument in its own definition.
- Numerous bug fixes.

Version 1.4.8 of 25 February 2014
- Added a feature to Renumber Proof command.
- Disallowed <*> and <+> in names of named proof steps.
- Minor bug fixes to Toolbox and TLC.
- Corrected definition of Tail in standard Sequences module.

Version 1.4.7 of 24 April 2013
- Fixes bugs in the Toolbox's Decompose Proof command

Version 1.4.6 of 18 April 2013
- Fixes bug in PlusCal translation of fairness for algorithms with procedures.
- Adds handling of strings to TLC's implementation of Tail and SubSeq.
- Fixes a minor TLATeX bug.

Version 1.4.5 of 22 February 2013
- The Decompose Proof Command has been added to the Toolbox editor.
   It makes it easy to perform the standard hierarchical decompositions of a proof
   based on the structure of the formula to be proved.
- A few minor bugs have been fixed.

Version 1.4.4 of 30 November 2012
- There have been numberous changes to distributed TLC and how to run it.
- Syntax coloring of PlusCal algorithms was added.
- TLATeX now formats PlusCal algorithms.
- Support for library folders required by Version 1.1.1 of TLAPS has been added.

Version 1.4.3.c of 24 May 2012
Version 1.4.3.b of 24 April 2012
Version 1.4.3.a of 17 April 2012
    These are intermediate versions that contain the current version of TLAPS.tla and
       fix mostly minor bugs.
    Version 1.4.3.c fixes a bug that can cause an updated version of the Toolbox
       to use an earlier version of TLC.
    The latest version is available only by updating.  (Select  Check for Updates 
       on the Toolbox's  Help  menu.)

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
- Contains a new editor command for jumping from a region in the TLA+ translation
  of a PlusCal algorithm to the region of PlusCal code that generated it.
- Introduces some additional editor commands, including one for parenthesis matching.
- Fixes a number of 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 specifation in a PlusCal algorithm.
    * Translation simplifications, including omission of the pc variable when not needed.
- Contains a number of 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.
- Various minor bug fixes.

Version 1.1.0 of 4 February 2010
- The initial public release.