Enumerating counterexamples

By default, Apalache stops whenever it finds a property violation. This is true for the commands that are explained in the Section on Running the Tool. Sometimes, we want to produce multiple counterexamples; for instance, to generate multiple tests.

Consider the following TLA+ specification:

---- MODULE View2 ----
EXTENDS Integers
VARIABLES
    \* @type: Int;
    x

Init ==
  x = 0

A ==
  x' = x + 1

B ==
  x' = x - 1

C ==
  x' = x

Next ==
  A \/ B \/ C

Inv ==
  x = 0

We can run Apalache to check the state invariant Inv:

$ apalache check --inv=Inv View2.tla

Apalache quickly finds a counterexample that looks like this:

...
(* Initial state *)
State0 == x = 0

(* Transition 0 to State1 *)
State1 == x = 1
...

Producing multiple counterexamples. If we want to see more examples of invariant violation, we can ask Apalache to produce up to 50 counterexamples:

$ apalache check --inv=Inv --max-error=50 View2.tla
...
Found 20 error(s)
...

Whenever the model checker finds an invariant violation, it reports a counterexample to the current symbolic execution and proceeds with the next action. For instance, if the symbolic execution Init \cdot A \cdot A has a concrete execution that violates the invariant Inv, the model checker would print this execution and proceed with the symbolic execution Init \cdot A \cdot B. That is why the model checker stops after producing 20 counterexamples.

The option --max-error is similar to the option --continue in TLC, see TLC options. However, the space of counterexamples in Apalache may be infinite, e.g., when we have integer variables, so --max-error requires an upper bound on the number of counterexamples.

Partitioning counterexamples with view abstraction. Some of the produced counterexamples are not really interesting. For instance, counterexample5.tla looks like follows:

(* Initial state *)
State0 == x = 0

(* Transition 1 to State1 *)
State1 == x = -1

(* Transition 1 to State2 *)
State2 == x = -2

(* Transition 0 to State3 *)
State3 == x = -1

Obviously, the invariant is violated in State1 already, so states State2 and State3 are not informative. We could write a trace invariant to enforce invariant violation only in the last state. Alternatively, the model checker could enforce the constraint that the invariant holds true in the intermediate states. As invariants usually produce complex constraints and slow down the model checker, we leave the choice to the user.

Usually, the specification author has a good idea of how to partition states into interesting equivalence classes. We let you specify this partitioning by declaring a view abstraction, similar to the VIEW configuration option in TLC. Basically, two states are considered to be similar if they have the same view.

In our example, we compute the state view with the operator View1:

\* @type: <<Bool, Bool>>;
View1 ==
  <<x < 0, x > 0>>

Hence, the states with x = 1 and x = 25 are similar, because their view has the same value <<FALSE, TRUE>>. We can also define the view of an execution, simply as a sequence of views of the execution states.

Now we can ask Apalache to produce up to 50 counterexamples again. This time we tell it to avoid the executions that start with the view of an execution that produced an error earlier:

$ apalache check --inv=Inv --max-error=50 --view=View1 View2.tla
...
Found 20 error(s)
...

Now counterexample5.tla is more informative:

(* Initial state *)
State0 == x = 0

(* Transition 2 to State1 *)
State1 == x = 0

(* Transition 2 to State2 *)
State2 == x = 0

(* Transition 0 to State3 *)
State3 == x = 1

Moreover, counterexample6.tla is intuitively a mirror version of counterexample5.tla:

(* Initial state *)
State0 == x = 0

(* Transition 2 to State1 *)
State1 == x = 0

(* Transition 2 to State2 *)
State2 == x = 0

(* Transition 0 to State3 *)
State3 == x = -1

By the choice of the view, we have partitioned the states into three equivalence classes: x < 0, x = 0, and x > 0. It is often useful to write a view as a tuple of predicates. However, you can write arbitrary TLA+ expressions. A view is just a mapping from state variables to the set of values that can be computed by the view expressions.

We are using this technique in model-based testing. If you have found another interesting application of this technique, please let us know!