The initial version of the TLA+ Toolbox was designed and programmed almost entirely by Simon Zambrovski in less than a year. The Toolbox is now being maintained and developed by Daniel Ricketts. Leslie Lamport has acted as mentor.
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.
Another problem we have faced is the difficulty of debugging this kind of interactive application. We have not had the time to do the kind of exhaustive testing that's needed to find and eliminate bugs. In particular, we have not done much testing on platforms other than Windows. We expect there to be many bugs that show up only on other platforms.
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 Leslie Lamport with your feedback.
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.