The TLA+ Video Course

Last modified 14 May 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. 

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

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
  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
  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
  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

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.