Link Search Menu Expand Document
Pragmatic Formal Modeling

Tools and Additional Citations

Tools for TLA+

  • TLA+ Toolbox: The fully featured (if somewhat outdated) IDE for TLA+. Includes modeling, document generation, and live syntax checking.
  • VSCode TLA+: Lighter weight IDE with textfile based model configuration. Generally more responsive. The latest alpha version, found here, has a debugger that might be useful to you while getting a handle on the language.

Tools for TLA+ display

  • tla2json: Used to turn trace output from toolbox into json for automatic trace widget generation.
  • LaTex: Used to render the LaTex output of TLA+ to dvi format.
  • dvisvgm: Used to convert the dvi formatted TLA+ specifications into SVGs that could be displayed inline in the website.
  • Code highlighting: Improved / repackaged for Jekyll, but the majority of the code came from this pull request by Tom Lee.

Tools for the website

  • Jekyll: A static site generator. This website heavily relied on the templating functionality Jekyll provides.
  • PlantUML: Used to generate UML diagrams from text.
  • Just the Docs: The theme that was used and modified for this website.

Assets

  • Favicon: Diamond icons created by Vaadin - Flaticon.

Acknowledgments

  • To Liza Knipscher for editing and proofreading tons of text and code.
  • To all the people who wrote the learning material and the tools above, your work was invaluable to the completion of this project.