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/05/21 19:44] (current) – ToC: changed some titles ahelwer
Line 27: Line 27:
   - [[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]]
  
 ===== Overview ===== ===== Overview =====
Line 37: Line 39:
  
 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.
  • creating/start.1745091640.txt.gz
  • Last modified: 2025/04/19 19:40
  • by ahelwer