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. 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.
To install the Toolbox, you will need a Java runtime. (You will
need version 1.8.) 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.
The Toolbox works well for us. However, 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--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 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.
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.
You can download the Toolbox from either of these sites:
-- DOWNLOAD
THE TLA+ TOOLBOX --
-- ALTERNATE DOWNLOAD
SITE --
The 32-bit version of the Toolbox is
available only from the alternate download site. We strongly advise
users of 64-bit computers not to use the 32-bit version.
Version 1.5.6 of 30 January 2018
- 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
- Provides only a partial fix of the TLC bug
fixed in version 1.5.6.
Version 1.5.4 of Approximately 7 October 2017
- 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 have been fixed in
the Toolbox and TLC.
Version 1.5.3 of 14 April 2017
- 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
- 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
- Fixes several bugs in TLC and a bug in the Toolbox's
trace explorer
Version 1.5.0 of 11 May 2015
- 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.
