Here is a quick example of a top-level user operator (which has to be defined in a module) and of its application:
----------------------- MODULE QuickTopOperator ------------------------------- ... Abs(i) == IF i >= 0 THEN i ELSE -i ... B(k) == Abs(k) ===============================================================================
As you most probably guessed, the operator
Abs expects one argument
Given an integer
j, then the result of computing
Abs(j) is the absolute
j. The same applies, when
j is a natural number or a real number.
In general, operators of
n arguments are
defined as follows:
\* an operator without arguments (nullary) Opa0 == body_0 \* an operator of one argument (unary) Opa1(param1) == body_1 \* an operator of two arguments (binary) Opa2(param1, param2) == body_2 ...
In this form, the operator arguments are not allowed to be operators. If you want to receive an operator as an argument, see the syntax of Higher-order operators.
Here are concrete examples of operator definitions:
----------------------------- MODULE FandC ------------------------------------ EXTENDS Integers ... ABSOLUTE_ZERO_IN_CELCIUS == -273 Fahrenheit2Celcius(t) == (t - 32) * 10 / 18 Max(s, t) == IF s >= t THEN s ELSE t ... ===============================================================================
What is their arity (number of arguments)?
If you are used to imperative languages such as Python or Java, then you are
probably surprised that operator definitions do not have any
statement. The reason for that is simple: TLA+ is not executed on any hardware.
To understand how operators are evaluated, see the semantics below.
Having defined an operator, you can apply it inside another operator as follows (in a module):
----------------------------- MODULE FandC ------------------------------------ EXTENDS Integers VARIABLE fahrenheit, celcius \* skipping the definitions of \* ABSOLUTE_ZERO_IN_CELCIUS, Fahrenheit2Celcius, and Max ... UpdateCelcius(t) == celcius' = Max(ABSOLUTE_ZERO_IN_CELCIUS, Fahrenheit2Celcius(t)) Next == /\ fahrenheit' \in -1000..1000 /\ UpdateCelcius(fahrenheit') ... ===============================================================================
In the above example, you see examples of four operator applications:
The nullary operator
ABSOLUTE_ZERO_IN_CELCIUSis applied without any arguments, just by its name. Note how a nullary operator does not require parentheses
(). Yet another quirk of TLA+.
The one-argument operator Fahrenheit2Celcius is applied to
t, which is a parameter of the operator
The two-argument operator
Maxis applied to
The one-argument operator
UpdateCelciusis applied to
fahrenheit', which is the value of state variable
fahrenheitin the next state of the state machine. TLA+ has no problem applying the operator to
Technically, there are more than four operator applications in our example. However, all other operators are the standard operators. We do not focus on them here.
Note on the operator order. As you can see, we are applying operators after they have been defined in a module. This is a general rule in TLA+: A name can be only referred to, if it has been defined in the code before. TLA+ is not the first language to impose that rule. For instance, Pascal had it too.
Note on shadowing. TLA+ does not allow you to use the same name as an operator parameter, if it has been defined in the context of the operator definition. For instance, the following is not allowed:
-------------------------- MODULE NoShadowing --------------------------------- VARIABLE x \* the following operator definition produces a semantic error: \* the parameter x is shadowing the state variable x IsZero(x) == x = 0 ===============================================================================
There are a few tricky cases, where shadowing can actually happen, e.g., see
dir in SlidingPuzzles. However, we recommend to keep things
simple and avoid shadowing at all.
Precise treatment of operator application is given on page 320 of Specifying Systems. In a nutshell, operator application in TLA+ is a Call by macro expansion, though it is a bit smarter: It does not blindly mix names from the operator's body and its application context. For example, the following semantics by substitution is implemented in the Apalache model checker.
Here we give a simple explanation for non-recursive operators. Consider the
definition of an
A and its application in the definition
of another operator
A(p_1, ..., p_n) == body_of_A ... B(p_1, ..., p_k) == ... A(e_1, ..., e_n) ...
The following three steps allow us to replace application of the operator
- Change the names in the definition of
Ain such a way such they do not clash with the names in
B(as well as with other names that may be used in
B). This is the well-known technique of Alpha conversion in programming languages. This may also require renaming of the parameters
p_1, ..., p_n. Let the result of alpha conversion be the following operator:
uniq_A(uniq_p_1, ..., uniq_p_n) == body_of_uniq_A
Substitute the expression
A(e_1, ..., e_n)in the definition of
Substitute the names
uniq_p_1, ..., uniq_p_nwith the expressions
e_1, ..., e_n, respectively.
The above transformation is usually called Beta reduction.
Example. Let's go back to the module
FandC, which we considered above. By
applying the substitution approach several times, we transform
several steps as follows:
First, by substituting the body of
Next == /\ fahrenheit' \in -1000..1000 /\ celcius' = Max(ABSOLUTE_ZERO_IN_CELCIUS, Fahrenheit2Celcius(fahrenheit'))
Second, by substituting the body of
Next == /\ fahrenheit' \in -1000..1000 /\ celcius' = IF ABSOLUTE_ZERO_IN_CELCIUS >= Fahrenheit2Celcius(fahrenheit') THEN ABSOLUTE_ZERO_IN_CELCIUS ELSE Fahrenheit2Celcius(fahrenheit')
Third, by substituting the body of
Next == /\ fahrenheit' \in -1000..1000 /\ celcius' = IF ABSOLUTE_ZERO_IN_CELCIUS >= (fahrenheit' - 32) * 10 / 18 THEN ABSOLUTE_ZERO_IN_CELCIUS ELSE (fahrenheit' - 32) * 10 / 18
You could notice that we applied beta reduction syntactically from top to
bottom, like peeling an onion. We could do it in another direction: First
starting with the application of
Fahrenheit2Celcius. This actually does not
matter, as long as our goal is to produce a TLA+ expression that is free of
user-defined operators. For instance, Apalache applies Alpha conversion and
Beta reduction to remove user-defined operator and then translates the TLA+
expression to SMT.