Session 2 Some Trivial Algorithms
Leslie Lamport
Last modified on Mon 19 August 2024 at 8:35:36 PST by lamport -->
|
|
1 A First Look at Algorithms
We will now begin looking at PlusCal algorithms. The tutorial
describes most of the PlusCal language, but you might want to
download and save
the PlusCal manual.
It contains a few features that aren't described here and provides
more detailed descriptions of ones that are.
Our first algorithm is in specification Session2 .
Open it in the Toolbox the same way you opened the specification
Session1 in
.
click here or type a letter to hide
This time, pay attention to how the module begins and ends.
(Beginners sometimes forget to add the MODULE
line or put their specification after the end of the
module, where it's ignored.)
Again, ignore the EXTENDS statement. The algorithm is
contained in a comment, which is enclosed by the delimiters
(* and *) . (You can also put such comments
inside the algorithm.) The algorithm itself begins with:
--algorithm AnyName {
where AnyName can be replaced by any
That name is not used anywhere. The algorithm is
terminated by a matching right brace } .
click here or type a letter to hide
The body of the algorithm begins with a declaration of all its
variables. The statement
variable x = 1 ;
declares x to be the only variable and to have the initial
value 1 . The rest of the algorithm's body is code
enclosed in curly braces { } . In this example,
that code simply adds 1 to x and
then prints the value of x :
x := x + 1 ;
print x
Unlike most of today's popular programming languages,
PlusCal uses := for
assignment. It uses = to mean what
it's meant for hundreds of years.
As in many languages, the semicolon ; indicates that
the print statement is to be executed immediately after
the assignment statement. Semicolons must come between
statements, but you can put a semicolon after the print
statement if it makes you happier.
To execute the algorithm, we must first run the PlusCal to TLA+
translator. You can run the Translate PlusCal Algorithm
command from the Toolbox's File menu, but it's much easier to
just type Control-T. This will add the resulting TLA+
specification to the module right below the comment containing the
algorithm. Don't try to read that specification.
As you've seen, TLC is run on a model. This time, you will
create a new model. As before, click on TLC Model Checker
in the Toolbox's top menu bar, but this time choose New
Model . This raises the New model window that
allows you to choose a name for the model. I'm usually happy
with the default name Model_1. Clicking
OK opens the Model Overview sub-tab of the new
model. Ignore what's on it. Run TLC by clicking on the
icon
in the upper-left corner of the sub-tab. TLC should run for a
few seconds and then raise the model's Model Checking Results
sub-tab. The output of the print statement appears
in the sub-tab's User Output section. It obviously should
show the value 2.
PlusCal treats all mathematical values and operations on them the
same, which is the way most programming languages treat only numbers
and a handful of other kinds of values. Check this out by
doing the following exercise.
Exercise 1 Modify algorithm AnyName to give
x the set {"a","b"} as its initial value and
so the assignment statement assigns to x the set obtained
by adding to this set the string "c".
(If you don't remember how to add an element to
a set, review the
.)
Save the module, run the translator, and then run TLC (on the same
model) to check that it prints {"a", "b", "c"} .
Show
the answer.
--algorithm AnyName {
variable x = {"a","b"} ;
{
x := x \cup {"c"} ;
print x
}
}
click here or type a letter to hide
Exercise 2 Now modify the algorithm so that instead
of adding "c" to the set
{"a", "b"} , it removes the "a" from that
set.
Show
the answer.
--algorithm AnyName {
variable x = {"a","b"} ;
{
x := x \ {"a"} ;
print x ;
}
}
2 Assigning to a Tuple
Now let's try setting x to a tuple and modifying it.
Enter the following algorithm body, which you can do by typing or
copy/pasting.
variable x = <<1, 2, 3>> ;
{
x[3] := x[2] + 4 ;
print x
}
Save the module, run the translator, and run TLC. It should print
<<1, 2, 6>> , which is probably what you expected.
Now modify the algorithm by adding the green code shown here:
variable x = <<1, 2, 3>> , y = x ;
{
x[3] := x[2] + 4 ;
print x ;
print y
}
This declares a second variable y (note the comma between
the two variable declarations) and declares its initial value to be
the initial value of x , which is
<<1, 2, 3>> .
This is legal because x has already been declared
and its initial value specified.
The code prints the value of y after it prints the value
of x . It will, of course, print the same value of
x as before. What value do you expect it to print
for y ? Save/translate/run TLC and see what it actually
prints.
Were you surprised? You shouldn't have been.
PlusCal treats all mathematical values the same. If the
algorithm had initialized x and y to the
number 42, you wouldn't have expected assigning a new value to
x to have changed the value of y .
Since all values are handled the same, this is true for assigning a
tuple to the variables. So, you should have expected the
print y statement to have printed
<<1, 2, 3>> ,
the initial value of y . If that's not what you
expected,
.
click here or type a letter to hide
|