Practical TLA+  by Hillel Wayne

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.

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 P-Version and C-Version to see which you prefer.  It should be easy to become bi-syntactic, 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.

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 higher-level 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.

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 mid-1980s.

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 non-declared 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 implementable--for 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.

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

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.

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.

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.

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 formula--that 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.

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.

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.

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 finite-state one.  TLC is generally run on a finite-state 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.

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 real-time 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 real-time 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.

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 Boolean-valued 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 non-empty 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 Boolean-valued 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 Boolean-valued 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.

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.