Corrections to the TLA+ Video Course

Last modified 24 October 2022

This page lists corrections for all known problems with the content of The TLA+ Video Course.  Problems in the videos include errors, misleading or hard to understand parts, and obsolete information.  They are identified by minutes:seconds into the video where the problem begins.  Not addressed are problems with video quality, trouble downloading the videos, or bad acting.

Lecture 1. Introduction to TLA+

  13:16   The word possible should be followed by behaviors.

Lecture 3. Two-Phase Commit

  10:34   The TLA+ web site has been completely changed since the video was made.  The URL of the home page is the same, but resources for learning about TLA+ are found by clicking on Learning TLA+, which takes you to this page.  The Summary of TLA+ is reached from a link in the text describing by the The TLA+ Book that takes you here.  The link to The TLA+ Google Group is now on the Learning page; it takes you here.
  11:56   You do not have to install Java.  Installing the Toolbox now automatically installs Java.
  12:34   The section to check if something goes wrong is now called If You Find a Problem.

Lecture 4. Two-Phase Commit

  15:22   In the definition of BigToSmall, the formula  big' = small - (3 - big)  should be changed to  big' = big - (3 - small) .

Lecture 5. Transaction Commit

  13:07   Ignore the spurious © symbol.
  18:21   The Toolbox's pages that specify a model have changed since the video was made.  If it's no longer easy to find something on those pages from the instructions in the video, a correction will lead you to it.
  20:28   The Coverage section of the Model Checking Results page has been replaced by a section that is more helpful for beginning users.  A new profiling feature provides much more information than the Coverage section did.  Profiling is described in the Features section of the TLC Options Page help page.

Lecture 6. Two-Phase Commit

  14:20   Instead of just creating a new module named TwoPhase, you should create a new spec by that name, which will create that module.
  15:50   Instead of TPnit, the initial predicate should be TPInit.

Lecture 7. Paxos Commit

  13:42   The word smallest in both the written and the spoken text should be largest.

Lecture 8. Implementation

Part 1: Preliminaries

  13:58   The term module-complete is used here and occasionally through 5:08 to mean module-closed.
  17:11   state expression should be action expression in A state expression has a value on a step.

Lecture 9. The Alternating Bit Protocol

Part 2: The Protocol

  17:28   The Advanced Options page has been eliminated.  The State Constraint is now specified on the Spec Options page, which is reached by clicking Additional Spec Options on the model's Model Overview page.

Lecture 10. Implementation with Refinement

Part 1: Preliminaries

  14:48   The formula  (AtoB2 < 4) (BtoA2 < 4)  should be
(Len(AtoB2) < 4) (Len(BtoA2) < 4) .