https://docs.tlapl.us/ 2026-05-05T12:24:03+00:00 https://docs.tlapl.us/ https://docs.tlapl.us/_media/logo.png text/html 2024-09-28T15:58:10+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/codebase:architecture_toolbox?rev=1727539090&do=diff Architecture of the TLA+ Toolbox (IDE) This paper by Kuppe et al presents the technical architecture of the toolbox in this paper: https://arxiv.org/pdf/1912.10633 text/html 2026-02-07T13:55:36+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/codebase:architecture?rev=1770472536&do=diff Codebase Architecture Walkthrough Modules * pcal: Converts the pcal language into TLA+ that can be run by TLC2. * tla2tex: “Pretty Prints” TLA+ code into LaTeX. This LaTeX can then be used for publishing. * tla2sany: Contains the AST and parsing logic for the TLA+ language. The AST classes generated from parsing are used by TLC2. text/html 2024-09-28T22:40:49+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/codebase:ci_cd?rev=1727563249&do=diff CI/CD overview The CI/CD is currently handled by Github Actions, see: <https://github.com/tlaplus/tlaplus/blob/master/.github/> The tests are run as part of every PR and for every merge to main. The codebase is built against both Mac and Linux. There are no performance testing as the last sponsor has pulled resources around 2022. text/html 2025-03-25T09:17:57+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/codebase:contributing?rev=1742894277&do=diff Contributing to the tools TL;DR: engage maintainers early & often, be surgical in your changes, and write lots of tests. We welcome contributions to this open source project! Before beginning work, please take some time to familiarize yourself with our development processes and expectations. The TLA⁺ tools are used to validate safety-critical systems, so maintaining quality is paramount. The existing code can also be quite complicated to modify and it is difficult to review changes effectively… text/html 2024-10-18T20:18:34+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/codebase:debugging?rev=1729282714&do=diff Debugging and rootcausing issues Start from the MRE Minimum Reproducible Example. Often, if you can get one half of your problem is solved. This is why is so important to provide one when creating issues. The smaller the state graph needed to reproduce the issue, the better. text/html 2024-09-28T22:55:59+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/codebase:devenv?rev=1727564159&do=diff Setting up the development environment For eclipse, you can follow directions here: <https://github.com/tlaplus/tlaplus/tree/master/general/ide> For intellij, if you plan to contribute to tlc, it’s fine to just open the relevant package from there. To build and run tests, you can use the cli. text/html 2024-09-28T15:58:14+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/codebase:idiosyncrasies?rev=1727539094&do=diff Codebase Idiosyncrasies As a 20 year old code base, one can expect idiosyncrasies that do not match current best practice. There are also inherent idiosyncrasies to any language interpreter. Maintaining functionality and performance is the most important concern. However whenever these idiosyncrasies can be removed without compromising those, they should be. text/html 2024-09-28T22:53:20+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/codebase:jpf?rev=1727564000&do=diff Java Path Finder Java Path Finder is a project developed by Nasa for model checking Java bytecode. See <https://github.com/javapathfinder/jpf-core>. JPF is used to test some of the datastructures of tlatools. These tests can be invoked by using: ant -f customBuild.xml compile compile-test test-verify text/html 2025-05-06T21:23:48+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/codebase:liveness?rev=1746566628&do=diff Liveness Checking Algorithm in TLC The algorithm is described in the book: "temporal verification of reactive systems: safety" High-Level Overview The liveness checking algorithm in TLA+ verifies temporal properties in specifications - properties that describe how a system should behave over time. Unlike safety properties (which check that bad things never happen), liveness properties assert that something good eventually happens. text/html 2024-09-28T22:54:40+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/codebase:pluscal?rev=1727564080&do=diff Pluscal (+cal) To learn more about pluscal, the language and how the generation process works check this out: <https://github.com/tlaplus/tlaplus/blob/ab14a33e39c78e4c88e81b664b9a8c916b943cab/tlatools/org.lamport.tlatools/src/pcal/PlusCal.tla>. Changing the pluscal translator The pluscal translator can be thought as the pluscal “compiler” which takes as input pluscal code and produces tla+ in output. text/html 2024-09-28T15:58:15+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/codebase:resources?rev=1727539095&do=diff Resources * Temporal Verification of Reactive Systems: Safety by Zohar Manna, Amir Pnueli. Section 5.5 “Particle Tableaux” is useful to understand the use of Tableaux for liveness verification in tlc codebase. text/html 2024-09-28T16:26:54+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/codebase:start?rev=1727540814&do=diff TLA+ codebase The tlaplus codebase is very complex. There are over 600k lines of code, in over 2000 files, written over 20+ years. And yet as the best distributed systems modelling tool on the market today, maintaining and improving it is critical. text/html 2025-09-23T01:06:05+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/codebase:testing?rev=1758589565&do=diff Building and running tests You will need ant build system. customBuild.xml supports different parameters to tune the tests. They can also be combined. customBuild.xml common commands * compile: recompiles the production code for project. Required if you changed any code in src folder. text/html 2024-09-28T15:58:18+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/codebase:wishlist?rev=1727539098&do=diff Wishlist: List of projects to extend/improve TLA+, TLC, TLAPS or the Toolbox Please also consult the issues tracker if you want to get started with contributing to TLA+. The items listed here likely fall in the range of man-months. TLC model checker (In Progress) Concurrent search for strongly connected components (difficulty: high) (skills: Java, TLA+)