Differences

This shows you the differences between two versions of the page.

--- creating:start [2025/03/24 19:28] – Wrote Getting Started blurb and linked to syntax parsing page ahelwer
+++ creating:start [2025/08/29 17:21] (current) – Added note about TLA+ Foundation support ahelwer
@@ Line 19: / Line 19: @@
 And, if you reach the edge of those capabilities - well, you're well-placed to extend TLC to handle it!
-===== Getting Started =====
+This guide was written with the generous support of the [[https://foundation.tlapl.us/|TLA⁺ Foundation]].
+===== Table of Contents =====
+  - [[creating:start|Introduction (this page)]]
+  - [[creating:scanning|Scanning TLA⁺ Tokens]]
+  - [[creating:expressions|Parsing Constant TLA⁺ Expressions]]
+  - [[creating:evaluation|Evaluating Constant TLA⁺ Expressions]]
+  - [[creating:statements|Handling TLA⁺ Statements]]
+  - [[creating:jlists|Conjunction & Disjunction Lists]]
+  - [[creating:operators|Functions, Operators, and Parameters]]
+  - [[creating:actions|Variables, States, and Actions]]
+  - [[creating:safety|Model-Checking Safety Properties]]
+  - [[creating:closures|Parameters as Closures]]
+===== Overview =====
 This tutorial uses Java.
 There are two good reasons for this:
   - At time of writing, [[codebase:start|the most mature TLA⁺ tools]] are written in Java, and this tutorial prepares you to work on them.
-  - The high-quality free online textbook [[https://craftinginterpreters.com/contents.html|Crafting Interpreters]] by Robert Nystrom uses Java, and this tutorial is a simple TLA⁺-themed wrapper around its concepts. That book states its own reasons for using Java, which you can read.
+  - The high-quality free online textbook //[[https://craftinginterpreters.com/contents.html|Crafting Interpreters]]// by Robert Nystrom uses Java, and this tutorial is largely a TLA⁺-themed wrapper around its concepts. That book states its own reasons for using Java, which you can read.
 You will need to install the [[https://adoptium.net/|Java Development Kit]] appropriate for your system.
-While all code artifacts can be produced entirely by reading this tutorial, if you get out of sync you can find working implementations in [[https://github.com/tlaplus-community/tlaplus-creator|this git repository]].
+This tutorial requires Java 21 or higher, for the Java 17 [[https://openjdk.org/jeps/395|records]] feature and the Java 21 ''[[https://docs.oracle.com/en/java/javase/21/docs/api/java.base/java/util/SequencedCollection.html#reversed()|reversed()]]'' method.
+While all code artifacts can be produced entirely by reading this tutorial, if you get out of sync you can find working implementations in [[https://github.com/tlaplus/devkit|this git repository]].
 The tutorial has you construct the TLA⁺ tools from the bottom up.
@@ Line 34: / Line 50: @@
 A minimal subset of the TLA⁺ language is used; users are encouraged to extend their tools to handle additional TLA⁺ syntax as desired.
-To begin the tutorial, start at page [[creating:syntax|Parsing TLA⁺ Syntax]].
+===== The Language =====
+TLA⁺ is a large, complicated, and ambiguous language that takes a huge amount of work to parse correctly & completely.
+This is assisted by [[https://github.com/tlaplus/rfcs/tree/2a772d9dd11acec5d7dedf30abfab91a49de48b8/language_standard/tests/tlaplus_syntax|a comprehensive test corpus]] exercising the language's nooks & crannies, but here we will make life easy on ourselves.
+This tutorial only uses a minimal subset of TLA⁺ syntax, enough to handle [[https://github.com/tlaplus/Examples/blob/37236893f14527b4fc9f3963891eb2316c3de62e/specifications/DieHard/DieHarder.tla|the generalized DieHard spec]] with some inconvenience.
+While that may seem limiting, this tutorial tries to focus on the difficult & interesting parts of bringing TLA⁺ to life instead of more mundane drudgework like handling all hundred-some user-definable operator symbols.
+You are encouraged to extend this minimal core as you wish; language tooling is best developed incrementally!
+Slowly filling in the details of this rough language sketch has a satisfying meditative aspect.
+Here is what our minimal language subset includes:
+  * Whole natural numbers like ''0'', ''5'', ''10'', etc.
+  * Boolean values ''TRUE'' and ''FALSE''
+  * Finite set literals, like ''{1, 2, 3, 4, 5}''
+  * Parentheses for expression grouping
+  * ''IF''/''THEN''/''ELSE'' expressions
+  * Single-line comments like ''\* comment text''
+  * The ''ENABLED'', negative (''-''), and logical negation (''~'') prefix operators
+  * Some infix operators: ''\in'', ''='', ''+'', ''-'', ''..'', ''/\'', ''\/'', and ''<''
+  * The variable-priming suffix operator
+  * Quantification over sets with ''\E'' and ''\A''
+  * Function construction and application, like ''[e \in S |-> op(e)]'' and ''f[e]''
+  * Named operator definitions like ''op == ...'' and ''op(x, y, z) == ...''
+  * Declaration of ''VARIABLES''
+  * Vertically-aligned conjunction & disjunction lists
+Notably, we do not use the familiar ''---- MODULE Name ----''/''===='' encapsulation.
+Files simply consist of a series of unit-level TLA⁺ definitions.
+We also do not leave room for a separate model configuration file; all ''CONSTANT'' values must instead be hardcoded, and well-known names like ''Init'', ''Next'', ''TypeOK'', and ''Inv'' identify important definitions.
+As outlined above, you are free to add missing features (or even your own invented features!) as you wish.
+Each chapter ends with a set of challenges that often involve adding these missing features.
+===== Getting Started =====
+Read part I (the first three chapters) of free online textbook //[[https://craftinginterpreters.com/contents.html|Crafting Interpreters]]// by Robert Nystrom.
+We will be closely following the material in this book, modifying it to our uses.
+The first two chapters are a nice introduction and overview of language implementation generally.
+Chapter three specifies a toy language called Lox, to be used as an object of study for the remainder of the book.
+Our minimal TLA⁺ subset has some similarity to Lox with regard to expressions involving integers and booleans, but also differences - you can skip the section on closures (unless you want to implement higher-order operator parameters yourself) and the section on classes.
+What's important is that it's similar enough for all the fundamentals to still apply!
+Code snippets are shown often in this tutorial.
+When a snippet is similar to code given in the book with the exception of a few lines, the differing lines will be highlighted.
+For example:
+<code java [highlight_lines_extra="2"]>
+  private char advance() {
+    column++;
+    return source.charAt(current++);
+  }
+</code>
+Highlighting is also used to identify //new// code being added to a large section of code given previously, with line numbers and surrounding lines included for context.
+For example:
+<code java [enable_line_numbers="true",highlight_lines_extra="2",start_line_numbers_at=82]>
+      case '\n':
+        column = 0;
+        line++;
+        break;
+</code>
+Sometimes the code given here is so different from that provided by the book that highlighting is simply ommitted to reduce visual noise.
+A parenthetical will specify the meaning of highlighted code when ambiguous.
+To begin the tutorial, start at page [[creating:scanning|Scanning TLA⁺ Tokens]].
+[[creating:start#table_of_contents|Table of Contents]] | [[creating:scanning|Next Page >]]