https://docs.tlapl.us/ 2026-05-19T06:47:38+00:00 https://docs.tlapl.us/ https://docs.tlapl.us/_media/logo.png text/html 2025-11-03T23:08:24+00:00 Anonymous (anonymous@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… text/html 2025-09-02T19:27:05+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/creating:closures?rev=1756841225&do=diff Parameters as Closures Remember way back at the start of the Functions, Operators, and Parameters chapter when operators were described as being like macros? This was very literal - the expressions provided as parameters to an operator should be substituted into the operator body itself, text/html 2025-06-19T16:31:49+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/creating:evaluation?rev=1750350709&do=diff Evaluating Constant TLA⁺ Expressions Now that we can parse expressions, let's evaluate them! Here we follow the material in Chapter 7 of Crafting Interpreters. It's an exciting chapter, so let's jump in. Section 7.1: Representing Values In section 7.1 we define a mapping from language values to internal Java values. Our mapping for TLA⁺ is fairly similar to Lox, although we use text/html 2025-05-13T15:58:58+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/creating:expressions?rev=1747151938&do=diff Parsing Constant TLA⁺ Expressions This tutorial page covers the next two chapters in Crafting Interpreters: * Chapter 5: Representing Code * Chapter 6: Parsing Expressions Same as the book, we could build a parser for our entire minimal TLA⁺ language subset before moving on to interpreting it, but that would be boring! Instead we focus on a simple vertical slice of the language: expressions. And not just any expressions, constant expressions - expressions that do not contain variables or … text/html 2025-11-04T17:32:49+00:00 Anonymous (anonymous@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-06-19T14:50:30+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/creating:operators?rev=1750344630&do=diff Functions, Operators, and Parameters We now rejoin Crafting Interpreters for Chapter 10. The chapter is titled Functions, but TLA⁺ actually has two related concepts to handle here: functions, and operators. It's worth taking some time to conceptually delineate them. text/html 2025-11-03T23:16:03+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/creating:safety?rev=1762211763&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-04-27T17:35:48+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/creating:scanning?rev=1745775348&do=diff Scanning TLA⁺ Tokens This page corresponds to chapter 4 of Crafting Interpreters by Robert Nystrom, henceforth referred to as "the book". We will learn how to chunk up TLA⁺ source file string input into a series of tokens suitable for parsing. For each section in the chapter, first read the section in the book and then read the corresponding section tutorial on this page to see how to adapt the concepts to TLA⁺. text/html 2025-11-04T20:16:16+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/creating:start?rev=1762287376&do=diff Create your own TLA⁺ tools Building your own simplified parsing, model-checking, and even proof-checking tools for TLA⁺ is the best way to prepare yourself for serious work on the existing TLA⁺ tools. This process will give you a strong understanding of how & why the tools are written the way they are. Even though your solution will not match their workings line-for-line, you'll learn to recognize the tricky parts and can compare & contrast your own approach with the existing implementation. Yo… text/html 2025-06-18T20:42:06+00:00 Anonymous (anonymous@undisclosed.example.com) https://docs.tlapl.us/creating:statements?rev=1750279326&do=diff Handling TLA⁺ Statements Here we cover Chapter 8: Statements and State of book Crafting Interpreters. We'll implement the ability to associate identifiers with values, then subsequently use those identifiers in expressions. While Lox was designed with a dual REPL/file execution model in mind, TLA⁺ was not - so the behavior of our interpreter will vary quite a bit from the book! We'll have to implement parser & interpreter