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/06/19 21:40] – ToC: added chapter on closures 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 =====
Line 29: Line 31:
   - [[creating:operators|Functions, Operators, and Parameters]]   - [[creating:operators|Functions, Operators, and Parameters]]
   - [[creating:actions|Variables, States, and Actions]]   - [[creating:actions|Variables, States, and Actions]]
-  - [[creating:closures|Closures]] 
   - [[creating:safety|Model-Checking Safety Properties]]   - [[creating:safety|Model-Checking Safety Properties]]
 +  - [[creating:closures|Parameters as Closures]]
  
 ===== Overview ===== ===== Overview =====
Line 37: 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.
-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.+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]]. 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]].
  
  • creating/start.1750369229.txt.gz
  • Last modified: 2025/06/19 21:40
  • by ahelwer