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/17 15:39] – Added links to new pages in table of contents ahelwercreating:start [2025/11/04 20:16] (current) – Added instanceof pattern-matching to Java version requirement justification 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!
 +
 +This guide was written with the generous support of the [[https://foundation.tlapl.us/|TLA⁺ Foundation]].
  
 ===== Table of Contents ===== ===== Table of Contents =====
  
-  - [[https://docs.tlapl.us/creating:start|Introduction (this page)]] +  - [[creating:start|Introduction (this page)]] 
-  - [[https://docs.tlapl.us/creating:scanning|Scanning TLA⁺ Tokens]] +  - [[creating:scanning|Scanning TLA⁺ Tokens]] 
-  - [[https://docs.tlapl.us/creating:expressions|Parsing Constant TLA⁺ Expressions]] +  - [[creating:expressions|Parsing Constant TLA⁺ Expressions]] 
-  - [[https://docs.tlapl.us/creating:evaluation|Evaluating Constant TLA⁺ Expressions]] +  - [[creating:evaluation|Evaluating Constant TLA⁺ Expressions]] 
-  - [[https://docs.tlapl.us/creating:statements|Handling TLA⁺ Statements]] +  - [[creating:statements|Handling TLA⁺ Statements]] 
-  - TODO+  - [[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 ===== ===== Overview =====
Line 33: Line 39:
 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 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. 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, ''[[https://docs.oracle.com/en/java/javase/17/language/pattern-matching-instanceof.html|instanceof]]'' pattern-matching, 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. The tutorial has you construct the TLA⁺ tools from the bottom up.
Line 107: Line 114:
  
 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.1744904369.txt.gz
  • Last modified: 2025/04/17 15:39
  • by ahelwer