Coming soon: TLA+ Toolbox
There are various tools available for the TLA+ specification language and PlusCal algorithm language, as described in the Tools section in more detail. An additional tool is coming soon: the TLA+ Toolbox.
In order to enhance the user experience with the tools and simplify the access to the languages some improvements are being developed in the scope of the project run by Microsoft Research and INRIA. Along with the focus on the proof aspect of TLA+, the development of a complete Integrated Development Environment (IDE) for writing and debugging of specifications has been identified as a project goal. The IDE unifies the editors for specifications and models with already existing TLA+ tools for syntax analyze, PlusCal translation and model checking in one application. It includes the console-based TLA+ Tools and enables the use of their whole functionality via rich graphical user interface.
The IDE is currently being finalized and will be available soon. It will include:
- Simple interface for managing specifications
- Integrated TLA+ specification editor with features like:
- SANY integration
- Syntax Highlighting
- Basic content assist
- Error marker support
- and others
- PlusCal Translator integration
- TLC Model Checker integration
- Simple interface for managing models
- Rich model editor
- Extended TLC result display
- Trace Explorer
- and others…
Stay tuned for the TLA+ Toolbox release…
