Difficulty: Red trail – Medium
Author: Philip Offtermatt, 2022
In this tutorial, we will show how Apalache can be used to decide temporal
properties that are more general than invariants.
This tutorial will be most useful to you if you have a basic understanding of
linear temporal logic, e.g. the semantics of
See a writeup of temporal operators here.
Further, we assume you are familiar with TLA+, but expert knowledge is not necessary.
As a running example, the tutorial uses a simple example specification, modelling a devious nondeterministic traffic light.
The traffic light has two main components: A lamp which can be either red or green, and a button which can be pushed to request the traffic light to become green. Consequently, there are two variables: the current state of the light (either green or red), and whether the button has been pushed that requests the traffic light to switch from red to green.
The full specification of the traffic light is here:
But don't worry - we will dissect the spec in the following.
In the TLA specification, we declare two variables:
VARIABLES \* If true, the traffic light is green. If false, it is red. \* @type: Bool; isGreen, \* If true, the button has been pushed to request the light to become green, but the light has \* not become green since then. \* If false, the light has become green since the button has last been pushed \* or the button has never been pushed. \* @type: Bool; requestedGreen
Initially, the light is red and green has not yet been requested:
\* The light is initially red, and the button was not pressed. Init == /\ isGreen = FALSE /\ requestedGreen = FALSE
We have three possible actions:
- The traffic light can switch from red to green,
- The traffic light can switch from green to red, or
- The button can be pushed, thus requesting that the traffic light becomes green.
(* ---------------------- *) (* requesting green light *) \* The switch to green can only be requested when the light is not green, and \* the switch has not *already* been requested since the light last turned green. RequestGreen_Guard == /\ ~isGreen /\ ~requestedGreen RequestGreen_Effect == /\ requestedGreen' = TRUE /\ UNCHANGED << isGreen >> RequestGreen == RequestGreen_Guard /\ RequestGreen_Effect (* ---------------------- *) (* switching to red light *) \* The light can switch to red at any time if it is currently green. SwitchToRed_Guard == isGreen SwitchToRed_Effect == /\ isGreen' = FALSE /\ UNCHANGED << requestedGreen >> SwitchToRed == SwitchToRed_Guard /\ SwitchToRed_Effect (* ------------------------ *) (* switching to green light *) \* The light can switch to green if it is currently red, and \* the button to request the switch to green has been pressed. SwitchToGreen_Guard == /\ ~isGreen /\ requestedGreen SwitchToGreen_Effect == /\ isGreen' = TRUE /\ requestedGreen' = FALSE SwitchToGreen == SwitchToGreen_Guard /\ SwitchToGreen_Effect Next == \/ RequestGreen \/ SwitchToRed \/ SwitchToGreen
In the interest of simplicity, we'll assume that the button cannot be pushed when green is already requested, and that similarly it's not possible to push the button when the light is already green.
Now, we are ready to specify the properties that we are interested in. For example, when green is requested, at some point afterwards the light should actually turn green. We can write the property like this:
RequestWillBeFulfilled == (requestedGreen => <>isGreen)
Intuitively, the property says:
"Check that at all points in time (),
if right now,
RequestGreen is true,
then at some future point in time,
IsGreen is true."
Let's run Apalache to check this property:
apalache-mc check --temporal=RequestWillBeFulfilled TrafficLight.tla
... The outcome is: NoError Checker reports no error up to computation length 10 It took me 0 days 0 hours 0 min 2 sec Total time: 2.276 sec EXITCODE: OK
This is because our traffic watch is actually
If it is red and green has not been requested,
the only enabled action is
If it is red and green has been requested,
SwitchToGreen is enabled.
And finally, if the light is green,
SwitchToRed is enabled.
However, we want to make our traffic light more devious. We will allow the model to stutter, that is, just let time pass and take no action.
We can write a new next predicate that explicitly allows stuttering like this:
\* @type: <<Bool, Bool>>; vars == << isGreen, requestedGreen >> StutteringNext == [Next]_vars
[Next]_vars is shorthand for
Next \/ UNCHANGED vars. Now, let us try to verify the property once again,
using the modified next predicate:
apalache-mc check --next=StutteringNext \ --temporal=RequestWillBeFulfilled TrafficLight.tla
Step 2: picking a transition out of 3 transition(s) I@18:04:16.132 State 3: Checking 1 state invariants I@18:04:16.150 State 3: Checking 1 state invariants I@18:04:16.164 State 3: Checking 1 state invariants I@18:04:16.175 State 3: Checking 1 state invariants I@18:04:16.186 Check an example state in: /home/user/apalache/docs/src/tutorials/_apalache-out/TrafficLight.tla/2022-05-30T18-04-13_3349613574715319837/counterexample1.tla, /home/user/apalache/docs/src/tutorials/_apalache-out/TrafficLight.tla/2022-05-30T18-04-13_3349613574715319837/MC1.out, /home/user/apalache/docs/src/tutorials/_apalache-out/TrafficLight.tla/2022-05-30T18-04-13_3349613574715319837/counterexample1.json, /home/user/apalache/docs/src/tutorials/_apalache-out/TrafficLight.tla/2022-05-30T18-04-13_3349613574715319837/counterexample1.itf.json E@18:04:16.346 State 3: state invariant 0 violated. E@18:04:16.346 Found 1 error(s) I@18:04:16.347 The outcome is: Error I@18:04:16.353 Checker has found an error I@18:04:16.354 It took me 0 days 0 hours 0 min 2 sec I@18:04:16.354 Total time: 2.542 sec I@18:04:16.354
This time, we get a counterexample.
Let's take a look at
Let's first focus on the initial state.
(* Initial state *) (* State0 == RequestWillBeFulfilled_init = FALSE /\ __loop_InLoop = FALSE /\ __loop_☐(requestedGreen ⇒ ♢isGreen) = FALSE /\ __loop_requestedGreen ⇒ ♢isGreen = TRUE /\ __loop_♢isGreen = FALSE /\ __loop_isGreen = FALSE /\ __loop_requestedGreen = FALSE /\ ☐(requestedGreen ⇒ ♢isGreen) = FALSE /\ ☐(requestedGreen ⇒ ♢isGreen)_unroll = TRUE /\ requestedGreen ⇒ ♢isGreen = TRUE /\ ♢isGreen = FALSE /\ ♢isGreen_unroll = FALSE /\ isGreen = FALSE /\ requestedGreen = FALSE *) State0 == RequestWillBeFulfilled_init = FALSE /\ __loop_InLoop = FALSE /\ __loop___temporal_t_1 = FALSE /\ __loop___temporal_t_2 = TRUE /\ __loop___temporal_t_3 = FALSE /\ __loop_isGreen = FALSE /\ __loop_requestedGreen = FALSE /\ __temporal_t_1 = FALSE /\ __temporal_t_1_unroll = TRUE /\ __temporal_t_2 = TRUE /\ __temporal_t_3 = FALSE /\ __temporal_t_3_unroll = FALSE /\ isGreen = FALSE /\ requestedGreen = FALSE
Two things are notable:
- The initial state formula appears twice, once as a comment and once in TLA+.
- There are way more variables than the two variables we specified.
The comment and the TLA+ specification express the same state, but in the comment, some variable names from the encoding have been replaced
with more human-readable names.
For example, there is a variable called
☐(requestedGreen ⇒ ♢isGreen) in the comment,
which is called
__temporal_t_1 in TLA+.
In the following, let's focus on the content of the comment, since it's easier to understand what's going on.
There are many additional variables in the counterexample because to check temporal formulas, Apalache uses an encoding that transforms temporal properties to invariants. If you are interested in the technical details, the encoding is described in sections 3.2 and 4 of Biere et al.. However, to understand the counterexample, you don't need to go into the technical details of the encoding. We'll go explain the counterexample in the following.
We will talk about traces in the following. You can find more information about (symbolic) traces here. For the purpose of this tutorial, however, it will be enough to think of a trace as a sequence of states that were encountered by Apalache, and that demonstrate a violation of the property that is checked.
First, it's important to know that for finite-state systems, counterexamples to temporal properties are traces ending in a loop, which we'll call lassos in the following. If you want to learn more about why this is the case, have a look at the book on model checking.
A loop is a partial trace that starts and ends with the same state. A lasso is made up of two parts: A prefix, followed by a loop. It describes a possible infinite execution: first it goes through the prefix, and then repeats the loop forever.
For example, what is a trace that is a counterexample to the property
It's an execution that loops without ever finding a state that satisfies
For example, a counterexample trace might visually look like this:
In contrast, as long as the model checking engine has not found a lasso, there may still exist some future state satisfying
The encoding for temporal properties involves lots of auxiliary variables. While some can be very helpful to understand counterexamples, many are mostly noise.
Let's first understand how Apalache can identify lassos using auxiliary variables.
The auxiliary variable
__loop_InLoop is true in exactly the states belonging to the loop.
Additionally, at the first state of the loop, i.e., when
__loop_InLoop switches from false to true,
we store the valuation of each variable in a shadow copy whose name is prefixed by
Before the first state of the loop, the
__loop_ carry arbitrary values.
In our example, it looks like this:
(* State0 == ... /\ __loop_InLoop = FALSE ... /\ __loop_isGreen = FALSE /\ __loop_requestedGreen = FALSE ... /\ isGreen = FALSE /\ requestedGreen = FALSE *) (* State1 == ... /\ __loop_InLoop = FALSE ... /\ __loop_isGreen = FALSE /\ __loop_requestedGreen = FALSE ... /\ isGreen = FALSE /\ requestedGreen = TRUE *) (* State2 == ... /\ __loop_InLoop = FALSE ... /\ __loop_isGreen = FALSE /\ __loop_requestedGreen = FALSE ... /\ isGreen = FALSE /\ requestedGreen = TRUE *) (* State3 == ... /\ __loop_InLoop = TRUE ... /\ __loop_isGreen = FALSE /\ __loop_requestedGreen = TRUE ... /\ isGreen = FALSE /\ requestedGreen = TRUE *)
requestedGreen are both false.
__loop_InLoop is false, and the copies of
requestedGreen, which are called
__loop_requestedGreen, are equal to the values of
From state 0 to state 1,
requestedGreen changes from false to true.
From state 1 to state 2, the system stutters, and the valuation of model variables remains unchanged.
Finally, in state 3
__loop_InLoop is set to true, which means that
the loop starts in state 2, and the trace from state 3 onward is inside the loop.
However, since state 3 is the last state, this means simply that the trace loops in state 2.
Since the loop starts, the copies of the system variables are also set to the values of the variables in state 2,
__loop_isGreen = FALSE and
__loop_requestedGreen = TRUE.
The lasso in this case can be visualized like this:
It is also clear why this trace violates the property:
requestedGreen holds in state 1, but
isGreen never holds,
so in state 1 the property
requestedGreen => <>isGreen is violated.
Next, let us discuss the other auxiliary variables that are introduced by Apalache to check the temporal property. These extra variables correspond to parts of the temporal property we want to check. These are the following variables with their valuations in the initial state:
(* State0 == RequestWillBeFulfilled_init = FALSE ... /\ ☐(requestedGreen ⇒ ♢isGreen) = FALSE /\ ☐(requestedGreen ⇒ ♢isGreen)_unroll = TRUE /\ requestedGreen ⇒ ♢isGreen = TRUE /\ ♢isGreen = FALSE /\ ♢isGreen_unroll = FALSE ...
There are three groups of variables:
- Variables that look like formulas, e.g.
☐(requestedGreen ⇒ ♢isGreen)
- Variables that look like formulas and end with
☐(requestedGreen ⇒ ♢isGreen)_unroll
- The variable
Let's focus on the non-
_unroll variables that look like formulas
Recall that the temporal property we want to check is
(requestedGreen => <>isGreen).
That's also the name of one of the variables: The value of the variable
☐(requestedGreen ⇒ ♢isGreen) tells us whether starting in the current state, the
(requestedGreen => <>isGreen) holds. Since we are looking at a counterexample to this formula, it is not
surprising that the formula does not hold in the initial state of the counterexample.
Similarly, the variable
requestedGreen ⇒ ♢isGreen tells us whether
requestedGreen ⇒ ♢isGreen holds at the current state.
It might be surprising to see that the property holds
but recall that in state 0,
requestedGreen = FALSE, so the implication is satisfied.
Finally, we have the variable
♢isGreen, which is false, telling
us that along the execution,
isGreen will never be true.
You might already have noticed the pattern of which formulas appear as variables.
Take our property
(requestedGreen => <>isGreen).
The syntax tree of this formula looks like this:
For each node of the syntax tree where the formula contains a temporal operator,
there is an auxiliary variable.
For example, there would be auxiliary variables for the formulas
(<>isGreen) /\ (requestedGreen), but not for the formula
isGreen /\ requestedGreen.
As mentioned before, the value of an auxiliary variable in a state tells us whether from that state, the corresponding subformula is true. In this particular example, the formulas that correspond to variables in the encoding are filled with orange in the syntax tree.
What about the
_unroll variables? There is one
_unroll variable for each immediate application of a temporal operator in the formula.
☐(requestedGreen ⇒ ♢isGreen)_unroll is the unroll-variable for the
leading box operator.
To illustrate why these are necessary, consider the formula
isGreen. To decide whether this formula holds in the last state of the loop, the algorithm needs to know whether
isGreen holds in all states of the loop. So it needs to store this information when it traverses the loop.
That's why there is an extra variable, which stores whether
isGreen holds on all states of the loop, and Apalache can access this information when it explores the last state of the loop.
Similarly, the unroll-variable
♢isGreen_unroll holds true
if there is a state on the loop such that
isGreen is true.
Let us take a look at the valuations of
☐(requestedGreen ⇒ ♢isGreen)_unroll along our counterexample to see this.
(* State0 == ... /\ __loop_InLoop = FALSE ... /\ ☐(requestedGreen ⇒ ♢isGreen) = FALSE /\ ☐(requestedGreen ⇒ ♢isGreen)_unroll = TRUE ... (* State1 == ... /\ __loop_InLoop = FALSE ... /\ ☐(requestedGreen ⇒ ♢isGreen) = FALSE /\ ☐(requestedGreen ⇒ ♢isGreen)_unroll = TRUE ... (* State2 == ... /\ __loop_InLoop = FALSE ... /\ ☐(requestedGreen ⇒ ♢isGreen) = FALSE /\ ☐(requestedGreen ⇒ ♢isGreen)_unroll = TRUE ... (* State3 == ... /\ __loop_InLoop = TRUE ... /\ ☐(requestedGreen ⇒ ♢isGreen) = FALSE /\ ☐(requestedGreen ⇒ ♢isGreen)_unroll = FALSE ...
So in the last state,
☐(requestedGreen ⇒ ♢isGreen)_unroll
is not true, since
☐(requestedGreen ⇒ ♢isGreen)
does not hold in state 2, which is on the loop.
Similar to the
__loop_ copies for model variables,
we also introduce copies for all (temporal) subformulas, e.g.,
__loop_☐(requestedGreen ⇒ ♢isGreen) for
☐(requestedGreen ⇒ ♢isGreen).
These fulfill the same function as the
__loop_ copies for the
original variables of the model, i.e., retaining the state of variables from the first state of the loop, e.g.,
(* State0 == ... /\ __loop_☐(requestedGreen ⇒ ♢isGreen) = FALSE /\ __loop_requestedGreen ⇒ ♢isGreen = TRUE /\ __loop_♢isGreen = FALSE /\ __loop_isGreen = FALSE /\ __loop_requestedGreen = FALSE
Finally, let's discuss
This variable is an artifact of the translation for temporal properties.
Intuitively, in any state, the variable will be true if the variable encoding the formula
is true in the first state.
A trace is a counterexample if
RequestWillBeFulfilled is false in the first state, so
RequestWillBeFulfilled_init is false,
and a loop satisfying requirements on the auxiliary variables is found.
In this tutorial, we learned how to specify temporal properties in Apalache, and how to read counterexamples for such properties.
If you want to dive deeper into the encoding, it is formally explained in sections 3.2 and 4 of Biere et al.. To understand why this encoding was chosen, you can read the ADR on temporal properties. Finally, if you want to go into the nitty-gritty details and see the encoding in action, you can look at the intermediate TLA specifying the encoding.
apalache-mc check --next=StutteringNext \ --write-intermediate=yes --temporal=RequestWillBeFulfilled TrafficLight.tla
You will get intermediate output in a folder named like
There, take a look at