https://docs.tlapl.us/ 2026-05-19T07:43:57+00:00 https://docs.tlapl.us/ https://docs.tlapl.us/_media/logo.png text/html 2025-11-04T17:32:49+00:00 ahelwer (ahelwer@undisclosed.example.com) https://docs.tlapl.us/creating:jlists?rev=1762277569&do=diff Conjunction & Disjunction Lists Chapter 9 of Crafting Interpreters covers control flow - if, while, for, and all that. TLA⁺ doesn't really have that, because TLA⁺ specifications aren't imperative programs. However, TLA⁺ does have something similar. When specifying a system's actions, we commonly need to do two things: write preconditions or "guards" controlling whether an action can be taken, and specify the set of possible next-state transitions. For the former we use conjunction (aka logical … text/html 2025-11-03T23:15:27+00:00 ahelwer (ahelwer@undisclosed.example.com) https://docs.tlapl.us/creating:safety?rev=1762211727&do=diff Model-Checking Safety Properties This has been a long journey. We learned scanning, then parsing, then how to interpret basic constant expressions. Statements were added next, then we mastered the difficult art of parsing conjunction & disjunction lists. Finally, we learned how to apply operators and move between states. Everything is in place; it is time to write a TLA⁺ model-checker. text/html 2025-11-03T23:08:24+00:00 ahelwer (ahelwer@undisclosed.example.com) https://docs.tlapl.us/creating:actions?rev=1762211304&do=diff Variables, States, and Actions Currently, our implementation is not significantly different from any other ordinary programming language. However, TLA⁺ is not an ordinary language - it isn't even a programming language! TLA⁺ specifications are not programs. Properly speaking, a TLA⁺ specification is a predicate over an infinite sequence of states, where states are an assignment of values to variables. TLA⁺ specs' closest analogue to program execution is enumerating the set of all unique reachab…