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:

The TLA tools offer three main features:

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:

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.

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
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?