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/09 14:52] – Added table of contents ahelwercreating:start [2025/05/21 19:44] (current) – ToC: changed some titles ahelwer
Line 21: Line 21:
 ===== 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|Handling Constant TLA⁺ Expressions]] +  - [[creating:expressions|Parsing Constant TLA⁺ Expressions]] 
-  - TODO+  - [[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 34: 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.
Line 105: 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.1744210369.txt.gz
  • Last modified: 2025/04/09 14:52
  • by ahelwer