# Sequential algorithms in PlusCal/TLA

The following exercices use PlusCal and TLA to write and check algorithms. Please refer to the documentation ~herbrete/public/TLA/c-manual.pdf and ~herbrete/public/TLA/pluscal.pdf.

## Introduction to the PlusCal language

PlusCal is an algorithmic language. It differs from programming languages since:

• PlusCal algorithms can manipulate arbitrary mathematical objects (graphs, etc). Programming languages require to implement these objects using low-level types (integers, booleans, etc).
• PlusCal algorithms can be non-deterministic. Programs need to be deterministic in order to be executable.
• PlusCal has a well-defined notion of an atomic step. In general, the instructions in a program are not atomic (mechanisms are usually provided to group instructions in atomic steps)
• PlusCal has a formal semantics defined as TLA+ expressions.

The TLA tools offer three main features:

• The translation of PlusCal programs into TLA+ expressions.
• The TLC model-checker that allows to find bugs in algorithms, and to prove algorithms with finite resources.
• The TLA prover which is not in the scope of this class.

Follow the short tutorial on TLA+ extension webpage to get started with the environment.

## Model-checking Euclid’s GCD algorithm

### Modeling Euclid’s algorithm in PlusCal

Create an empty file euclid.tla and a module in thie file. Then, copy and paste Euclid’s algorithm below inside the module.

EXTENDS TLC, Integers

CONSTANT MAXINT  (* Maximal integer *)

(* PlusCal options (-termination) *)

(*
--algorithm EuclidAlg {
variables
u \in 1..MAXINT;
v \in 1..MAXINT;

{
print <<u, v>>;
while (u /= 0) {
if (u < v) {
u := v || v := u
};
u := u - v
}
}
}
*)

In this algorithm:

• EXTENDS is used to import libraries (here, the TLC library and the natural numbers library).
• CONSTANT introduces new symbolic names. Here MAXINT is a parameter of the algorithm. Its value is unspecified yet.
• The algorithm itself is placed inside a comment bloc (* ... *). Its specification starts with --algorithm followed by a name.
• Two variables u and v are declared. The declaration u \in 1..MAXINT defines the initial value of variable u. It is non-deterministically chosen in the set 1..MAXINT.
• The statement print <<u, v>> displays the value of the tuple <<u, v>>. Tuples can be made from any values, for instance <<"foo", u, 7>> is a valid tuple.
• PlusCal supports parallel assignment like u := v || v := u. The two assignments are executed in parallel. Thus the values of u and v are swapped by this statement.

Use the parse module command to check for syntax errors, and get a translation of Euclid’s algorithm in TLA+. The TLA+ translation corresponds to a logical description of the algorithm. It is used by the model-checking tool TLC to assess correcteness of the algorithm.

### Checking the correctness and the termination of Euclid’s Algorithm

Our goal is to check that this algorithm computest the greatest common divisor (gcd) of u and v.

• To that purpose, first add the following definition of the gcd immediately after the definition of constant MAXINT:
gcd(x,y) == CHOOSE i \in 1..x:
/\ x % i = 0
/\ y % i = 0
/\ \A j \in 1..x: x % j = 0 /\ y % j = 0 => i >= j
• Then, add 2 new variables u_init and v_init that are initialized to u and v respectively.
• Finally, add the following statements after the while loop in the algorithm:
print <<u_init, v_init, "have gcd", v>>;
assert v = gcd(u_init, v_init);
1. Translate the definition of gcd in natural language. What is provided by this definition?
2. Edit the file euclid.cfg and set CONSTANT MAXINT = 5. What is provided by this definition?
3. Use command Check module with TLC and observe the output. What can you conclude on the algorithm?
4. Observe the effect of choosing bigger values for constant MAXINT.
5. Replace the instruction u := u - v by u := u - v + 1 in the algorithm, then parse and check the algorithm. What do you observe?
6. Replace the instruction u := u - v + 1 by u := u - v - 1. Parse and check the algorithm. What can you conclude?

### Getting a counter-example for the correctness property

Assertion can be used to fail the model-checker when some condition is not met, just as a C program. However, this is not a convenient way to verify a program since the model-checker just stops and does not provide any insight on why the property is violated. We are going to replace the assertion in the algorithm by the following specification:

Postcond == [] (pc = "Done" => v = gcd(u_init, v_init))
1. What is expressed by the property Postcond above?
2. Comment the assertion using (* ... *). Then, copy and paste the property Postcond above after the \* END TRANSLATION. Add PROPERTY Postcond in the file euclid.cfg. Parse the algorithm, then run the model-checker. Explain what you observe.
3. Then fix the algorithm by setting back u := u - v instead of u := u - v. Check the algorithm. What can you conclude about your algorithm?

## Testing an implentation of Euclid’s algorithm

We now want to compare testing with model-checking.

1. Download the C implementation of Euclid’s algorithm euclid.c. Compile it: cc -std=c99 -Wall -o euclid euclid.c. Run the resulting executable euclid for different input values. What do you observe?
2. Read the source code euclid.c`. What are the differences with the PlusCal model?
3. What can you conclude regarding the termination of correctness of this implementation?