The TLA+ Video Course

Last modified 16 August 2017
This is a work in progress that consists of the beginning of 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 videos 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.  It can be useful for the hearing impaired, viewers who want to review a lecture, and people 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   -   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.   Length: 11:13
    Web version   -   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   -   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   -   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   -   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   -   Offline version: video file, zip file   -   Script

Downloading Instructions

Before watching any lecture off-line, download  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 .  Extract the contents of  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.