View abstraction to enumerate counterexamples

[konnov]

This discussion is inspired by the demand for enumeration of counterexamples, e.g., in model-based testing, as discussed in #542. In a nutshell, we want to enumerate multiple counterexamples to a property, instead of producing just one example. The important question is how to enumerate essentially different counterexamples instead of enumerating similar counterexamples. As the notion of similarity depends on the specification and the user, we let the user decide what it means for states to be similar.

TLC has the VIEW configuration option that forces the model checker to search over abstract states instead of concrete states. As many abstractions, the view abstraction is usually an overapproximation. We can borrow the idea of the view abstraction and use it to partition the space of counterexamples. For example:

---- MODULE View ----
EXTENDS Integers
VARIABLES
    \* @type: Int;
    x,
    \* @type: Int;
    y,
    \* @type: Str;
    action

Init ==
  /\ x = 0
  /\ y = 0
  /\ action = "Init"

A ==
  \E d \in Int:
    /\ x' = x + d
    /\ y' = y
    /\ action' = "A"

B ==
  \E d \in Int:
    /\ x' = x + d
    /\ y' = y
    /\ action' = "B"

Next ==
  A \/ B

Inv ==
  x + y < 10

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

View2 ==
  action
=================

We can run apalache in the standard safety-checking mode:

apalache check --inv=Inv View.tla

Apalache will find a counterexample, e.g., x=10 and y=0 after firing action A. However, if we want to find another counterexample to this property, e.g., for testing, it will be hard to do so. We can set the random seed in z3 and try our luck again:

apalache check --inv=Inv --tuning-options=smt.randomSeed=133333 View.tla

However, the use of the random seed is up to z3, so it may return the same model. In principle, we would like to exclude the execution that resulted in a counterexample, that is, we could add a trace invariant like this:

\* @type: Seq([x: Int, y: Int, action: Str]) => Bool;
TraceInv1(hist) ==
  \/ /\ hist[1].x = 0 /\ hist[1].y = 0
     /\ hist[2].x = 10 /\ hist[2].y = 0
  \/ LET last == hist[Len(hist)] IN
     last.x + last.y < 10

Note that we had to embed Inv right into TraceInv1. Let's run apalache again:

apalache check --inv=TraceInv1 View.tla

This time it finds another counterexample: x = 11 and y = 0 after firing action A. That's a bit disappointing. Intuitively, it is not the most interesting test, as the solver has found yet another data point. We can see that the solver can just keep enumerating the values x=11, 12, 13, ...

Now let's write the trace invariant differently:

\* @type: Seq([x: Int, y: Int, action: Str]) => Bool;
TraceInv2(hist) ==
  \/ /\ hist[1].x >= 0 /\ hist[1].y >= 0
     /\ hist[2].x >= 0 /\ hist[2].y >= 0
  \/ LET last == hist[Len(hist)] IN
     last.x + last.y < 10

Intuitively, we are using the view abstraction, as defined with the operator View1, to exclude the whole set of executions that have non-negative components in the second state. If we check TraceInv2, the model checker produces another counterexample:

(* Initial state *)
State0 == action = "Init" /\ x = 0 /\ y = 0

(* Transition 0 to State1 *)
State1 == action = "A" /\ x = -1 /\ y = 0

(* Transition 0 to State2 *)
State2 == action = "A" /\ x = 10 /\ y = 0

As you can see, the solver is playing a little game here. It produces a very similar counterexample, but at different depth. We can go on and exclude this new set of counterexamples:

\* @type: Seq([x: Int, y: Int, action: Str]) => Bool;
TraceInv3(hist) ==
  \/ /\ hist[1].x >= 0 /\ hist[1].y >= 0
     /\ hist[2].x >= 0 /\ hist[2].y >= 0
  \/ /\ hist[1].x >= 0 /\ hist[1].y >= 0
     /\ hist[2].x < 0  /\ hist[2].y >= 0
     /\ hist[3].x >= 0 /\ hist[3].y >= 0
  \/ LET last == hist[Len(hist)] IN
     last.x + last.y < 10

By checking TraceInv3, we finally get a new interesting counterexample:

(* Initial state *)
State0 == action = "Init" /\ x = 0 /\ y = 0

(* Transition 0 to State1 *)
State1 == action = "A" /\ x = -1 /\ y = 0

(* Transition 1 to State2 *)
State2 == action = "B" /\ x = -1 /\ y = 11

As you can see, we can partition the execution space to exclude the examples that we have seen before. It is up to us how to do this partitioning. In the above example, we have been essentially using the operator View1 to exclude equivalence classes of executions. Alternatively, we could use View2 to exclude the same sequence of actions, independently of the values of x and y. If you know CEGAR, our approach is a very simple implementation of it.

We propose to implement this approach in the model checker, in order to enumerate classes of counterexamples instead of presenting just one example.

[konnov]

Automatic enumeration of counterexamples with the view abstraction is implemented in #833