Corrections to the TLA+ Video Course

Last modified 6 February 2019

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

Lecture 5. Transaction Commit

  13:07   Ignore the spurious © symbol.

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.