Please Help Us

Leslie Lamport has mentored the development of the TLA+ Toolbox continually, while it has been developed by a small number of people over the years. The initial version was designed and implemented almost entirely by Simon Zambrovski in less than a year; followed by work done by Daniel Ricketts; followed by Markus Kuppe and others.

The Toolbox is written as an Eclipse RCP (Rich Client Platform) application.  This has made it possible to implement a great deal of functionality in a fairly short time.  It has also led to compromises.  There are things we would like the Toolbox to do that it doesn't.  Some of the inadequacies are due to a lack of time; others are because we have been unable to figure out how to implement them in Eclipse--either because Eclipse lacks the necessary functionality, or because we don't know how to do them in Eclipse.

We can use your help.  Let us know about problems you encounter or about any aspect of the Toolbox that you don't like.  We also want to know what important features you feel the Toolbox lacks.  Below is a list of some of the features we are thinking of adding.  We probably won't have time to add them all, so we want to know which of them you would most like.  And we would love your help in debugging and developing the Toolbox.  Contact us on the Google Groups forum or open a new issue at GitHub.

Some Features We May Add

A TLA+ Tutorial

A tutorial on specifying systems with TLA+ and checking the specifications with the TLA+ tools is being written.  It is based on the Toolbox.  The current, incomplete version, is available; see the TLA+ web site. We do not know whether the tutorial will be incorporated within the Toolbox itself.

Better Support for PlusCal

Errors in expressions in a PlusCal algorithm are manifest as parsing errors or TLC errors in the corresponding expressions of the algorithm's TLA+ translation.  We would like to have the Toolbox mark the locations of those errors in the PlusCal code.

The pretty-printer does not yet properly format PlusCal algorithms.  We would like it to.

Support for the TLA+ Proof System

A TLA+ proof checker is under development at the Microsoft Research-Inria Joint Centre.  We expect to add at least a basic level of support for writing and checking proofs within the Toolbox.
↑ TLA+ Toolbox User's Guide