1 Labels
In TLA+, an execution of an algorithm is described as a sequence of
states.
The change from one state to the next is called a step.
In the algorithms we've considered so far, execution of a single
iteration of a As we'll see in later sessions, what constitutes a single step is an important part of the definition of a multiprocess algorithm. The translator shouldn't decide it; we need to specify it ourselves. In PlusCal, what constitutes a step is described with labels. From now on, we will add the labels ourselves instead of letting the translator decide where they should go.
Open the specification
Algorithm
In any state, the value of the variable
The specification
has a model that assigns the value 2 to
Read the trace and understand the details of each step. Observe
that the 1^{st}, 3^{rd}, and 5^{th}
steps are
Now label the assignment to
c: i := i + 1 ;and run TLC on the algorithm. This will produce an error trace with 7 steps (8 states). In that trace, an a step
represents the evaluation of the while test; it changes
only the value of pc .
Now remove the labels 2 The TLA+ Translation
Let's now look at the TLA+ translation.
First, restore the original algorithm
The translation of
Next comes the definition of
/\ x = 0 /\ i = 0 /\ pc = "a"It is a formula that is true iff the variables x ,
i , and pc have the values assigned to them
by the first state of the execution. Change the algorithm's
variables declaration to
variables x = 0, i \in 0..3 ;and run the translator (but not TLC). This changes the conjunct i = 0 in the definition of Init to i
\in 0..3 . The initial state of the trace is then just one
of four initial states allowed by the new algorithm, each of which
gives rise to a different possible execution. Change the
declaration of i in the algorithm back to
i = 0 and run the translator again.
After the definition of
Until the algorithm terminates, it can take steps that start
with
/\ pc = "b" /\ x' = x + (2*i  1) /\ pc' = "a" /\ i' = iA step is said to be a b step iff this formula is
satisfied when the unprimed variables have their values in the
step's starting state and the primed variables have their values in
the step's ending state.
Let's check that the 4^{th} step of the trace, shown here, is a
b step.
Replacing the unprimed variables in formula b with their
values in the first state, coloring those values green, gives us:
/\ "b" = "b" /\ x' = 1 + (2*2  1) /\ pc' = "a" /\ i' = 2Then replacing the primed variables with their values in the second state, coloring them red, we get:
/\ "b" = "b" /\ 4 = 1 + (2*2  1) /\ "a" = "a" /\ 2 = 2The resulting formula obviously equals TRUE .
Check that the second step of the trace likewise satisfies
formula b .
Any pair of states satisfying formula
Following the definitions of formulas
pc = "Done" /\ UNCHANGED varsBecause vars equals the tuple
<< ,
the formula UNCHANGED vars is an abbreviation for
the formula:
(x' = x) /\ (i' = i) /\ (pc' = pc)Thus, a step is a Terminating step—one that
satisfies formula Terminating —iff it starts
in a state in which pc equals "Done" and
leaves the values of all variables (including pc )
unchanged. This formula Terminating appears
in the translation of any algorithm that can terminate,
with vars defined to equal the tuple of the particular
algorithm's variables. The step described by the arrow from
the terminated state to itself in the
state graph of the Session5
algorithm
is a Terminating step. Remember that the
translation permits Terminating steps so TLC doesn't
think the algorithm has deadlocked when it has terminated.
The definitions that come next appear in translations of all PlusCal
algorithms. Formula
If you change
The translation ends with the definition of formula
3 Invariants
Instead of using an If the state is a terminated state, then the postcondition is true in that state.For Square , satisfaction of the postcondition is
equivalent to the invariance of the formula
(pc = "Done") => (x = N^2)since a formula of the form (pc = "Done") => ... is
trivially true in any state with pc not equal to
"Done" . (If you don't find this obvious,
review
the definition of implication
.)
Look at the Invariants section of the What to check? section of the model's Model Overview tab. It tells TLC to check the invariance of:
(pc = "Done") => (x /= N^2)Since algorithm Square satisfies its postcondition, this
formula is not an invariant because it is not true of the terminated
state.
Since the shortest execution that shows the formula is not an
invariant is an execution that terminates, TLC's error trace describes
a terminating execution. Since we haven't declared the algorithm
to be fair , an execution can stop before it terminates,
but such an execution does not violate the invariant.
Edit the alleged invariant in the model to replace
Exercise 1 Test the correctness of algorithm
You may have noticed that PlusCal does not require type declarations
for variables. In PlusCal, type correctness is an invariance
property. It's a useful property to check, since it quickly
catches a lot of trivial errors. In a conventional typed
programming language, the variables
TypeOK == /\ x \in Int /\ i \in Int /\ pc \in STRINGTLA+ defines STRING to be the set of all its legal
strings. Add TypeOK to the list of invariants to be
checked by the model and run TLC. It should report no error.
TLA+ allows a more precise and useful type invariant than this.
For example, instead of just stating that the value of
TypeOK == /\ x \in 0..N^2 /\ i \in 0..N /\ pc \in {"a", "b", "Done"}It provides more information to the reader of the specification and checks your understanding of the algorithm. Replace the definition of TypeOK you just added to the specification with this one,
and run TLC to check that it actually is an invariant.
Invariance is arguably the most important concept in programming. What an algorithm or a program does next depends only on its current state, not what it did in the past. To understand why an algorithm is correct, we must understand at each point in its execution what it is about the current state that ensures it must produce a correct result. That understanding is best expressed as an invariant. By definition, an invariant is true on all reachable states of the algorithm. The invariant that provides the most information about an algorithm is one that is true only on its reachable states. That invariant is usually too complicated to write down. However, it can be written for the simple algorithms we've been looking at. But even for them, it's not easy. Before looking at the answer to the following exercise, check your answer by counting how many states are allowed by your invariant and comparing it with the number of reachable states TLC found. (You saw how to find the number of reachable states here.)
Exercise 2
Define an invariant
Answer Here are two equivalent answers. The first
uses the second definition of
Inv == /\ TypeOK /\ (pc = "a") => (x = i^2) /\ (pc = "b") => (x = (i1)^2) /\ (i > 0) /\ (pc = "Done") => (x = N^2) /\ (i = N) Inv == /\ i \in 0.. N /\ \/ (pc = "a") /\ (x = i^2) \/ (pc = "b") /\ (x = (i1)^2) /\ (i > 0) \/ (pc = "Done") /\ (x = N^2) /\ (i = N) Most algorithms are too complicated to have a simple invariant that is true only on reachable states. However, an algorithm is correct because it maintains a suitable invariant. Learning to express an intuitive understanding of an algorithm's correctness with a formula whose invariance captures that understanding is not easy, but it makes one a better algorithm designer and therefore a better programmer. This tutorial does not try to teach you that skill. 4 Functions
We will now modify algorithm
So far, the only functions we've been able to write explicitly are
tuples, where a tuple
[i \in D > exp]for any expression exp , which can contain i .
(The symbol > is prettyprinted ↦.) This defines
the function, let's call it f here, with domain
D such that f[i] equals exp for
all i in D . For example, the value we
want x to equal when our new algorithm terminates is
[j \in 0..N > j^2]The algorithm will let the initial value of x
be the function with domain 0..N such that
x[j] equals 0 for all j in its domain.
You should be able to write the code.
Exercise 3 Modify the algorithm as indicated above. Modify the model's invariant so it checks that the new algorithm satisfies its postcondition and check that it's correct. Show the answer. Answer Two lines of code need to be modified: The variable declaration becomes
variables x = [j \in 0..N > 0], i = 0 ;and statement b becomes
b: x[i] := x[i1] + (2*i  1)The invariant is
(pc = "Done") => (x = [j \in 0..N > j^2]) b should be? Here is what almost
every reader of this tutorial would answer:
b == /\ pc = "b" /\ x'[i] = x[i1] + (2*i  1)] /\ pc' = "a" /\ i' = iPlusCal users don't have to understand why that's not correct. But if you're curious, here is an explanation. As you can see, the second conjunct of the actual translation is:
x' = [x EXCEPT ![i] = x[i1] + (2*i  1)]Spoken languages all have idioms that make no sense to nonnative speakers, who learn what idioms mean without understanding why they mean it. This piece of the translation is a TLA+ idiom. Since you understand the meaning of the PlusCal statement b , you should understand what the idiom means. One
of the advantages of using PlusCal instead of using TLA+ directly is
that you don't have to understand why this idiom means what it
does. You should be aware of the idiom because you may have to
look at the translation when debugging an algorithm, and you shouldn't
be freaked out when you see the mysterious EXCEPT s.
back to top
