The TLA Toolbox

Last modified 14 March 2014

Contents

What is the Toolbox? Installing and Running the Toolbox If You Find a Problem Downloading the Toolbox System Specific Instructions Release History

What is the Toolbox?

The TLA Toolbox is an IDE (integrated development environment) for the TLA+ tools.  You can use it to:

Installing and Running the Toolbox

To install the Toolbox, you will need a Java runtime.  (You will probably need version 1.6.)  Just 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 Resources section of the TLA+ home 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 TLA Toolbox Bugs page for instructions on how to see the list of known bugs and how to report a new bug.  Here is a list of the most important bugs we know about.

Implementing the Toolbox has involved a lot of work--mainly by Simon Zambrovski, Dan Ricketts, and Markus Kuppe.  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 has 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

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.zip  is for a 32-bit Linux system and  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.

       -- DOWNLOAD THE TOOLBOX --

System Specific Instructions

Linux

On some versions of Ubuntu, the Toolbox's menus may not be displayed.  To fix this, you can launch the Toolbox with a shell script that sets the environment variable UBUNTU_MENUPROXY to 0--for example the shell script:

   #!/bin/bash
   export UBUNTU_MENUPROXY=0 
   toolbox/toolbox

Release History

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.


Contact Us Terms of Use Trademarks Privacy Statement ©2010 Microsoft Corporation. All rights reserved.Microsoft