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/04/01 14:46] – Expanded and reordered language feature list 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 98: 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.1743518794.txt.gz
  • Last modified: 2025/04/01 14:46
  • by ahelwer