| Both sides previous revision Previous revision Next revision | Previous revision |
| learning:start [2025/05/04 21:01] – typo jesse_emptysquare.net | learning:start [2025/08/20 09:47] (current) – fponzi |
|---|
| After that, you can start digging into Lamport’s video course available on the [[https://lamport.azurewebsites.net/video/videos.html|website]]. If you prefer a written medium, [[https://lamport.azurewebsites.net/tla/book.html|Specifying systems]]: by Leslie Lamport is still the reference book for TLA+ and its tools. It’s well written and easy to follow. | After that, you can start digging into Lamport’s video course available on the [[https://lamport.azurewebsites.net/video/videos.html|website]]. If you prefer a written medium, [[https://lamport.azurewebsites.net/tla/book.html|Specifying systems]]: by Leslie Lamport is still the reference book for TLA+ and its tools. It’s well written and easy to follow. |
| |
| After learning some TLA+, it might be helpful to start learning some Pluscal. Checkout the [[./pluscal.md|pluscal]] page for more info and some resources. | After learning some TLA+, it might be helpful to start learning some Pluscal. Checkout the [[learning:pluscal|pluscal]] page for more info and some resources. |
| |
| Don’t just learn the theory, start by solving some small [[learning:exercises|exercises]]. | Don’t just learn the theory, start by solving some small [[learning:exercises|exercises]]. |
| ---- | ---- |
| |
| * [[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 ===== | ===== Resources ===== |
jesse_emptysquare.net