https://docs.tlapl.us/ 2026-04-26T10:21:41+00:00 https://docs.tlapl.us/ https://docs.tlapl.us/_media/logo.png text/html 2025-07-15T16:57:30+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/learning:distributed?rev=1752598650&do=diff Distributed mode and Cloud mode [deprecated] Please Note: this feature is on track to be deprecated. More info can be found here: <https://github.com/tlaplus/tlaplus/issues/718> When we need to model check a model that has a large state space, we can run tlc in distributed mode. In this mode, TLC will run in multiple machines. Cloud mode is distributed mode, but automatically spawns up instances in the supported clouds. text/html 2025-08-20T20:41:57+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/learning:exercises?rev=1755722517&do=diff Exercises This page provides some execises you can use when learning tla+ or to brush your memory on the language. Finder Exercises These exercises ask you to write a spec that finds a solution to a problem, like a path through a maze. You can do this by writing an invariant saying "the goal state is impossible". TLC will then "solve" the problem by breaking the invariant! text/html 2024-10-19T00:35:30+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/learning:faq?rev=1729298130&do=diff FAQ Do you need to know math to learn TLA+? To learn TLA+ you need to be able to think mathematically and precisely. While a deep understanding of advanced mathematical concepts is not necessary, a solid foundation in basic mathematical concepts is important. Here's why: text/html 2025-07-26T17:56:29+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/learning:pluscal?rev=1753552589&do=diff Learning PlusCal PlusCal is an algorithm language—a language for writing and debugging algorithms. It is especially good for algorithms to be implemented with multi-threaded code. Instead of being compiled into code, a PlusCal algorithm is translated into a TLA+ specification. An algorithm written in PlusCal is debugged using the TLA+ tools—mainly the TLC model checker. Correctness of the algorithm can also be proved with the TLAPS proof system, but that requires a lot of hard work and is seldo… text/html 2025-08-20T09:47:06+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/learning:start?rev=1755683226&do=diff Learning TLA+ and Model Checking This page lists some external resources one could use to learn more about TLA+ and related topics. First things first: * Setup your IDE. Visual Studio code with tlaplus plugin tlaplus plugin is recommended. * If you have questions or if you feel stuck at any point, reach out to the text/html 2025-01-02T16:32:09+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/learning:symmetry?rev=1735835529&do=diff Symmetry <https://jack-vanlightly.com/blog/2024/12/5/an-introduction-to-symmetry-in-tla> text/html 2025-01-02T16:31:16+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/learning:tla_comparisons?rev=1735835476&do=diff TLA+ vs xxx This page describes how does TLA+ compare to over specification and model checking tools. TLA+ vs FizzBee Not a full comparison, but this blog post is a good starting point: <https://jack-vanlightly.com/analyses/2024/12/5/verifying-kafka-transactions-diary-entry-4-writing-an-initial-fizzbee-spec> text/html 2025-08-20T10:20:18+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/learning:tla_summary?rev=1755685218&do=diff Summary You can access to a quick pdf summary about the tla+ language here: <https://lamport.azurewebsites.net/tla/summary-standalone.pdf>. This is a web accessible version. ---------- Module-Level Constructs Construct Description module M Begins the module or submodule named M. extends M1, ..., Mn Incorporates the declarations, definitions, assumptions, and theorems from the modules named