From 8d7d591260ab4526767b249998eeb565c43ba72a Mon Sep 17 00:00:00 2001 From: Federico Ponzi Date: Sat, 28 Sep 2024 13:28:50 +0100 Subject: [PATCH] more intro material --- src/learning/intro.md | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/learning/intro.md b/src/learning/intro.md index ce5c189..ce2cc17 100644 --- a/src/learning/intro.md +++ b/src/learning/intro.md @@ -1,8 +1,17 @@ # Learning TLA+ and Model Checking +This page lists some external resources one could use to learn more about TLA+ and related topics. -* [Specyfing systems](https://lamport.azurewebsites.net/tla/book.html): by Leslie Lamport is still the reference book for TLA+ and its tools +First things first: +1. Setup your IDE. Visual Studio code with [tlaplus plugin](../using/vscode.md) is recommended. +2. If you have questions or if you feel stuck at any point, reach out to the [community](../community.md). -* [The Specification Language TLA+](https://members.loria.fr/SMerz/papers/tla+logic2008.pdf): Another good manuscript by Stephan Merz explaining TLA+ specification language: Sect. 2 introduces TLA+ by way of a first specification of the resource allocator and illustrates the use of the tlc model checker. The logic TLA is formally defined in Sect. 3, followed by an overview of TLA+ proof rules for system verification in Sect. 4. Section 5 describes the version of set theory that underlies TLA+, including some of the constructions most frequently used for specifying data. The resource allocator example is taken up again in Sect. 6, where an improved high-level specification is given and a step towards a distributed refinement is made. Finally,Sect. 7 contains some concluding remarks +If you want a good kickstart to TLA+, start with [Leslie Lamport — The Paxos algorithm or how to win a Turing Award. Part 1](https://www.youtube.com/watch?app=desktop&v=tw3gsBms-f8) and [Part 2](https://www.youtube.com/watch?v=8-Bc5Lqgx_c). It is a good introduction on TLA+ and uses Paxos and Consensus as an example. + +Another longer, popular and more complete option is Lamport's video course available on the [website](https://lamport.azurewebsites.net/video/videos.html). + +[Specyfing systems](https://lamport.azurewebsites.net/tla/book.html): by Leslie Lamport is still the reference book for TLA+ and its tools. It's well written and easy to follow. + +* [The Specification Language TLA+](https://members.loria.fr/SMerz/papers/tla+logic2008.pdf): Another good manuscript by Stephan Merz explaining TLA+ specification language: Sect. 2 introduces TLA+ by way of a first specification of the resource allocator and illustrates the use of the tlc model checker. The logic TLA is formally defined in Sect. 3, followed by an overview of TLA+ proof rules for system verification in Sect. 4. Section 5 describes the version of set theory that underlies TLA+, including some of the constructions most frequently used for specifying data. The resource allocator example is taken up again in Sect. 6, where an improved high-level specification is given and a step towards a distributed refinement is made. The fnal Sect. 7 contains some concluding remarks. ## Resources