tla_workshop

This is the complete set of materials for my rax.io TLA+ workshop.

The contents of this workshop are generally based on Leslie Lamport's video series. My thought there was that if we don't finish the workshop in the three hours we have, you'll have a fantastically produced video series with which to continue learning.

The complete workshop slides are available in their original Keynote format, zipped into tla_workshop.zip. A PDF version of the slides is available at tla_workshop.pdf. This was generated by turning every slide transition/animation into a separate page in the PDF.

The cheat sheet with common TLA+ idioms and syntax (as covered in the workshop) is in tla_cheatsheet.pdf. Please note that this cheat sheet does not cover all of TLA+, just the material in this workshop. Leslie Lamport's "official" cheat sheet can be found at http://lamport.azurewebsites.net/tla/summary.pdf.

The TLA+ spec files used in the workshop can be found in the specs/ directory. These are all from Lamport's video series, with either minor or no modifications.