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.
|
13:16
|
The word possible should be followed by behaviors .
|
|
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.
|
|
15:22
|
In the definition of BigToSmall, the formula
big' = small - (3 - big) should be changed to
big' = big - (3 - small) .
|
|
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.
|
|
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.
|
|
13:42
|
The word smallest in both the written and the spoken
text should be largest .
|
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 .
|
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.
|
Part 1: Preliminaries
|
14:48
|
The formula (AtoB2 < 4)
∧ (BtoA2 < 4) should be
(Len(AtoB2) < 4) ∧ (Len(BtoA2) < 4) .
|