TLA in Pictures

Leslie Lamport

Abstract— Predicate-action diagrams, which are similar to standard state-transition diagrams, are precisely defined as formulas of TLA (the Temporal Logic of Actions). We explain how these diagrams can be used to describe aspects of a specification—and those descriptions then proved correct— even when the complete specification cannot be written as a diagram. We also use the diagrams to illustrate proofs.

Keywords— Concurrency, specification, state-transition diagrams, temporal logic.

I. Introduction

Pictures aid understanding. A simple flowchart is easier to understand than the equivalent programming-language text. However, complex pictures are confusing. A large, spaghetti-like flowchart is harder to understand than a properly structured program text.

Pictures are inadequate for specifying complex systems, but they can help us understand particular aspects of a system. For a picture to provide more than an informal comment, there must be a formal connection between the complete specification and the picture. The assertion that the picture is a correct description of (some aspect of) the system must be a precise mathematical statement.

We use TLA (the Temporal Logic of Actions) to specify systems. In TLA, a specification is a logical formula describing all possible correct behaviors of the system. As an aid to understanding TLA formulas, we introduce here a type of picture called a predicate-action diagram. These diagrams are similar to the various kinds of state-transition diagrams that have been used for years to describe systems, starting with Mealy and Moore machines [1], [2]. We relate these pictures to TLA specifications by interpreting a predicate-action diagram as a TLA formula. A diagram denoting formula D is a correct description of a system with specification S iff (if and only if) S implies D. We therefore provide a precise statement of what it means for a diagram to describe a specification.

We use predicate-action diagrams in three ways that we believe are new for a precisely defined formal notation:

• To describe aspects of a specification even when it is not feasible to write the complete specification as a diagram.

• To draw different diagrams that provide complementary views of the same system.

• To illustrate formal correctness proofs. Section II is a brief review of TLA; a more leisurely in-

troduction to TLA appears in [3]. Section III describes predicate-action diagrams, using an n-input Muller Celement as an example. It shows how diagrams are used to describe aspects of a complete specification, and to provide complementary views of a system. Section IV gives another example of how predicate-action diagrams are used to describe a system, and shows how they are used to illustrate a proof.

II. TLA

We now describe the syntax and semantics of TLA. The description is illustrated with the formulas defined in Figure 1. (The symbol =^{Δ} means equals by definition.)

We assume an infinite set of variables (such as x and y) and a class of semantic values. Our variables are the flexible variables of temporal logic, which are analogous to variables in a programming language. TLA also includes the rigid variables of predicate logic, which are analogous to constant parameters of a program, but we ignore them here. The class of values includes numbers, strings, sets, and functions.

A state is an assignment of values to variables. A behavior is an infinite sequence of states. Semantically, a TLA formula is true or false of a behavior. Syntactically, TLA formulas are built up from state functions using Boolean operators (¬, ∧, ∨, ⇒ [implication], and ≡ [equivalence]) and the operators ′ and □, as described below. TLA also has a hiding operator ∃ ∃ ∃ ∃ ∃ ∃, which we do not use here.

A state function is a nonBoolean expression built from variables, constants, and constant operators. Semantically, it assigns a value to each state—for example x + 1 assigns to state s one plus the value that s assigns to the variable x. A state predicate (often called just a predicate) is a Boolean expression built from variables, constants, and constant operators such as +. Semantically, it is true or false for a state—for example the predicate Init_{Φ} is true of state s iff s assigns the value zero to both x and y.

An action is a Boolean expression containing primed and unprimed variables. Semantically, an action is true or false of a pair of states, with primed variables referring to the second state—for example, action M_{1} is true for ⟨s, t⟩ iff the value that state t assigns to x equals one plus the value that state s assigns to x, and the values assigned to y by states s and t are equal. A pair of states satisfying an action A is called an A step. Thus, an M_{1} step is one that increments x by one and leaves y unchanged.

If f is a state function or state predicate, we write f′ for the expression obtained by priming all the variables of f. For example (x + 1)′ equals x′ + 1, and Init′_{Φ} equals (x′ = 0) ∧ (y′ = 0). For an action A and a state function v,

Init_{Φ} =^{Δ} (x = 0) ∧ (y = 0)

M_{1} =^{Δ} (x′ = x + 1) ∧ (y′ = y)

M_{2} =^{Δ} (y′ = y + 1) ∧ (x′ = x)

M =^{Δ} M_{1} ∨ M_{2}

Φ =^{Δ} Init_{Φ} ∧ □[M]_{⟨x, y⟩} ∧ WF_{⟨x, y⟩}(M_{1}) ∧ WF_{⟨x, y⟩}(M_{2})

Fig. 1. The TLA formula Φ describing a simple program that repeatedly increments x or y.

we define [A]_{v} to equal A∨(v′ = v), so a [A]_{v} step is either an A step or a step that leaves the value of v unchanged. Thus, a [M_{1}]_{⟨x,y⟩} step is one that increments x by one and leaves y unchanged, or else leaves the ordered pair ⟨x, y⟩ unchanged. Since a tuple is unchanged iff each component is unchanged, a [M_{1}]_{⟨x,y⟩} step is one that increments x by one and leaves y unchanged, or else leaves both x and y unchanged. We define ⟨A⟩_{v} to equal A ∧ (v′ ≠ v), so an ⟨M_{1}⟩_{⟨x,y⟩} step is an M_{1} step that changes x or y. Since an M_{1} step leaves y unchanged, an ⟨M_{1}⟩_{⟨x,y⟩} step is a step that increments x by 1, changes the value of x, and leaves y unchanged.

We say that an action A is enabled in state s iff there exists a state t such that ⟨s, t⟩ is an A step. For example, M_{1} is enabled iff it is possible to take a step that increments x by one, changes x, and leaves y unchanged. Since x + 1 ≠ x for any natural number x, action ⟨M_{1}⟩_{⟨x,y⟩} is enabled in any state in which x is a natural number. If ∞ + 1 equals ∞, then ⟨M_{1}⟩_{⟨x,y⟩} is not enabled in a state in which x equals ∞.

A TLA formula is true or false of a behavior. A predicate is true of a behavior iff it is true of the first state. An action is true of a behavior iff it is true of the first pair of states. As usual in temporal logic, if F is a formula then □F is the formula meaning that F is always true. Thus, □Init_{ϕ} is true of a behavior iff x and y equal zero for every state in the behavior. The formula □[M]_{⟨x,y⟩} is true of a behavior iff each step (pair of successive states) of the behavior is a [M]_{⟨x,y⟩} step.

Using □ and “enabled” predicates, we can define fairness operators WF and SF. The weak fairness formula WF_{v}(A) asserts of a behavior that there are infinitely many ⟨A⟩_{v} steps, or there are infinitely many states in which ⟨A⟩_{v} is not enabled. In other words, WF_{v}(A) asserts that if ⟨A⟩_{v} becomes enabled forever, then infinitely many ⟨A⟩_{v} steps occur. The strong fairness formula SF_{v}(A) asserts that either there are infinitely many ⟨A⟩_{v} steps, or there are only finitely many states in which ⟨A⟩_{v} is enabled. In other words, SF_{v}(A) asserts that if ⟨A⟩_{v} is enabled infinitely often, then infinitely many ⟨A⟩_{v} steps occur.

The standard form of a TLA specification is Init ∧ □[N]_{v} ∧ L, where Init is a predicate, N is an action, v is a state function, and L is a conjunction of fairness conditions. This formula asserts of a behavior that (i) Init is true for the initial state, (ii) every step of the behavior is an N step or leaves v unchanged, and (iii) L holds. Formula Φ of Figure 1 is in this form, asserting that (i) initially x and y both equal zero, (ii) every step either increments x by one and leaves y unchanged, increments y by one and leaves x unchanged, or leaves both x and y unchanged, and (iii) the fairness condition WF_{⟨x, y⟩}(M_{1}) ∧ WF_{⟨x, y⟩}(M_{2}) holds. Formula WF_{⟨x, y⟩}(M_{1}) asserts that there are infinitely many ⟨M_{1}⟩_{⟨x,y⟩} steps or ⟨M_{1}⟩_{⟨x,y⟩} is infinitely often not enabled. Since (i) and (ii) imply that x is always a natural number, ⟨M_{1}⟩_{⟨x,y⟩} is always enabled. Hence, WF_{⟨x, y⟩}(M_{1}) implies that there are infinitely many ⟨M_{1}⟩_{⟨x,y⟩} steps, so x is incremented infinitely often. Similarly, WF_{⟨x, y⟩}(M_{2}) implies that y is incremented infinitely E n v i r o n m e n t C - E l e m e n t in[1]

in[n]

out

⋮

Fig. 2. A Muller C-element.

often. Putting this all together, we see that Φ is true of a behavior iff (i) x and y are initially zero, (ii) every step increments either x or y by one and leaves the other unchanged or else leaves both x and y unchanged, and (iii) both x and y are incremented infinitely many times. The formula Init ∧ □[N]_{v} is a safety property [4]. It describes what steps are allowed, but it does not require anything to happen. (The formula is satisfied by a behavior satisfying the initial condition in which no variables ever change.) Fairness conditions are used to specify that something must happen.

III. Predicate-Action Diagrams

A. An Example

We take as an example a Muller C-element [5]. This is a circuit with n binary inputs in[1], …, in[n] and one binary output out, as shown in Figure 2. As the figure indicates, we are considering the closed system consisting of the Celement together with its environment. Initially, all the inputs and the output are equal. The output becomes 0 when all the inputs are 0, and it becomes 1 when all the inputs are 1. After an input changes, it must remain stable until the output changes.

The behavior of a 2-input C-element and its environment is described by the predicate-action diagram of Figure 3(a), where C is defined by

C(i, j, k) =^{Δ} (in[1] = i) ∧ (in[2] = j) ∧ (out = k)

The short arrows, with no originating node, identify the nodes labeled C(0, 0, 0) and C(1, 1, 1) as initial nodes. They indicate that the C-element starts in a state satisfying C(0, 0, 0) or C(1, 1, 1). The arrows connecting nodes indicate possible state transitions. For example, from a state satisfying C(1, 1, 1), it is possible for the system to go to a state satisfying either C(0, 1, 1) or C(1, 0, 1). More precisely, these arrows indicate all steps in which the triple ⟨in[1], in[2], out⟩ changes—that is, transitions in which at least one of in[1], in[2], and out changes. Steps that change other variables—for example, variables representing circuit elements inside the environment—but leave ⟨in[1], in[2], out⟩ unchanged are also possible.

The predicate-action diagram of Figure 3(a) looks like a standard state-transition diagram. However, we interpret it formally not as a conventional state machine, but as the

(a) A predicate-action diagram.

[figure: C(0, 0, 0); C(1, 0, 0); C(0, 1, 0); C(1, 1, 0); C(1, 1, 1); C(0, 1, 1); C(1, 0, 1); C(0, 0, 1)]

(b) The corresponding TLA formula.

∧ C(0, 0, 0) ∨ C(1, 1, 1)
∧ □[C(0, 0, 0) ⇒ C(1, 0, 0)′ ∨ C(0, 1, 0)′]_{⟨in[1],in[2],out⟩}
∧ □[C(1, 0, 0) ⇒ C(1, 1, 0)′]_{⟨in[1],in[2],out⟩}
…
∧ □[C(0, 0, 1) ⇒ C(0, 0, 0)′]_{⟨in[1],in[2],out⟩}

Fig. 3. Predicate-Action diagram of ⟨in[1], in[2], out⟩ for a 2-input C-element, and the corresponding TLA formula.

TLA formula of Figure 3(b).^{1} This formula has the form Init ∧ ⋀_{o} F_{o}, where Init is a state predicate and there is one conjunct F_{o} for each node o. The predicate Init is C(0, 0, 0) ∨ C(1, 1, 1). Each F_{o} describes the possible state changes starting from a state described by node o. For example, the formula F_{o} for the node labeled C(1, 1, 0) is

□[C(1, 1, 0) ⇒ C(1, 1, 1)′]_{⟨in[1],in[2],out⟩}

A predicate-action diagram represents a safety property; it does not include any fairness conditions.

Figure 3(a) is a reasonable way to describe a 2-input C-element. However, the corresponding diagram for a 3input C-element would be quite complicated; and there is no way to draw such a diagram for an n-input circuit. The general specification is written directly as a TLA formula in Figure 4. The array of inputs is represented formally by a variable in whose value is a function with domain {1, …, n}, where square brackets denote function application. (Formally, n is a rigid variable—one whose value is constant throughout a behavior.) We introduce two pieces of notation for representing functions:

• [i ∈ S ↦ e(i)] denotes the function f with domain S such that f[i] equals e(i) for every i in S.

• [f except ![i] = e] denotes the function g that is the

same as f except that g[i] equals e. The formulas defined in Figure 4 have the following interpretation.

Init_{C} A state predicate asserting that out is either 0 or 1, and that in is the function with domain {1, …, n} such that in[i] equals out for all i in its domain.

Input(i) An action that is enabled iff in[i] equals out. It complements in[i], leaves in[j] unchanged for j ≠ i, and leaves out unchanged. (The symbol i is a parameter.)

Output An action that is enabled iff all the in[i] are different from out. It complements out and leaves in unchanged.

1A list of formulas bulleted by ∧ or ∨ denotes their conjunction or disjunction; ∧ and ∨ are also used as ordinary infix operators.

Init_{C}  =^{Δ}

∧ out ∈ {0, 1}

∧ in = [i ∈ {1, …, n} ↦ out]

Input(i) =^{Δ} ∧ in[i] = out

∧ in′ = [in except ![i] = 1 − in[i] ] ∧ out′ = out

Output =^{Δ}

∧ ∀i ∈ {1, …, n} : in[i] ≠ out

∧ out′ = 1 − out

∧ in′ = in

Next  =^{Δ} Output ∨ ∃ i ∈ {1, …, n} : Input(i)
Π_{C}  =^{Δ} Init_{C} ∧ □[Next]_{⟨in,out⟩} ∧ WF_{⟨in,out⟩}(Output)

Fig. 4. A TLA specification of an n-input C-element.

Next An action that is the disjunction of Output and all the Input(i) actions, for i ∈ {1, …, n}. Thus, a Next step is either an Output step or an Input(i) step for some input line i.

Π_{C} A temporal formula that is the specification of the C-element (together with its environment). It asserts that (i) Init_{C} holds initially, (ii) every step is either a Next step or else leaves ⟨in, out⟩ unchanged, and (iii) Output cannot be enabled forever without an Output step occurring. The fairness condition (iii) requires the output to change if all the inputs have; inputs are not required to change. (Since predicate-action diagrams describe only safety properties, the fairness condition is irrelevant to our explanation of the diagrams.)

The specification Π_{C} is short and precise. However, it is not as reader-friendly as a predicate-action diagram. We therefore use diagrams to help explain the specification, beginning with the predicate-action diagram of Figure 5. It is a diagram of the state function ⟨in[i], out⟩, meaning that it describes transitions that change ⟨in[i], out⟩. It is a diagram for the formula Π_{C}, meaning that it represents a formula that is implied by Π_{C}. The diagram shows the synchronization between the C-element’s ith input and its output.

We can draw many different predicate-action diagrams

[figure: \begin{matrix}∧ in[i] = & 0 \\ ∧ out = & 0 \end{matrix}; \begin{matrix}∧ in[i] = & 1 \\ ∧ out = & 0 \end{matrix}; \begin{matrix}∧ in[i] = & 1 \\ ∧ out = & 1 \end{matrix}; \begin{matrix}∧ in[i] = & 0 \\ ∧ out = & 1 \end{matrix}]

Fig. 5. A predicate-action diagram of ⟨in[i], out⟩ for the specification Π_{C} of an n-input C-element, where 1 ≤ i ≤ n.

[figure: in[i] = out; in[i] ≠ out]

Fig. 6. Another predicate-action diagram of ⟨in[i], out⟩ for Π_{C}, where 1 ≤ i ≤ n.

for the same specification. Figure 6 shows another diagram of ⟨in[i], out⟩ for Π_{C}. It is simpler than the one in Figure 5, but it contains less information. It does not indicate that the values of in[i] and out are always 0 or 1, and it does not show which variable is changed by each transition. The latter information is added in the diagram of Figure 7(a), where each transition is labeled with an action. The label Input(i) on the left-to-right arrow indicates that a transition from a state satisfying in[i] = out to a state satisfying in[i] ≠ out is an Input(i) step. This diagram represents the TLA formula of Figure 7(b).

Even more information is conveyed by a predicate-action diagram of ⟨in, out⟩, which also shows transitions that leave in[i] and out unchanged but change in[j] for some j ≠ i. Such a diagram is drawn in Figure 8(a). Figure 8(b) gives the corresponding TLA formula.

There are innumerable predicate-action diagrams that can be drawn for a specification. Figure 9 shows yet another diagram for the C-element specification Π_{C}. Since we are not relying on these diagrams as our specification, but simply to help explain the specification, we can show as much or as little information in them as we wish. We can

(a) A predicate-action diagram of ⟨in[i], out⟩.

[figure: in[i] = out; in[i] ≠ out; Input(i); Output]

(b) The corresponding TLA formula.

∧ in[i] = out

∧ □[(in[i] = out) ⇒ Input(i) ∧ (in′[i] ≠ out′)]_{⟨in[i],out⟩} ∧ □[(in[i] ≠ out) ⇒ Output ∧ (in′[i] = out′)]_{⟨in[i],out⟩}

Fig. 7. A more informative predicate-action diagram of ⟨in[i], out⟩ for Π_{C}, and the corresponding TLA formula.

(a) A predicate-action diagram of ⟨in, out⟩.

[figure: in[i] = out; in[i] ≠ out; Input(i); Output; ∃ j ≠ i : Input(j); ∃ j ≠ i : Input(j)]

(b) The corresponding TLA formula.

∧ in[i] = out

∧ □ [\begin{matrix}(in[i] = out) ⇒ \\ ( & ∨ Input(i) ∧ (in′[i] ≠ out′) ∨ (∃ j ≠ i : Input(j)) ∧ (in′[i] = out′) & ) \end{matrix}]_{⟨in,out⟩}

∧ □ [\begin{matrix}(in[i] ≠ out) ⇒ \\ ( & ∨ Output ∧ (in′[i] = out′) ∨ (∃ j ≠ i : Input(j)) ∧ (in′[i] ≠ out′) & ) \end{matrix}]_{⟨in,out⟩}

Fig. 8. A predicate-action diagram of ⟨in, out⟩ for Π_{C}, and the corresponding TLA formula, where 1 ≤ i ≤ n.

[figure: in[i] = out; in[i] ≠ out; in′[i] = 1 − in[i]; out′ = 1 − out]

Fig. 9. Yet another predicate-action diagram of ⟨in, out⟩ for Π_{C}.

draw multiple diagrams to illustrate different aspects of a system. Actual specifications are written as TLA formulas, which are much more expressive than pictures.

B. A Formal Treatment

B.1 Definition

We first define precisely the TLA formula represented by a diagram. Formally, a predicate-action diagram consists of a directed graph, with a subset of the nodes identified as initial nodes, where each node is labeled by a state predicate and each edge is labeled by an action. We assume a given diagram of a state function v and introduce the following notation.

N The set of nodes.

I The set of initial nodes.

E(n) The set of edges originating at node n.

d(e) The destination node of edge e. P_{n} The predicate labeling node n. E_{e} The action labeling edge e.

The formula Δ represented by the diagram is defined as follows.

Init_{Δ} =^{Δ} ∃ n ∈ I : P_{n}
A_{n}  =^{Δ} ∃ e ∈ E(n) : E_{e} ∧ P′_{d(e)}
Δ  =^{Δ} Init_{Δ} ∧ ∀n ∈ N : □[P_{n} ⇒ A_{n}]_{v}

When no explicit label is attached to an edge e, we take E_{e} to be true. When no set of initial nodes is explicitly indicated, we take I to be N. With the usual convention for quantification over an empty set, A_{n} is defined to equal false if there are no edges originating at node n.

B.2 Another Interpretation

Another possible interpretation of the predicate-action diagram is the formula Δ̂, defined by

Δ̂ =^{Δ} Init_{Δ} ∧ □[∃ n ∈ N : P_{n} ∧ A_{n}]_{v}

This is perhaps a more obvious interpretation—especially if the diagram is viewed as a description of a next-state relation. We now show that Δ always implies Δ̂, and that the converse implication holds if the predicates labeling the nodes are disjoint.

(A) Δ implies Δ̂. Proof : A simple invariance proof, using rule INV1 of [3, Figure 5, page 888], shows that Δ implies □(∃ n ∈ N : P_{n}). We then have:

Δ =^{Δ} Init_{Δ} ∧ ∀ n ∈ N : □[P_{n} ⇒ A_{n}]_{v}
≡ \begin{matrix}Init_{Δ} ∧ □([∃ n ∈ N : P_{n}]_{v}) \\ ∧ ∀ n ∈ N : □[P_{n} ⇒ A_{n}]_{v} \end{matrix}

[ because Δ implies □(∃ n ∈ N : P_{n}) ]

≡ Init_{Δ} ∧ □[\begin{matrix}(∃ n ∈ N : P_{n}) \\ ∧ ∀ n ∈ N : (P_{n} ⇒ A_{n})]_{v} \end{matrix}

[ because □ distributes over conjunction and ∀, and [X]_{v} ∧ ∀n ∈ N : [Y_{n}]_{v} is equivalent to [X ∧ ∀n ∈ N : Y_{n}]_{v} ]

⇒ Init_{Δ} ∧ □[∃ n ∈ N : P_{n} ∧ A_{n}]_{v}

[ by predicate logic, since B ⇒ C implies □[B]_{v} ⇒ □[C]_{v} ]

=^{Δ}  Δ̂

(B) If ¬(P_{m} ∧P_{n}) holds for all m, n in N with m ≠ n, then Δ̂ implies Δ. Proof : By propositional logic, the hypothesis implies

(∃ n ∈ N : P_{n} ∧ A_{n}) ⇒ (∀ n ∈ N : P_{n} ⇒ A_{n})

The result then follows from simple temporal reasoning, essentially by the reverse of the string of equivalences and implication used to prove (A).

We usually label the nodes of a predicate-action diagram with disjoint predicates, in which case (A) and (B) imply that the interpretations Δ and Δ̂ are equivalent. Diagrams with nondisjoint node labels may occasionally be useful; Δ is the more convenient interpretation of such diagrams.

C. Proving a Predicate-Action Diagram

Saying that a diagram is a predicate-action diagram for a specification Π asserts that Π implies the formula Δ represented by the diagram. Formula Π will usually have the form Init_{Π} ∧ □[M]_{u} ∧ L, where L is a fairness condition. Formula Δ equals Init_{Δ} ∧ ∀n ∈ N : □[P_{n} ⇒ A_{n}]_{v}. To prove Π ⇒ Δ, we prove:

1. Init_{Π} ⇒ Init_{Δ}

2. Init_{Π} ∧ □[M]_{u} ⇒ □[P_{n} ⇒ A_{n}]_{v}, for each node n.

The first condition is an assertion about predicates; it is generally easy to prove. To prove the second condition, one usually finds an invariant Inv such that Init_{Π} ∧ □[M]_{u} implies □Inv, so Π implies □[M ∧ Inv]_{u}. The second condition is then proved by showing that [M ∧ Inv]_{u} implies [P_{n} ⇒ A_{n}]_{v}, for each node n. Usually, u and v are tuples and every component of v is a component of u, so u′ = u implies v′ = v. In this case, one need show only that M∧Inv implies [P_{n} ⇒ A_{n}]_{v}, for each n. By definition of A_{n}, this means proving

P_{n} ∧ M ∧ Inv ⇒ (∃ m ∈ E(n) : E_{m} ∧ P′_{d(m)}) ∨ (v′ = v)

for each node n. This formula asserts that an M step that starts with P_{n} and Inv true and changes v is an E_{m} step that ends in a state satisfying P_{d(m)}, for some edge m originating at node n.

IV. Illustrating Proofs

In TLA, there is no distinction between a specification and a property; they are both formulas. Verification means proving that one formula implies another. A practical, relatively complete set of rules for proving such implications is described in [3]. We show here how predicate-action diagrams can be used to illustrate these proofs. We take as our example the same one treated in [3], that the specification Ψ defined in Section IV-A below implies the specification Φ defined in Section II above.

A. Another Specification

We define a TLA formula Ψ describing a program with two processes, each of which repeatedly loops through the sequence of operations P (sem); increment; V (sem), where one process increments x by one and the other increments y by one. Here, P (sem) and V (sem) denote the usual operations on a semaphore sem. To describe this program formally, we introduce a variable pc that indicates the control state. Each process has three control points, which we call “a”, “b”, and “g”. (Quotes indicate string values.)

We motivate the definition of Ψ with the three predicateaction diagrams for Ψ in Figure 10. In these diagrams, the predicate PC (p, q) asserts that control is at p in process 1 and at q in process 2. Figure 10(a) shows how the control state changes when the P (sem), V (sem), and increment actions are performed. Variables other than pc not mentioned in an edge label are left unchanged by the indicated steps—for example, steps described by the edge labeled x′ = x + 1 leave y and sem unchanged—but this is not asserted by the diagram. The next-state action N is written as the disjunction N_{1} ∨ N_{2} of the next-state actions of each process; and each N_{i} is written as the disjunction α_{i} ∨ β_{i} ∨ γ_{i}. Figure 10(b) illustrates this decomposition. Finally, the predicate-action diagram of Figure 10(c) describes how the semaphore variable sem changes.

To write the specification Ψ, we let pc be a function with domain {1, 2}, with pc[i] indicating where control resides in process i. The formula PC (p, q) can then be defined by

PC (p, q) =^{Δ} (pc[1] = p) ∧ (pc[2] = q)

(a)

[figure: PC (“a”, “a”); PC (“b”, “a”); PC (“a”, “b”); PC (“g”, “a”); PC (“a”, “g”); x′ = x + 1; P (sem); V (sem); y′ = y + 1; P (sem); V (sem)]

(b)

[figure: PC (“a”, “a”); PC (“b”, “a”); PC (“a”, “b”); PC (“g”, “a”); PC (“a”, “g”); β_{1}; α_{1}; γ_{1}; β_{2}; α_{2}; γ_{2}]

(c)

[figure: sem = 1; sem = 0; α_{1} ∨ α_{2}; γ_{1} ∨ γ_{2}; β_{1} ∨ β_{2}]

Fig. 10. Three predicate-action diagrams of ⟨x, y, pc, sem⟩ for Ψ.

The semaphore actions P and V are defined by

P (sem) =^{Δ} ∧ 0 < sem ∧ sem′ = sem − 1

V (sem) =^{Δ} sem′ = sem + 1

Missing from Figure 10 are a specification of the initial values of x and y, which we take to be zero, and a fairness condition. One could augment predicate-action diagrams with some notation for indicating fairness conditions. However, the conditions that are easy to represent with a diagram are not expressive enough to describe the variety of fairness requirements that arise in practice. The WF and SF formulas, which are expressive enough, are not easy to represent graphically. So, we have not attempted to represent fairness in our diagrams. We take as the fairness condition for our specification Ψ strong fairness on the next-state action N_{i} of each process. The complete definition of Ψ appears in Figure 11.

B. An Illustrated Proof

The proof of Ψ ⇒ Φ is broken into the proof of three conditions:

1. Init_{Ψ} ⇒ Init_{Φ}

2. Init_{Ψ} ∧ □[N]_{w} ⇒ □[M]_{⟨x,y⟩}

3. Ψ ⇒ WF_{⟨x,y⟩}(M_{i}), for i = 1, 2 We illustrate the proofs of conditions 2 and 3 with the predicate-action diagram of ⟨x, y, sem, pc⟩ for Ψ in Figure 12, where Q is defined by

Q_{i}(p, q) =^{Δ} ∧ PC (p, q) ∧ sem = i ∧ (x ∈ Nat) ∧ (y ∈ Nat)

and Nat is the set of natural numbers.

First, we must show that the diagram in Figure 12 is a predicate-action diagram for Ψ. This is easy using the definition in Section III-B.1; no invariant is needed. For example, the condition to be proved for the node labeled Q_{0}(“b”, “a”) is that an N step that starts with Q_{0}(“b”, “a”) true is an M_{1} step (one that increments x and leaves y unchanged) that makes Q_{0}(“g”, “a”) true. This follows easily from the definitions of Q and N, since an N step starting with PC (“b”, “a”) true must be a β_{1} step.

To prove condition 2, it suffices to prove that every step allowed by the diagram of Figure 12 is a [M]_{⟨x,y⟩} step. The steps not shown explicitly by the diagram are ones that leave w unchanged. Such steps leave ⟨x, y⟩ unchanged, so they are [M]_{⟨x,y⟩} steps. The actions labeling all the edges of the diagram imply [M]_{⟨x,y⟩}, so all the steps shown ex-

Init_{Ψ} =^{Δ} \begin{matrix}∧ pc = [i ∈ \{1, 2\} ↦ “a”] \\ ∧ (x = 0) ∧ (y = 0) \\ ∧ sem = 1 \end{matrix}

α_{i} =^{Δ} ∧ (pc[i] = “a”) ∧ (0 < sem) ∧ pc′ = [pc except ![i] = “b”] ∧ sem′ = sem − 1 ∧ ⟨x, y⟩′ = ⟨x, y⟩

γ_{i} =^{Δ} ∧ pc[i] = “g” ∧ pc′ = [pc except ![i] = “a”] ∧ sem′ = sem + 1 ∧ ⟨x, y⟩′ = ⟨x, y⟩

β_{1} =^{Δ} ∧ pc[1] = “b” ∧ pc′ = [pc except ![1] = “g”] ∧ x′ = x + 1 ∧ ⟨y, sem⟩′ = ⟨y, sem⟩

β_{2} =^{Δ} ∧ pc[2] = “b” ∧ pc′ = [pc except ![2] = “g”] ∧ y′ = y + 1 ∧ ⟨x, sem⟩′ = ⟨x, sem⟩

N_{i} =^{Δ} α_{i} ∨ β_{i} ∨ γ_{i}

N =^{Δ} N_{1} ∨ N_{2}

w =^{Δ} ⟨x, y, sem, pc⟩

Ψ =^{Δ} Init_{Ψ} ∧ □[N]_{w} ∧ SF_{w}(N_{1}) ∧ SF_{w}(N_{2})

Fig. 11. The specification Ψ.

[figure: Q_{1}(“a”, “a”); Q_{0}(“b”, “a”); Q_{0}(“a”, “b”); Q_{0}(“g”, “a”); Q_{0}(“a”, “g”); M_{1}; ⟨x, y⟩′ = ⟨x, y⟩; ⟨x, y⟩′ = ⟨x, y⟩; M_{2}; ⟨x, y⟩′ = ⟨x, y⟩; ⟨x, y⟩′ = ⟨x, y⟩]

Fig. 12. Another predicate-action diagram of ⟨x, y, sem, pc⟩ for Ψ.

plicitly by the diagram are also [M]_{⟨x,y⟩} steps. This proves condition 2.

We now sketch the proof of condition 3. To prove WF_{⟨x,y⟩}(M_{i}), it suffices to show that infinitely many ⟨M_{i}⟩_{⟨x,y⟩} steps occur. We first observe that each of the predicates labeling a node in the diagram implies that either ⟨N_{1}⟩_{w} or ⟨N_{2}⟩_{w} is enabled. The fairness condition of Ψ then implies that a behavior cannot remain forever at any node, but must keep moving through the diagram. Hence, the behavior must infinitely often pass through the Q_{1}(“a”, “a”) node. The predicate Q_{1}(“a”, “a”) implies that both ⟨N_{1}⟩_{w} and ⟨N_{2}⟩_{w} are enabled. Hence, the fairness condition SF_{w}(N_{1}) ∧ SF_{w}(N_{2}) implies that infinitely many ⟨N_{1}⟩_{w} steps and infinitely many ⟨N_{2}⟩_{w} steps must occur. Action ⟨N_{1}⟩_{w} is enabled only in the three nodes of the top loop. Taking infinitely many ⟨N_{1}⟩_{w} steps is therefore possible only by going around the top loop infinitely many times, which implies that infinitely many M_{1} steps occur, each starting in a state with Q_{0}(“b”, “a”) true. Since Q_{0}(“b”, “a”) implies x ∈ Nat, an M_{1} step starting with Q_{0}(“b”, “a”) true changes x, so it is an ⟨M_{1}⟩_{⟨x,y⟩} step. Hence, infinitely many ⟨M_{1}⟩_{⟨x,y⟩} steps occur. Similarly, taking infinitely many ⟨N_{2}⟩_{w} steps implies that infinitely many ⟨M_{2}⟩_{⟨x,y⟩} steps occur. This completes the proof of condition 3.

Using the predicate-action diagram does not simplify the proof. If we were to make the argument given above rigorous, we would go through precisely the same steps as in the proof described in [3]. However, the diagram does allow us to visualize the proof, which can help us to understand it.

V. Conclusion

We have described three uses of diagrams that we believe are new for diagrams with a precise formal semantics:

• To describe particular aspects of a complex specification with a simple diagram. An n-input C-element cannot be specified with a simple picture. However, we explained the specification with diagrams describing the synchronization between the output and each individual input.

• To provide complementary views of the same system. Diagrams (b) and (c) of Figure 10 look quite different, but they are diagrams for the same specification.

• To illustrate proofs. The disjunction of the predicates labeling the nodes in Figure 12 equals the invariant I of the proof in Section 7.2 of [3]. The diagram provides a graphical representation of the invariance proof. TLA differs from traditional specification methods in two important ways. First, all TLA specifications are interpreted over the same set of states. Instead of assigning values just to the variables that appear in the specification, a state assigns values to all of the infinite number of variables that can appear in any specification. Second, TLA specifications are invariant under stuttering. A formula can neither require nor rule out finite sequences of steps that do not change any variables mentioned in the formula. (The state-function subscripts in TLA formulas are there to guarantee invariance under stuttering.)

These two differences lead to two major differences between traditional state-transition diagrams and predicateaction diagrams. In traditional diagrams, each node represents a single state. Because states in TLA assign values to an infinite number of variables, it is impossible to describe a single state with a formula. Any formula can specify the values of only a finite number of variables. To draw diagrams of TLA formulas, we let each node represent a predicate, which describes a set of states. In traditional diagrams, every possible state change is indicated by an edge. Because TLA formulas are invariant under stuttering, we draw diagrams of particular state functions—usually tuples of variables.

TLA differs from most specification methods because it is a logic. It uses simple logical operations like implication and conjunction instead of more complicated automatabased notions of simulation and composition [6]. Everything we have done with predicate-action diagrams can be done with state-transition diagrams in any purely statebased formalism. However, conventional formalisms must use some notion of homomorphism between diagrams to describe what is expressed in TLA as logical implication.

Most formalisms employing state-transition diagrams are not purely state-based, but use both states and events. Nodes represent states, and edges describe input and output events. The meaning of a diagram is the sequence of events it allows; the states are effectively hidden. In TLA, there are only states, not events. Systems are described in terms of changes to interface variables rather than in terms of interface events. Variables describing the internal state are hidden with the existential quantifier ∃ ∃ ∃ ∃ ∃ ∃ described in [3]. Changes to any variable, whether internal or interface, can be indicated by node labels or edge labels. Hence, a purely state-based approach like TLA allows more flexibility in how diagrams are drawn than a method based on states and events.

References

[1] G. H. Mealy, “A method for synthesizing sequential circuits,” Bell System Technical Journal, vol. 34, pp. 1045–1079, Sept. 1955.

[2] E. F. Moore, “Gedanken-experiments on sequential machines,” in Automata Studies (C. E. Shannon and J. McCarthy, eds.), pp. 129–153, Princeton, New Jersey: Princeton University Press, 1956.

[3] L. Lamport, “The temporal logic of actions,” ACM Trans. Programming Languages and Systems, vol. 16, pp. 872–923, May 1994.

[4] B. Alpern and F. B. Schneider, “Defining liveness,” Information Processing Letters, vol. 21, pp. 181–185, Oct. 1985.

[5] C. Mead and L. Conway, Introduction to VLSI Systems, ch. 7. Reading, Massachusetts: Addison-Wesley, 1980.

[6] M. Abadi and L. Lamport, “Conjoining specifications,” Research Report 118, Digital Equipment Corporation, Systems Research Center, 1993. To appear in ACM Transactions on Programming Languages and Systems.

Leslie Lamport Leslie Lamport attended the Bronx High School of Science, where he took a course in mechanical drawing. He later received a Ph.D. in mathematics from Brandeis University, where he studied the propagation of singularities in the Cauchy problem for analytic partial differential equations. Since 1985, he has been a member of Digital Equipment Corporation’s Systems Research Laboratory, where he has written several biographical sketches.