The TLA+ Video Course

Last modified 23 October 2021
This is a series of video lectures to teach programmers and software engineers how to write their own TLA+ specifications.  It assumes a basic understanding of programming concepts.  Some knowledge of elementary mathematics, such as might be taught in a beginning university math course for computer scientists, would also be helpful. 

A Word of Warning  These videos are not light entertainment.  They require careful viewing and actual thinking.  You may often stop a video to digest what you've just seen, and perhaps to skip back and view it again.  To accompany the videos, coffee will be better than popcorn.

The lectures can be watched on the Web.  However, people with slow network connections might prefer to download lower resolution versions of the videos and watch them off-line.  Instructions on how to do that are given below. 

The script of each video is also provided.  It contains everything shown and said on the video, except for shots of the author.  The hearing impaired and viewers not fluent in English will find it helpful to read the script as they watch the video.  The script can also be read instead of watching the video by those who want to review the lecture and those who hate videos.  However, the html file that displays the video may be needed to download material.

The Lectures

  1. Introduction to TLA+
    Explains what TLA+ is and why you might want to use it.  It introduces the concept of a state machine.   Length: 21:18
    Web version   -   Correction   -   Offline Version: video file, zip file   -   Script
  2. State Machines in TLA+
    Shows how a simple state machine is described in TLA+, giving the first glimpse of a TLA+ specification.   Length: 15:40
    Web version   -   Offline version: video file, zip file   -   Script
  3. Resources and Tools
    Describes resources for learning about TLA+.  Explains how to download the Toolbox and shows how to use it to open a spec, view the pretty-printed version, and run TLC on it.   The script does not display what is being said in some portions of the video that demonstrate the use of the Toolbox.   Length: 11:13
    Web version   -   Correction   -   Offline version: video file, zip file   -   Script
  4. Die Hard
    We save the lives of two Hollywood action heroes.  On the way, you will start learning to write TLA+ specs and checking them with the parser and with TLC.   Length: 19:39
    Web version   -   Correction   -   Offline version: video file, zip file   -   Script
  5. Transaction Commit
    Commitment, in marriage and database transactions, is specified.  You also learn how to use mathematical functions in specifications.   Length: 24:39
    Web version   -   Correction   -   Offline version: video file, zip file   -   Script
  6. Two-Phase Commit
    How commitment is achieved, in marriage and database transactions.  You also learn about records in TLA+ and some more about using TLC.   Length: 21:22
    Web version   -   Correction   -   Offline version: video file, zip file   -   Script
  7. Paxos Commit
    Specifies a real fault-tolerant algorithm for committing database transactions.  It explains a few mathematical operations for constructing and combining sets.   Length: 19:46
    Web version   -   Correction   -   Offline version: video file, zip file   -   Script
  8. Implementation
    A two-part lecture that introduces temporal formulas and explains what it means for one specification to implement another.   Length: Part 1: 15:53, Part 2: 12:13
    Part 1: Preliminaries
       Web version   -   Correction   -   Offline version: video file, zip file   -   Script     
    Part 2: How it Works
       Web version   -   Offline version: video file, zip file   -   Script     
  9. The Alternating Bit Protocol
    A two-part lecture that explains liveness, which describes what must happen, and fairness.
    Part 1: The High Level Specification
       Web version   -   Offline version: video file, zip file   -   Script      Length: 20:51
    Part 2: The Protocol
       Web version   -   Correction   -   Offline version: video file, zip file   -   Script      Length: 18:45
  10. Implementation with Refinement
    A two-part lecture that explains the general meaning of implementation, which involves refinement mappings.
    Part 1: Preliminaries
       Web version   -   Correction   -   Offline version: video file, zip file   -   Script      Length: 19:53
    Part 2: Refinement Mappings
       Web version   -   Offline version: video file, zip file   -   Script      Length: 21:26

Downloading Instructions

 Before watching any lecture off-line, download  tla-video-files.zip  and extract its contents into a folder.  Let's suppose you name the folder  tla-lectures .  That folder should then contain the files  tlastyles.css  and  tlavideo.js  and the folder  dist . 

To watch a lecture off-line, download the lecture's video file and zip file, which will have the same first names, into the folder  tla-lectures .  Let's suppose those files are named  smandtla.mp4  and  smandtla.zip .  Extract the contents of  smandtla.zip  into folder  tla-lectures .  One of the extracted files will be named smandtla.html .  (For most lectures, the zip file will contain only that file.)  To view the video, open a Web browser on this html file.