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
- 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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, downloadtla-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.