TLA Toolbox

People who use the TLA+ tools could seek a way of integrating the functionality of their features by using a single application. TLA Toolbox integrated development environment was designed in order to offer users the choice of using the TLA+ tools in order to create custom specifications, perform PlusCal translations or print the resulted models. It will allow them to also run the TLC model checker or TLAPS, the proofing system.

TLA Toolbox comes packed with a clean interface that carries a classic editor layout, where one can easily create new specifications, load the corresponding models and view their contents. A dedicated bottom log viewer will alert users of any errors or occurring events and the disk space availability will also be listed.

People will be able to navigate line-by-line through the loaded models and the application will allow them to run a translation using the PlusCal Algorithm. The side panel where the model and specification structure are stored can also be toggled, in order to gain more viewing space.

Users will be able to create their own custom specifications, clone their models or run them in order to see how they perform. Being a collection of tools, means that the application will also provide users with access to other external features.

To this end, they will be able to perform check-ups using the TLC Model Checker or proofing with the TLA Proof Manager. This can save precious time, as users will not need to open the external applications separately in order to perform the required tasks.

This utility addresses people who require a reliable solution for creating specifications using the TLA+ IDE tools, but from a single platform. It will allow them to easily load new specifications, create models and view their corresponding contents on its classic editor viewer. However, novice users are advised to consult the interactive help module provided, as the application will require solid IDE knowledge.