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/19 19:40] – Use internal wiki links 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 27: Line 29:
   - [[creating:statements|Handling TLA⁺ Statements]]   - [[creating:statements|Handling TLA⁺ Statements]]
   - [[creating:jlists|Conjunction & Disjunction Lists]]   - [[creating:jlists|Conjunction & Disjunction Lists]]
-  - TODO+  - [[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 34: 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.
  • creating/start.1745091640.txt.gz
  • Last modified: 2025/04/19 19:40
  • by ahelwer