1 Nondeterminism

1.1 Why?


1.2 The with Statement


2 More About Sets

2.1 Specifying a Subset


2.2 Building a Set


2.3 Sets of Sets


2.4 The Cartesian Product


Prev:  Session 3

Next:  Session 5

Contents
 ↑

top

 ↑

top

 ↑

top

 ↑

top

 ↑

top

 ↑

top

 ↑

top

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 set-valued 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 integer-valued loop variable i to examine inp[i].  To examine the elements in an arbitrary order, we use a while statement with the set-valued 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 non-maximal 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.  Why is this deadlock?

2  More About Sets

Sets are a very important data type for describing algorithms.  Here are the remaining built-in 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 drop-down 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 Boolean-valued 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 bound variable.

Exercise 2   Write the set of all prime numbers.  Show the answer.

Answer   Here are two possible answers, using the definition of IsPrime from Session 1:

{n \in Int : IsPrime(n)}    and    {n \in Nat : IsPrime(n)}

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 3-tuples <<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 built-in 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} }
A note on parsing.

Mathematicians call SUBSET S the powerset of S; they write it P(S) or sometimes 2S—the latter notation because if S is a finite set with n elements, then SUBSET S has 2n 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 {S1, S2, ... , S99}   and   S1 \cup S2 \cup  ... \cup S99
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 2-tuples (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 3-tuples.

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 1-tuples whose element is in the set S ?  Show the answer.

Answer   I can think of these two: [{1} -> S] and {<<s>> : s \in S}