Assignments in Apalache

Any run of Apalache requires an operator name as the value for the parameter --next (by default, this value is "Next"). We refer to this operator as the transition operator (or transition predicate).

Actions, Slices and Minimal Actions

Actions

In TLA+, an action is any Boolean-valued expression or operator, that contains primed variables (e.g. Next). For the sake of this definition, assume UNCHANGED x is just syntactic sugar for x' = x. Intuitively, actions are used to define the values of state variables after a transition, for example:

VARIABLE x
...

Next == x' = x + 1

The state transition described by Next is fairly obvious; if x has the value of 4 in the current state, it will have the value of 5 in any successor state. This brings us to the first natural requirement by Apalache: the transition operator must be an action.

Successor State Encodings

Unfortunately, the notion of an action is too broad to be a sufficient requirement for the transition operator. Consider this slight modification of the above example:

VARIABLE x, y (* new variable *)
...

Next == x' = x + 1

Just as in the first example, the expression x' = x + 1 is, by definition, an action. However, since the second example defines a state variable y, this action is no longer a sufficient description of a relation between a current state and a successor state; it does not determine a successor value y'. This brings us to the second requirement: the transition operator must allow Apalache to directly encode the relation between two successive states. This captures two sub-requirements: firstly, we disallow transition operators which fail to specify the value of one or more variables in the successor states, like the one in the example above. Secondly, we also disallow transition operators where the value of a successor state variable is determined only by implicit equations. Consider the following two cases:

VARIABLE y
...

A == y' = 1
B == y' * y' - 2 * y' + 1 = 0

Using some basic math, we see that action B can be equivalently written as (y' - 1)*(y' - 1) = 0, so it describes the exact same successor state, in which the new value of y is 1. What makes it different from action A is the fact that this is far from immediately obvious from the syntax. The fact that there happened to be a closed-form solution for which gave us an integer value for y', is a lucky coincidence, as B could have been, for example, y' * y' + 1 = 0, with no real roots. To avoid cases like this, we require that transition operators explicitly declare the values of state variables in successor states.

We call syntactic forms, which explicitly represent successor state values, assignment candidates. An assignment candidate for x is a TLA+ expression that has one of the following forms:

x' = e,
x' \in S,
UNCHANGED x, or
x' := e (note that := is the operator defined in Apalache.tla)

So to reformulate the second requirement: the transition operator must contain at least one assignment candidate for each variable declared in the specification.

Control Flow: Minimal and Compound Actions

When writing non-trivial specifications, authors often end up with something similar to the following:

EventA == ...
EventB == ...
...

Next == \/ EventA
        \/ EventB

Specifically, EventA and EventB often represent mutually exclusive possibilities of execution. Just like before, the basic definition of an action is not sufficient to explain the relation of EventA or EventB and Next; if EventA is an action and EventB is an action, then Next is also an action. To more accurately describe this scenario, we observe that the operator or ( \/) sometimes serves as a kind of parallel composition operator (||) in process algebra - it connects two (or more) actions into a larger one.

There are only two operators in TLA+ that could be considered control-flow operators in this way, the or (\/) operator and the if-then-else operator. We distinguish their uses as action- and as value operators:


A == x = 1 \/ x = 2 (* arguments are not actions *)
B == x' = 1 \/ x' = 2 (* arguments are actions *)

Simply put, if all arguments to an operator \/ are actions, then that operator is an action-or, otherwise it is a value-or. Similarly, if both the THEN _ and ELSE _ subexpressions of if-then-else are actions, it is an action-ITE, otherwise it is a value-ITE (in particular, a value-ITE can be non-Boolean).

Using these two operators we can define the following terms: A minimal action is an action which contains no action-or and no action-ITE. Conversely, a compound action is an action which contains at least one action-or or at least one action-ITE.

Slices

Given a transition operator, which is most commonly a compound action, we can decompose it into as many minimal actions as possible. We call this process slicing and the resulting minimal actions slices. This allows us to write transition operators in the following equivalent way:

Next == \/ Slice1
        \/ Slice2
        ...
        \/ SliceN

Where each Slice[i] is a minimal action.

The details of slicing are nuanced and depend on operators other than or (\/) and if-then-else, but we give two examples here:

If a formula A has the shape A1 \/ ... \/ An (where A1, ... An are actions), then a slice of A has the shape Si, where Si is a slice of some Ai.

If a formula A has the shape IF p THEN A1 ELSE A2 (where A1, A2 are actions), then a slice of A has the shape p /\ S1 or \neg p /\ S2, where S1 is a slice of A1 and S2 is a slice of S2.

Slices allow us to formulate the final requirement: the transition operator must be such, that we can select one assignment candidate for each variable in each of its slices (minimal actions) as an assignment. The process and conditions of selecting assignments from assignment candidates is described in the next section.

Assignments and Assignment Candidates

Recall, an assignment candidate for x is a TLA+ expression that has one of the following forms:

x' = e,
x' \in S,
UNCHANGED x, or
x' := e (note that := is the operator defined in Apalache.tla)

While a transition operator may contain multiple assignment candidates for the same variable, not all of them are chosen as assignments by Apalache. The subsections below describe how the assignments are selected.

Minimality

Assignments aren't spurious; each variable must have at least one assignment per transition operator, but no more than necessary to satisfy all of the additional constraints below (i.e. no more than one assignment per slice).

If all possible slices fail to assign one or more variables, an error, like the one below, is reported:

Assignment error: No assignments found for: x, z

Such errors are usually the result of adding a VARIABLE without any accompanying TLA+ code relating to it. The case where at least one transition, but not all of them, fails to assign a variable is shown below.

Syntax Order

For the purpose of evaluating assignments, Apalache considers the left-to-right syntax order of and-operator (/\) arguments. Therefore, as many assignments as possible are selected from the first (w.r.t. syntax order) argument of and (/\), then from the second, and so on.

Example:

Next == x' = 1 /\ x' = 2

In the above example, x' = 1 would be chosen as an assignment to x, over x' = 2.

Assignment-before-use Convention

If, in the syntax order defined above, an expression containing a primed variable x' syntactically precedes an assignment to x, the assignment finder throws an exception of the following shape:

Assignment error: test.tla:10:16-10:17: x' is used before it is assigned.

notifying the user of any variables used before assignment. In particular, right-hand-sides of assignment candidates ( e.g. x' + 2 in y' = x' + 2 )are subject to this restriction as well. Consider:

A == x' > 0 /\ x' = 1
B == y' = x' + 2 /\ x' = 1

In A, the expression x' > 0 precedes any assignment to x and in B, while y' = x' + 2 is an assignment candidate for y, it precedes any assignment to x, so both expressions are inadmissible (and would trigger exceptions).

Note that this only holds true if A (resp. B) is chosen as the transition operator. If A is called inside another transition operator, for example in Next == x' = 1 /\ A, no error is reported.

Balance

In cases of the or-operator (\/), all arguments must have assignments for the same set of variables. In particular, if one argument contains an assignment candidate and another does not, such as in this example:

\/ y = 1
\/ y' = 2

the assignment finder will report an error, like the one below:

Assignment error: test.tla:10:15-10:19: Missing assignments to: y

notifying the user of any variables for which assignments exist in some, but not all, arguments to \/. Note that if we correct and extend the above example to

/\ \/ y' = 1
   \/ y' = 2
/\ y' = 3

the assignments to y would be y' = 1 and y' = 2, but not y' = 3; minimality prevents us from selecting all three, the syntax order constraint forces us to select assignments in y' = 1 \/ y' = 2 before y' = 3 and balance requires that we select both y' = 1 and y' = 2. On the other hand, if we change the example to

/\ y' = 3
/\ \/ y = 1
   \/ y' = 2

the only assignment has to be y' = 3. While one of the disjuncts is an assignment candidate and the other is not, the balance requirement is not violated here, since neither disjunct is chosen as an assignment.

Similar rules apply to if-then-else: both the THEN _ and ELSE _ branch must assign the same variables, however, the IF _ condition is ignored when determining assignments.

Assignment-free Expressions

Not all expressions may contain assignments. While Apalache permits the use of all assignment candidates, except ones defined with :=(details here), inside other expressions, some of these candidates will never be chosen as assignments, based on the syntactic restrictions outlined below:

Given a transition operator A, based on the shape of A, the following holds:

If A has the shape A_1 /\ ... /\ A_n, then assignments are selected from A_1, ... , A_n sequentially, subject to the syntax-order rule.
If A has the shape A_1 \/ ... \/ A_n, then assignments are selected in all A_1, ... , A_n independently, subject to the balance rule.
If A has the shape IF p THEN A_1 ELSE A_2, then:
- p may not contain assignments. Any assignment candidates in p are subject to the assignment-before-use rule.
- Assignments are selected in both A_1 and A_n independently, subject to the balance rule.
If A has the shape \E x \in S: A_1, then:
- S may not contain assignments. Any assignment candidates in S are subject to the assignment-before-use rule.
- Assignments are selected in A_1
In any other case, A may not contain assignments, however, any assignment candidates in A are subject to the assignment-before-use rule.

Examples:

A == /\ x' = 2
     /\ \E s \in { t \in 1..10 : x' > t }: y' = s

Operator A contains assignments to both x and y; while x' > t uses x', it does not violate the assignment-before-use rule, since the assignment to x precedes the expression, w.r.t. syntax order.

(* INVALID *)
B == \E s \in { t \in 1..10 : x' > t }: y' = s

In operator B, the assignment to x is missing, therefore x' > t produces an error, as it violates assignment-before-use.

C == /\ x' = 1
     /\ IF x' = 0 /\ 2 \in {x', x' + 2, 0}
        THEN y' = 1
        ELSE y' = 2

The case in C is similar to A; conditions of the if-then-else operator may not contain assignments to x, so x' = 0 can never be one, but they may use x', since a preceding expression (x' = 1) qualifies as an assignment.

(* INVALID *)
D == IF x' = 0
     THEN y' = 1
     ELSE y' = 2

The operator D produces an error, for the same reason as B; even though x' = 0 is an assignment candidate, if-conditions are assignment-free, so x' = 0 cannot be chosen as an assignment to x.

(* INVALID *)
E == /\ x' = 2
     /\ \A s \in { t \in 1..10 : x' > t }: y' = s

Lastly, while E looks almost identical to A, the key difference is that expressions under universal quantifiers may not contain assignments. Therefore, y' = s is not an assignment to y and thus violates assignment-before-use.

Manual Assignments

Users may choose, but aren't required, to use manual assignments x' := e in place of x' = e. While the use of this operator does not change Apalache's internal search for assignments (in particular, using manual assignment annotations is not a way of circumventing the syntax order requirement), we encourage the use of manual assignments for clarity.

Unlike other shapes of assignment candidates, whenever a manual assignment is used in a position where the assignment candidate would not be chosen as an assignment (either within assignment-free expressions or in violation of, for example, the syntax order rule) an error, like one of the two below, is reported:

Assignment error: test.tla:10:12-10:18: Manual assignment is spurious, x is already assigned!

Assignment error: test.tla:10:15-10:21: Illegal assignment inside an assignment-free expression.

The benefit of using manual assignments, we believe, lies in synchronizing the user's and the tool's understanding of where assignments happen. This helps prevent unexpected results, where the user's expectations or intuition regarding assignment positions are incorrect.

Note: To use manual assignments where the assignment candidate has the shape of x' \in S use \E s \in S: x' := s.

Apalache Documentation