Differences

This shows you the differences between two versions of the page.

--- learning:start [2025/08/20 09:38] – fponzi
+++ learning:start [2025/08/20 09:47] (current) – fponzi
@@ Line 20: / Line 20: @@
 ----
-  * [[https://members.loria.fr/SMerz/papers/tla+logic2008.pdf|The Specification Language TLA+]]: 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.
+[[https://members.loria.fr/SMerz/papers/tla+logic2008.pdf|The Specification Language TLA+]]: 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 final Sect. 7 contains some concluding remarks.
+===== Learn by Doing ====
+Markus Kuppe does TLA+ trainings using the two following repositories:
+  * https://github.com/lemmy/BlockingQueue
+  * https://github.com/tlaplus-workshops/ewd998/  Distributed termination detection on a ring.
+The way to use them is to basically check the git history from the beginning and follow along.
 ===== Resources =====