Session 4 Nondeterminism and Sets
Leslie Lamport
Last modified on 6 December 2021


1 Nondeterminism
1.1 Why Nondeterminism?
Our algorithms for computing the maximum element of the tuple
inp examine the elements in order, starting with
inp[1] . However, that's not necessary; the elements
can be examined in any order. If you're designing an algorithm
just for use in one program, examining them in a particular order is
fine. But there may be other programs in which it would be
better to examine them in some other order. If you're writing
the algorithm for others to use, it's best to allow it to examine the
elements in any order. Of course, this is silly for our simple
example; but it could be an issue for a subtle, complicated algorithm.
So, you should know how to do it.
1.2 The with Statement
An algorithm that allows multiple executions is said to be
nondeterministic. We've already introduced nondeterminism
into algorithm TupleMax
by allowing it to start with inp
having any of a set of initial values. We now add
nondeterminism in the rest of the execution. This is done
in PlusCal with the with statement. For any identifier
id that does not already have a meaning and any setvalued expression
S , the statement
with (id \in S) { body }
causes the code body to be executed with id
equal to an arbitrary (nondeterministically chosen) element of
S . Of course, id can appear in
body .
To examine the elements of inp in a fixed order, we used a
while statement with an integervalued loop variable
i to examine inp[i] . To examine the
elements in an arbitrary order, we use a while statement
with the setvalued loop variable I to examine
inp[i] for an arbitrarily chosen element i
of I . Here is an outline of the two ways of
examining the tuple's elements:
fixed order arbitrary order
variables ... i = 1 ; variables ... I = 1..Len(inp)
... ...
while (i =< Len(inp)) { while (I /= {}) {
examine inp{i] ; with (i \in I) {
i := i + 1 examine inp{i] ;
} I := I \ {i}
}
}
The complete algorithm TupleMaxND that examines the
elements in an arbitrary order is in specification
Session4 , which is among the ones you downloaded.
Open that specification and examine the code. The translation is
included, as is a model you can run to test the algorithm. For
all nondeterministic algorithms, TLC checks all possible executions.
Exercise 1 Write an algorithm
SillyTupleMax by modifying TupleMax to work
in the following silly way. It repeatedly examines an arbitrary
element of the tuple inp and terminates with max
equal to that value if it is the maximum value of all the tuple's
elements. Thus, if it's lucky, it can terminate after trying a
single element. If it's very, very unlucky, it can keep picking
nonmaximal elements and never terminate.
Show the answer.
Answer
Here is my solution. It uses a variable b whose value is
always a Boolean. The while loop terminates when
b equals FALSE . It equals
FALSE initially iff inp is the empty
tuple. It is set to FALSE and max
is set to inp[i] if the with
statement chooses a value i such that inp[i]
is a maximal element, as determined by the if test.
algorithm SillyTupleMax {
variables inp \in Tuples, max = minValue, I = 1..Len(inp), b = (I /= {}) ;
{ while (b) {
with (i \in I) {
if (\A j \in I : inp[i] >= inp[j]) {
max := inp[i] ;
b := FALSE
}
}
} ;
assert IF inp = << >> THEN max = minValue
ELSE /\ \E n \in 1..Len(inp) : max = inp[n]
/\ \A n \in 1..Len(inp) : max >= inp[n]
}
}
It is possible for algorithm SillyTupleMax
never to terminate. For
example, for any input tuple not all of whose element are the same, it
is possible for the with statement to keep choosing some
i for which inp[i] is not maximal. Why
the possibility of nontermination doesn't cause TLC to report
an error is explained in the next session.
In either TupleMaxND or your algorithm
SillyTupleMax , change the with (i \in I) to
with (i \in {})
and run the translator. What do you think the algorithm now does?
Run TLC and find out.
TLC should have reported the error: Deadlock reached.
The with statement is supposed to execute its body
with i equal to an element of the empty set, which is
impossible because there is no such element. So, execution
must stop.
click here or type a letter to hide
2 More About Sets
Sets are a very important data type for describing algorithms.
Here are the remaining builtin TLA+ operators for defining
sets. Use TLC to check your understanding of these operators on
examples by entering them in the Evaluate Constant Expression
section of the model's Model Checking Results tab. TLC
will evaluate expressions you enter there when it checks an
algorithm. You can suppress checking of the algorithm by using
the dropdown menu in the What is the behavior spec section of
the Model Overview page to select the No behavior spec
option. Don't forget to change it back to the Temporal
formula option when you do want TLC to check the algorithm.
You can also create a separate model just for evaluating expressions
by changing that option on a cloned copy of an existing model, which
you can create by clicking the main menu's TLC Model Checker
button and selecting Clone Model.
2.1 Specifying a Subset
If S is a set and exp is a
Booleanvalued expression, then
{x \in S : exp }
is the subset of S consisting of all elements
x in S for which exp equals
TRUE . For example, since n % 2 equals
zero iff n is a multiple of 2,
{n \in Int : n % 2 = 0}
is the set of all even integers. In this expression, n
is a
click here or type a letter to hide
Exercise 2 Write the set of all prime numbers.
Show the answer.
Answer Here are two possible answers, using the
from Session 1:
{n \in Int : IsPrime(n)} and {n \in Nat : IsPrime(n)}
click here or type a letter to hide
2.2 Building a Set
If S is a set and exp is any
expression, then
{exp : x \in S}
is the set of all elements obtained from exp by
substituting elements of S for x . For
example {2 * n : n \in Int} equals the set of all even
integers. In this expression, n is a bound
variable.
Let's compare these two ways of defining the set of
even integers:
EvenInt1 == {n \in Int : n % 2 = 0}
EvenInt2 == {2 * n : n \in Int}
They define EvenInt1 and EvenInt2 to both
equal the same set—the set of all integers that are multiples
of 2. The first defines a subset of Int ; the second
builds a new set of elements from the elements of
Int . I don't know of any standard names for these
two ways of describing sets, so I'll call the first
subsetting and the second building.
While the definitions of EvenInt1 and EvenInt2
are mathematically equivalent, TLC handles them differently.
In particular, TLC can evaluate the expression
42 \in EvenInt1 , but not the expression
42 \in EvenInt2 .
To tell if a value is an element of a set described with building, TLC
has to construct the entire set, which it can do only if the set is
finite.
The building construct has an abbreviation involving multiple bound
variables similar to that of the quantifiers \A and
\E . For example,
{<<i , j, k>> : i, j \in Int, k \in Nat}
is the set of all 3tuples <<i ,j,k>> such
that i and j are integers
and k is a natural number. It is an abbreviation
of:
{ { {<<i , j, k>> : i \in Int} : j \in Int } : k \in Nat }
Exercise 3
Write the set of all pairs <<p , q>> of integers such
that p is less than q .
Show the answer.
Answer
{ t \in {<<p , q>> : p, q \in Int} : t[1] < t[2] }
2.3 Sets of Sets
Sets of sets are often used in algorithms.
There are two builtin TLA+ set operators that involve such sets.
SUBSET
The operator SUBSET is defined so that for
any set S , the expression
SUBSET S
is the set of all subsets of S . For example,
SUBSET {1,2,3} equals
{ {}, {1}, {2}, {3}, {1,2}, {1,3}, {2,3}, {1,2,3} }
click here or type a letter to hide
Mathematicians call SUBSET S the powerset
of S ; they write it P(S)
or sometimes 2^{S} —the latter notation
because if S is a finite set with n elements,
then SUBSET S has 2^{n}
elements. Note that for any sets S and T ,
the these two expressions are equal:
S \subseteq T and S \in SUBSET T
UNION
The operator UNION is defined so that for any
set S whose elements are sets, UNION S
equals the union of all the elements of S .
Thus, these two sets are equal:
UNION {S_{1}, S_{2}, ... , S_{99}} and S_{1} \cup S_{2} \cup ... \cup S_{99}
In general, the set UNION S is the set of all elements of
elements of S . This can get confusing; even I
occasionally find it hard to understand some formula containing
UNION . It's an operator that takes time to get
comfortable with. Here are two observations that will help you
get started:
 Any set
S equals UNION (SUBSET S) .
 Any set
S of sets is a subset of (possibly equal to)
SUBSET (UNION S)
Exercise 4
Use UNION to write the set of all tuples of length at
most 21 whose elements are "a" , "b" ,
or "c" .
Show the answer.
Answer Since [1..i > S]
is the set of all tuples of length i with elements
in S , the answer is:
UNION {[1..i > {"a","b","c"}] : i \in 0..21}
Puzzle 1
Define Intersect so that for any set S
of sets, Intersect(S) is the intersection of the
sets in S —that is, the set of all elements that are
in all the elements of S .
Show the answer.
Answer A value v is an element of
Intersect(S) iff the formula
\A r \in S : v \in r
is true.
This suggests using the subsetting construct to write the
definition in the form:
Intersect(S) == {v \in ... : \A r \in S : v \in r}
The trick is finding a set ...
that contains all
the elements of Intersect(S) . That set is
UNION S .
Puzzle 2
What does this set equal: {(x \in S) : x \in S} ?
Show the answer.
Answer The parentheses mean that this is
a building construct rather than a subsetting construct.
Since the expression x \in S equals TRUE for every
element x of S , the set
{(x \in S) : x \in S} equals {TRUE}
except in one case. What is that case?
Show the answer.
Answer
The empty set has no elements, so
{(x \in {}) : x \in {}}
equals the empty set {} .
2.4 The Cartesian Product
If S and T are sets,
S \X T
is the set of all 2tuples (ordered pairs) whose first element is
in S and whose second element is in T .
In other words, S \X T equals
{<<s , t>> : s \in S, t \in T}
Mathematicians call \X the Cartesian product
and write it × . We can also form the Cartesian product
of three or more sets. For example, S \X T \X U
is the obvious set of 3tuples.
Exercise 5
What is this set: (S \X T) \X U ?
Show the answer.
Answer The set
{<< <<s , t>>, u >> : s \in S, t \in T, u \in U}
of all ordered pairs whose first element is in S \X T
and whose second element is in U .
Exercise 6
How many ways can you write the set of all 1tuples whose element
is in the set S ?
Show the answer.
Answer I can think of these two:
[{1} > S] and
{<<s >> : s \in S}
