creating:start

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision		 Previous revision
creating:start [2025/03/29 14:11] – Moved introductory material from scanning tutorial into this page ahelwercreating:start [2025/05/21 19:44] (current) – ToC: changed some titles ahelwer
Line 18: Line 18:
 Developing an intuition of what TLC is doing when it model-checks your spec will enable you to write specifications that make better use of its capabilities. Developing an intuition of what TLC is doing when it model-checks your spec will enable you to write specifications that make better use of its capabilities.
 And, if you reach the edge of those capabilities - well, you're well-placed to extend TLC to handle it! And, if you reach the edge of those capabilities - well, you're well-placed to extend TLC to handle it!
 +
 +===== 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]]
  
 ===== Overview ===== ===== Overview =====
Line 24: Line 36:
 There are two good reasons for this: 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.   - 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 a simple 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. 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 uses the Java 17 [[https://openjdk.org/jeps/395|records]] feature for terse definition of dataclasses, so you must install JDK 17 or higher. 
 +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. The tutorial has you construct the TLA⁺ tools from the bottom up.
Line 44: Line 57:
  
 Here is what our minimal language subset includes: Here is what our minimal language subset includes:
-  * Named operator definitions like ''op == ...'' and ''op(x, y, z) == ...'' +  * Whole natural numbers like ''0'', ''5'', ''10'', etc. 
-  * Single-line comments like ''\* comment text'' +  * Boolean values ''TRUE'' and ''FALSE''
-  * Declaration of ''VARIABLES''+
   * Finite set literals, like ''{1, 2, 3, 4, 5}''   * 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''   * Quantification over sets with ''\E'' and ''\A''
   * Function construction and application, like ''[e \in S |-> op(e)]'' and ''f[e]''   * Function construction and application, like ''[e \in S |-> op(e)]'' and ''f[e]''
-  * The ''ENABLED'' and logical negation (''~'') prefix operators +  * Named operator definitions like ''op == ...'' and ''op(x, y, z) == ...'' 
-  * Some infix operators: ''\in'', ''='', ''+'', ''-'', ''..'', and ''<'' +  * Declaration of ''VARIABLES''
-  * The variable-priming suffix operator+
   * Vertically-aligned conjunction & disjunction lists   * Vertically-aligned conjunction & disjunction lists
-  * The ''IF''/''THEN''/''ELSE'' construct 
-  * Whole natural numbers like ''0'', ''5'', ''10'', etc. 
-  * Boolean values ''TRUE'' and ''FALSE'' 
  
 Notably, we do not use the familiar ''---- MODULE Name ----''/''===='' encapsulation. Notably, we do not use the familiar ''---- MODULE Name ----''/''===='' encapsulation.
Line 97: Line 111:
  
 To begin the tutorial, start at page [[creating:scanning|Scanning TLA⁺ Tokens]]. To begin the tutorial, start at page [[creating:scanning|Scanning TLA⁺ Tokens]].
 +
 +[[creating:start#table_of_contents|Table of Contents]] | [[creating:scanning|Next Page >]]
  
  • creating/start.1743257488.txt.gz
  • Last modified: 2025/03/29 14:11
  • by ahelwer