
Practical TLA+ by Hillel Wayne
Leslie Lamport
Last modified on 23 November 2018


You'll miss a lot on this web site unless you enable Javascript
in your browser.
The Book
[show]
Practial TLA+ is a book by Hillel Wayne,
available
from the publisher.
It provides a good complete course on the PlusCal algorithm
language.
This web page describes a number of minor problems in the book,
including hard to understand statements and small errors.
It also explains why I disagree with a few things the book says.
I want to emphasize that the issues listed here
are small problems in an excellent book.
General Remarks
[show]
The P Syntax
PlusCal has two syntaxes: the P syntax inspired by Niklaus Wirth's Pascal
programming language, and the C syntax inspired by the programming language
C.
The book uses the P syntax.
That's the syntax I would prefer if I wrote algorithms only
for my own use and never wrote programs.
Most engineers and programmers will prefer the C syntax, which will look
more familiar to them, so I've used it for all my published algorithms.
You should compare the PlusCal manual's PVersion
and CVersion to see which you prefer.
It should be easy to become bisyntactic, translating the book's
P syntax to C syntax.
Copying the Code
The source files for the specs in the book are available on line.
However, those are the final versions. If you want to follow the
development of the spec in your Toolbox, you'll have to copy the
pieces of the spec from the book. Unfortunately, that removes all
indenting, which makes the result unreadable.
You can try to find the bits of code being added at each step
in the complete spec and copy them from there. It would be nice if
all the code snippets in the book were available in an ascii file,
identified by page and line numbers.
Possible Typos in the Code
I noticed one typo in the code in the book (on page 161, Chapter 10).
It probably occurred in copying text from the PlusCal source file to
the book's source file. I didn't read the code carefully, and
there could be more such errors. If some code in the
book doesn't look right, you should try it yourself to see if the
problem is in your understanding or is a typo in the book.
The Title
[show]
This book is about
PlusCal, not about TLA+.
It describes all the TLA+ operators for writing ordinary mathematical
expressions and says a little about expressing liveness properties
with TLA+'s temporal operators. However, it doesn't mention some
of the most important features of TLA+, including the ability to state
and check that one specification implements a higherlevel
specification. After reading this book, you should find it easy
to learn TLA+. I recommend that you do so. While reading
the book, you might want to look at the TLA+ translation of the
PlusCal specs.
Introduction
[show]
 Page xix

Without having something to program with, there's really no reason to
use TLA+.
Wrong!
Here are potential users of TLA+ who don't do any programming.
 People who need to express precisely what a system or program
should do, including customers hiring someone else to build the
system or software engineers describing a system for others to
build.
 Computer scientists who design algorithms, but don't write programs
to implement them. I believe I have written only one concurrent
program in my life, which was used by me and a few other people
for a couple of years in the mid1980s.
Chapter 1
[show]
 Page 7, line 16

which is closer to what we normally think of programming functions
This should be something like:
which is closer to what we normally think of in programming as
functions .
 Page 14

The text should mention that a state is an assignment of values to variables,
and there is a nondeclared variable pc added by the PlusCal to TLA+
translation.
 Page 18, line 5

Every following state highlights with variables that have changed
from the previous state.
Better would be:
Every following state highlights with red the variables that have
changed from the previous state.
 Page 22, line 1

Unfortunately, there are no good options.
This is not accurate. In particular, the objection of bullet two is
misleading. First of all, it is impossible to write in TLA+ that the
process can't stutter between the withdrawal and deposit.
(You can understand the book without knowing this,
but if you're curious you can look
here
to find out why not.)
The correct statement is that,
by adding the keyword
fair
in front of
process
in the code, we can specify that the process doesn't stop until it's
gotten to the end.
The fact that there's no way to implement it is
irrelevant. It's impossible to implement the safety part of the
spec because a cosmic ray could hit the computer and cause it to do
something not allowed by the spec. Verifying a property shows
that if a behavior satisfies the spec, then it satisfies the
property. This may or may not be useful. Many specs people
write are not implementablefor example, they may contain unbounded
queues, or variables whose value can be an arbitrary integer. It
requires engineering judgment to know whether or not the inability to
implement those things makes it useless to know that the spec
satisfies some property. It's useful to know that the spec with
the fairness assumption satisfies
EventuallyConsistent .
That's because there would be something seriously wrong with the spec
if fairness didn't imply
EventuallyConsistent .
This is not the right place to discuss fairness and
liveness, and that discussion is deferred to Chapter 6 of the book.
However, it would be useful point to that discussion. I think
something like the following belongs here:
For now, the PlusCal specs we write allow processes to stop
at any time. They therefore describe what a system is allowed
to do, but not what it must do. Chapter 6 explains how we
write specs that specify what must happen.
Chapter 2
[show]
 Page 24, line 3

This is for backwards compatibility reasons.
I don't know with what this is supposed to be backwards compatible.
 Page 24, line 9

It would be a good idea for item (4) to mention that comments can be
nested to arbitrary depth, since, for some unfathomable reason, that's
not true of most programming languages.
 Page 24, lines 5 to 1

This paragraph should refer to the tip on the following page,
which explains how to evaluate expressions
without running the entire spec.
 Page 26, lines 10 to 1

In the = VS := section,
I don't like the explanation of
=
in the variable declaration as an
initial assignment.
It would be better
to say that a variable's declaration includes its initial value (as an
optional part).
Also, this would be a good point to introduce the distinction between
legal PlusCal specs and ones that TLC can handle. For example,
this is perfectly legal PlusCal:
variables z = (x=y), x = 2, y = 2;
The TLAPlus proof system treats it exactly the same as
variables x = 2, y = 2, z = (x=y);
It's just TLC that can't handle the first.
 Page 27, line 3

In introducing the
..
operator, it should be mentioned
that
3..1
equals
{} (the empty set).
 Page 27, line 10

All elements in the set must have the same type
This is inaccurate. First,
{"a", 1}
is a legal PlusCal expression; it's TLC that can't deal with it.
Second, being of the same type is a sufficient but not necessary
condition for TLC to be able to deal with an expression. For example,
it has no trouble with
{{1}, {"a", "b"}}
It's usually the case that TLC cannot handle sets containing
elements of different types. However, there's one important
exception: sets of structures. (Structures are introduced on
page 29.) TLC can handle sets of structures whose elements
don't all have the same set of keys.
 Page 29, Note

Mathematically, a structure is a function whose
domain is a set of strings, and a sequence is a function whose domain
is a set of integers. I doubt if many people would say that these
kinds of functions have the same type. It would be better to say that
structures and sequences are both instances of a more general class of
values called functions.
 Page 31, line 11

For example, the following is a spec error:
This does not mean that the following is incorrect
PlusCal code. It means that an execution of the
spec evaluates the assert statement with
x
equal to
FALSE , generating an
assertion failure.
Formally, a spec is a definition, and a definition can be incorrect
only if it is syntactically illegal. Informally, a definition is
called incorrect if it doesn't define what we think it should.
 Page 32ff

In the example, the variable curr can be eliminated by updating
items
at the end of the while loop and replacing occurrences of
curr
by
Head(items) .
Chapter 3
[show]
 Page 44, line 3

The TLA+ does not use semicolons; only the PlusCal computations
need semicolons.
This should be:
TLA+ does not use semicolons; only the PlusCal code
that gets translated to TLA+ uses semicolons.
 Page 45, line 15

>> Apply(Add, 1, 2)
You can also write this as
Apply(+, 1, 2) ;
there's no need to define
Add or use a
LAMBDA expression.
 Page 46, line 7

Not all models you write will check all invariants.
You have to specify what you actually care about.
I believe this means that an invariant is just a formula,
and a spec can define lots of formulas.
TLC has no way of knowing by itself which of those formulas are
supposed to be invariants; you have to tell it in the model.
 Page 47, line 2

However, creating dedicated operators is cleaner and better signals
your intent to anybody else who reads your spec.
Defining an operator signals to the reader that the operator is
supposed to be an invariant only if you write in a comment that it's
supposed to be one.
 Page 48 and elsewhere

I believe that the quantifiers
\A and
\E are the first TLA+ operators described
so far that declare bound identifiers—for example, the formula
\A num \in set: num < max
declares the bound identifier num
in the scope of the subformula
num < max .
It should be mentioned that in TLA+, it is illegal to
give a meaning to an identifier that already has a meaning.
Thus, the formula above would be illegal if num
had already been defined.
This means that the formula
\A x \in S : (... /\ \E x \in T : ...)
is illegal because the inner
\E assigns a meaning to
x in a context
(the outer \A x )
in which x already has a meaning. Note that
P == \E x \in T : ...
Q == \A x \in S : (... /\ P)
is legal because the use of
x inside the
definition of
P doesn't
leak out of that definition. The rule that
you can't assign a meaning to an identifier that already has a meaning also
makes this illegal
VARIABLE x
...
P(x) == ...
This is also illegal:
\E x \in S : 2*x \in {x \in Nat : ... }
It should be mentioned that the scope of
\A and \E
extends
as far as possible . For example, this is illegal
\A x \in S : x > 1
=>
\E x \in T : x < 23
because it's parsed as
\A x in S : (x > 1 => \E x \in T : x < 23)
The following is legal
(\A x \in S : x > 1) => \E x \in T : x < 23
as is
/\ \A x \in S : x > 1
/\ \E x \in T : x < 23
Extending as far as possible applies to other TLA+ constructs signaled
by a prefix.
 Page 49, line 11

\A <<x, y>> \in S \X S:
Op(x, y) = Op(y, x)
Please don't use quantifiers over tuples like this. I think it was a
mistake to allow them in TLA+ because it adds a bit of complexity
for something that's seldom useful. That construct
isn't supported by the TLA+ prover, and probably won't be supported by
new tools. Some day, I expect it no longer to be accepted by the
parser.
 Page 49, line 17

People are often confused because
P => Q
is not really equivalent
to the informal use of the phrase if P then Q .
The informal phrase means that
P
being true causes
Q
to be true, while
P => Q
does not imply causality.
 Page 51, line 15

make sure your statements are mutually exclusive
If you make all the cases mutually exclusive, there's little
difference between a CASE and a sequence of nested IF/THEN/ELSEs. One
reason for having a CASE statement is to emphasize symmetry that is
hidden by an IF/THEN/ELSE. For example, compare
AbsoluteValue(x) == CASE x >= 0 > x [] x =< 0 > x
with the equivalent IF/THEN/ELSE.
 Page 53, line 7

This has five states, three of which are distinct.
This presumably means that TLC reports finding five states, three
of which are distinct.
 Page 53, line 7

On execution, TLC will set one of the flags to true while
leaving the other false.
I don't know what this means and I advise not trying to
figure it out. You shouldn't think of TLC setting variables to
values. TLC conceptually computes all possible executions of the
spec, where an execution is a sequence of states and a state is
defined by the values of all the spec's variables. In the course of
computing all executions, TLC computes all reachable states.
 Page 53, line 4

You can make a function as an operator. If the operator doesn't
take any arguments, ...
This means that, since a function is an ordinary value, you can
define an operator to equal a function. If the operator takes no
arguments, you can use the special syntax
Op[x \in S] == ...
for the definition. As is suggested by the example on the next
page, this special syntax can be used for recursive definitions.
If the ordinary syntax is used, a recursive function definition must
be preceded by a RECURSIVE statement.
 Pages 55 and 56

It should be mentioned that TLC uses the operators
@@ and :>
to represent functions that aren't sequences or records.
 Page 57, line 9

The example has an unnecessary bit of complexity. The knapsack
problem is stated as fitting any number of each item into the
knapsack. Since two different items can have the same size and value,
the knapsack problem remains the same if each item appears in the
knapsack at most once. A knapsack then just becomes a set of items,
not a function from items to natural numbers.
Chapter 4
[show]
 Page 68, line 4

In general it is safe.
In general here means usually .
The most common case in which it's not safe to use a symmetry set
is when your spec uses the CHOOSE
operator. Read the Toolbox's help page titled
Model Values and Symmetry to find out precisely
when you can use a symmetry set.
 Page 68, line 9

In 99% of the cases you work with, you want finite sets.
Here, work with probably means define to be CONSTANTS .
It's not that uncommon to use infinite sets like
Nat
in a spec.
 Page 68, line 5

We could also EXTEND Naturals to get the set Nat
Nat
is also defined in the
Integers module;
but
Int
is not defined in the
Naturals
module. Very rarely will there be any reason to
EXTEND
Naturals
instead of
Integers .
 Page 73, line 5ff

As the example shows, strings in TLA+ are defined to be sequences of
characters, though the only way to refer to the character
a
is with
an expression like
"abc"[1] .
However, TLC cannot evaluate that expression.
The only operations on sequences that TLC can evaluate on strings are
\o , Tail ,
and Len .
 Page 75, line 4

The section on
EXTENDS should say that
the EXTENDS statement must be
the first statement in the module. (It can be preceded only by
comments.)
 Page 75, line 5

The module may not have any constants.
That's not true.
Declared CONSTANTS can be
imported by
EXTENDS
just like defined operators.
Chapter 5
[show]
 Page 80, line 1

It should be noted that the variable
pc is
not created if each process has the form
process ...
begin label: while TRUE do ... end while ;
end process
and there are no other labels and no
goto
statement in the code. This
kind of spec is often written for distributed algorithms.
Chapter 6
[show]
 Page 99, line 4

Most temporal properties, though, are what's called liveness checks.
In my experience, the temporal properties engineers check most often
are invariance properties. Perhaps they are not considered here
to be temporal properties because they are usually not written as
temporal formulas when entered in a TLC model to be checked.
 Page 101, line 16

For label
A:
in an unfair process, writing
A:+
will make it weakly fair.
This is incorrect. To make some actions weakly fair, you have to
write
fair process
and write
label:
for each action
label
that you don't want to be weakly fair. Writing
label:+
in a
fair process
makes action
label
strongly fair. Modifying labels with
+
and

in this way allows you to declare some actions unfair,
some weakly fair, and some strongly fair.
 Page 101, line 9

You can also make the spec globally fair by writing
fair algorithm
instead of
algorithm
Note that this is not always equivalent to making each process fair.
 Page 101, line 2

TLC uses a much faster algorithm to evaluate invariants.
It should be noted that TLC uses this faster algorithm no matter which
way you declare the invariant.
 Page 102, line 16

The current version of TLC cannot check set membership of a variable
set as part of a property with
<> .
So you can't write...
This is false. (I don't remember TLC ever having this limitation.)
 Page 102, line 7

P ~> Q
means that if there is some state where
P
is true, then either
Q
is true either now or in some future state.
This can be more clearly stated as:
P ~> Q
means that for any state in which
P
is true,
Q
must be true in that state or in some later state.
It should also be noted that
P ~> Q
is defined to equal
[](P => <>Q) .
 Page 103, line 14

For a finite spec, these mean the same thing...
Here, finite spec and infinite spec mean
terminating spec and nonterminating spec , respectively.
 Page 103, line 2

As with
<> ,
TLC cannot check set membership of a variable set
as part of a property with
<>[] ,
or
[]<> .
As with <> ,
this statement is false.
 Page 104, line 10

TLC uses a different algorithm for this, which is slower and
is not parallelizable.
This is true now, but we hope to enhance TLC to use a parallel
liveness checking algorithm. However, checking liveness will always
be slower than checking safety.
 Page 105, libe 8

Since this is best represented by a check on pc, we need to
place this after the PlusCal translation.
It could instead go in the algorithm's
define section.
 Page 107, line 1

TLC can handle this property because the set, Threads ,
is a constant.
Formula
Liveness
is the first one presented in the book that
quantifies a temporal formulathat is, the first formula of the form
\A v \in S : F
or
\E v \in S : F
where
F is a temporal formula
(one containing
[] , <> ,
or ~> ).
In such a formula,
S
must be a constant set.
Chapter 7
[show]
 Page 113, line 9

By algorithm , we're assuming that algorithms are code intended to
terminate and produce an output, rather than run forever or
continuously interact with its environment.
This is an idiosynchratic, inconsistent use of the term
algorithm . For example, see Dekker's Algorithm
on page 104.
 Page 114, line 13

TLC will create the constant
DefaultInitValue
The constant is created by the PlusCal to TLA+ translation.
The assignment of a model value
to the constant occurs when the Toolbox initializes the model.
If you create the model before translating the algorithm, you will have
to assign a value to that constant when it appears in the TLA+
translation.
 Page 117, line 14ff

The
Leftpad algorithm defined in
the book takes
k
steps to add
k
characters. There is a more interesting algorithm that takes
log k
steps. The idea is to use a helper variable
v
that initially equals
c .
At each step, output is either left unchanged or set to
v \o output , and
v
is set to v \o v .
This is a challenging problem that most
programmers will be able to solve only through a rather long process
of trial and error. A really good programmer will be able to get
it right much quicker—on her first try if she's really, really
good. What she would do is define a formula
I(output, v, in_c, in_n, in_str)
that should be true whenever control is at the beginning of the
while
loop. She would then put the statement
assert I(output, v, in_c, in_n, in_str)
at the beginning of the loop body and debug
the definition of I
as she's debugging the algorithm. Doing this requires a
lot of thinking before you write any code. Thinking before coding is
a good thing to do. On a difficult problem, it will save you time and
produce better code.
 Page 121, line 11

It may be instructive to define
Pow2(n) recursively, but it's easier to write
Pow2(n) == 2^n
using the integer exponentiation operator
^
defined in the Naturals and
Integers modules.
 Page 123

As an exercise, try writing the
binary_search algorithm yourself,
without looking at the book. I'll bet it doesn't work right
on your first
try. If it fails on your first test, instead of continuing
by trial and error, use the same approach I recommended for the more
efficient
Leftpad
algorithm than the one on page 117. Put an
assert
statement at the beginning of the while loop's body asserting
that either
target = seq[i] for some
i in
low..high , or else
target is not in
seq .
Then design your code so that this assertion is not violated.
Chapter 8
[show]
 Page 127, line 4

That means we should write data structures as separate modules
that are extended or instantiated in our spec.
This is standard, good advice. It's what you should do if you were
writing a program rather than a spec. It's also what you should do if
you or others want the identical data structure spec—for example, if
it models a data structure that is already implemented in code.
However, specs are simpler and much smaller than programs. Engineers
generally prefer to keep the spec of a data structure in the same
module as the spec of the algorithm that uses it. Copying and pasting
a few lines of data structure spec is no big deal. Moreover, it
encourages them to modify the data structure so it's exactly what
they want for their new spec.
 Page 128, line 9

This means using TLC to get
Assert .
This seems to mean importing the TLC module to import the definition
of Assert .
 Page 132, line 14

It is probably a mistake to make the definition of
isLinkedList
local, since for an algorithm that is supposed to create linked
lists, one wants to check that it actually does create one. This
can be done by evaluating
isLinkedList ,
without having to evaluate the complete set of all linked lists.
There is one issue that should be discussed in Chapter 8 but isn't.
It's good to define data structures as simply as possible, to make
sure that the definition is correct. However, for using the data
structure in other specs, efficiency of TLC's evaluation of the operators
can be important. For example,
isLinkedList is defined on page 132 to equal
isLinkedList(PointerMap) ==
LET ... IN \E ordering \in all_seqs : ...
If the cardinality of nodes is
n ,
then all_seqs contains n^n elements,
which makes evaluation of
isLInkedList(PointerMap)
inefficient unless
n
is very small.
It's easy to recursively define an operator
startsLL(node,PointerMap) to be true iff
PointerMap is a linked list
starting at
node ,
where
StartsLL
can be evaluated in time polynomial in
n .
A more efficient definition of
isLinkedList is then
IsLinkedList(PointerMap) ==
LET nodes == ... IN \E node \in nodes : startsLL(node, PointerMap)
You can test that the two definitions of
isLinkedList are the same on
a set of nodes small enough so it can be handled by the inefficient
definition. Having two separate definitions helps assure that both
definitions are correct. Often the more efficient definition of
an operator is a more operational recursive one.
Chapter 9
[show]
 Page 137, line 9

A state machine is a system with a finite set of internal states
along with a set of transitions between the states.
That's a finite state machine. Not all the state machines
specified in this chapter are finite. For example, in the spec
on page 141, nothing says that the sets Data
and Clients are finite.
The whole idea of PlusCal and TLA+ is to model a system as a state
machine—usually not a finitestate one. TLC is generally run on
a finitestate model of the state machine.
 Page 146, line 5

Ghost variables are more accurately called history variables because
they record information about past states. Somewhat surprisingly,
some refinements require a different kind of variable, which doesn't
have to be implemented, called a prophecy variable—a variable
that predicts what
will happen in the future. Such a variable might be needed if a
decision is made in the spec before it needs to be, and that decision
happens later in the refinement.
Chapter 10
[show]
The example of this chapter nicely illustrates that reasonable
liveness properties often can't be satisfied. But you should remember
that liveness itself is just an approximation of the property we
really want. It's of no use to know that a program will
eventually produce an answer if it might take billions of years.
Liveness properties can be useful because checking them can reveal
that the system can't always do something that should be possible.
The properties we really want are realtime properties, which assert
that something must happen within some length of time. These are
safety properties and can be asserted by adding some kind of clock to
the system. It would be a nice exercise to add the requirement
that reservations time out after some number of days have elapsed.
This can be asserted by adding a
date
variable representing the number of days that have elapsed since the
library opened, with an
AdvanceDate
process that repeatedly advances the value of
date by one. A
reservation queue should include the date when an entry was added to
it. A requirement that a user checks out a book before a certain
date can be represented by an enabling condition on when the date can
be advanced.
There's no problem writing PlusCal specs with this kind of realtime
condition, though they might be simpler written directly in TLA+.
However, the number of reachable states in such a spec increases
exponentially with the length of time the system runs. The library
example is simple enough that it should be possible for TLC to check
models that allow time to advance far enough to adequately debug the
code.
Appendix A
[show]
This chapter describes mathematical concepts informally and
imprecisely, the way most
mathematicians do.
To truly understand the concepts, you should understand
how they can be stated rigorously and precisely.
I will try to help you do that.
When a mathematician writes a formula like x+2 > 4 , it can
be a noun as in
We know that if x equals 3 then
x+2 > 4 is true.
or it can be a complete clause, as in
If x equals 3, then x+2 > 4 .
In TLA+, as in all formal mathematics, formulas are nouns. The
assertion that the formula x+2 > 4 is true
is written in TLA+ as
THEOREM x+2 > 4
Whether or not this assertion is true depends on the context in which
it appears. For example, it is true if it appears
in a module and is preceded by
CONSTANT x
ASSUME x \in 3..10
It is false if it's preceded by
x == 2
A rigorous understanding of the mathematical concepts described
in this chapter is obtained by translating the informal assertions
made in the text to theorems, and understanding the context in which
those theorems are true.
 Page 200, line 9

Since their columns are different,
A /\ B /= A \/ B .
This is asserting that the following theorem is not true:
THEOREM A /\ B = A \/ B
The assumed context is:
CONSTANTS A, B
ASSUME (A \in BOOLEAN) /\ (B \in BOOLEAN)
(The theorem is true in a context in which
A and B
are Booleans and
A equals B .)
 Page 200, Line 14

Since their columns are the same,
A = ¬¬A .
This asserts the truth of:
CONSTANT A
ASSUME A \in BOOLEAN
THEOREM A = ¬¬A
 Page 201, line 10

Another way of saying A = B is to write A ⇔ B
The symbol ⇔ is typed
<=>
or
\equiv . It is the Boolean operator
such that for any Boolean values
A and B ,
the expression
A <=> B
equals TRUE if
A equals B
and otherwise equals FALSE .
The semantics of TLA+ do not specify the value of
A <=> B
unless both
A and B
are Booleans. Thus, TLC will evaluate
FALSE <=> TRUE
to equal FALSE , but
will report an error if it tries
to evaluate 42 <=> 27 .
It's good to write
exp1 <=> exp2
rather than
exp1 = exp2
if it appears in a context in which
exp1 and exp2
should both be Booleanvalued expressions, since TLC will
report an error if they're not.
 Page 202, line 10

x ∉ {{x}} but {x} ∈ {{x}}.
I believe this is asserting the following two theorems:
THEOREM x ∉ {{x}}
THEOREM {x} ∈ {{x}}
for any value of x . The second
theorem is true. Since {x}
is the one element of
{{x}} ,
the first theorem is true if and only if
x is not equal to
{x} .
But the semantics of TLA+ do not specify whether or not
x equals
{x} ,
so the first theorem is not a true TLA+ theorem.
 Page 203, Line 12

TLC can test membership of infinite sets
This means that for some infinite sets
T ,
TLC can test whether a value
v is in
T . Try TLC on these two expressions:
4 \in {x \in Nat : x % 2 = 0}
4 \in {2*x : x \in Nat}
 Page 204, Lines 1 to 5

Cardinal numbers like two and seventeen are answers to the
question
how many? . Zero is a cardinal number.
Ordinal numbers like second and seventeenth are answers
to the question which one? . The first ordinal number is
first; there is no number named zeroth. (That's
why the first element of a nonempty sequence
seq is
seq[1] .)
There is no good reason why either kind of number should be considered
more natural than the other.
The standard TLA+ modules define the set
Nat
of natural numbers to contain 0 because that's what computer scientists
do.
 Page 204, Lines 12 to 1

I find this discussion rather confusing. The Predicate
Logic section should have contained these theorems,
which are true for all sets
S and Booleanvalued operators
P :
THEOREM (\A x \in S : P(x)) <=> ¬ (\E x \in S : ¬ P(x))
THEOREM (\E x \in S : P(x)) <=> ¬ (\A x \in S : ¬ P(x))
They should help you understand the truth of the following theorems, for any
Booleanvalued operator
P :
THEOREM \A x \in {} : P(x)
THEOREM ¬ (\E x \in {} : P(x))
 Page 206, Line 2

TLA+ cannot quantify over infinite sets
This is false. The following is a perfectly legal TLA+ theorem
that the TLAPS proof system easily proves:
THEOREM \A x \in Nat \ {0} : 2*x > x
It is true that TLC cannot evaluate a formula
\A x \in S : ... or
\E x \in S : ...
if S is an infinite set.
Appendix B
[show]
 Page 208, line 10

It should be noted that the time and space TLC takes to evaluate
Order(set)
are exponential in the set's cardinality. The obvious
recursive definition would be evaluated more efficiently.
