Enumerating counterexamples

UNRELEASED.md

@@ -10,6 +10,12 @@
          * Some bug fix, see #124
 
      DO NOT LEAVE A BLANK LINE BELOW THIS PREAMBLE -->
+### Features
+
+* Checker: enumerating multiple counterexamples, see #542 and #827
+
 ### Documentation
 
- * links to ADR005
+* Manual: manual page on enumerating counterexamples and view abstraction, see #542
+
+* links to ADR005

docs/src/SUMMARY.md

@@ -18,6 +18,7 @@
         - [Source](./apalache/installation/source.md)
     - [Running the Tool](./apalache/running.md)
     - [Invariants: State, Action, Trace](./apalache/invariants.md)
+    - [Enumeration of counterexamples](./apalache/enumeration.md)
     - [TLA+ Execution Statistics](./apalache/statistics.md)
     - [An Example TLA+ Specification](./apalache/example.md)
     - [Specification Parameters](./apalache/parameters.md)

docs/src/apalache/enumeration.md

@@ -0,0 +1,150 @@
+# 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](./running.md). Sometimes, we want to produce multiple counterexamples;
+for instance, to generate multiple tests.
+
+Consider the following TLA+ specification:
+
+```tla
+{{#include ../../../test/tla/View2.tla:1:24}}
+```
+
+We can run Apalache to check the state invariant `Inv`:
+
+```sh
+$ apalache check --inv=Inv View2.tla
+```
+
+Apalache quickly finds a counterexample that looks like this:
+
+```tla
+...
+(* 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:
+
+```sh
+$ 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:
+
+```tla
+(* 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](./invariants.md#traceInv) 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 partitiong 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`:
+
+```tla
+{{#include ../../../test/tla/View2.tla:25:27}}
+```
+
+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:
+
+```sh
+$ apalache check --inv=Inv --max-error=50 --view=View1 View2.tla
+...
+Found 20 error(s)
+...
+```
+
+Now `counterexample5.tla` is more informative:
+
+```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
+```
+
+Moreover, `counterexample6.tla` is intuitively a mirror version of `counterexample5.tla`:
+
+```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!
+
+
+[TLC options]: https://lamport.azurewebsites.net/tla/tlc-options.html?back-link=tools.html
+

docs/src/apalache/invariants.md

@@ -73,6 +73,7 @@ There is no typo in the CLI arguments above: You pass action invariants the same
 as you pass state invariants. Preprocessing in Apalache is clever enough to figure out,
 what kind of invariant it is dealing with.
 
+<a name="traceInv"></a>
 ## Trace invariants
 
 

docs/src/apalache/running.md

@@ -32,6 +32,8 @@ The arguments are as follows:
     - `--discard-disabled` does a pre-check on transitions and discard the disabled ones at every step. If you know that
       many transitions are always enabled, set it to false. Sometimes, this pre-check may be slower than checking the
       invariant. Default: true.
+    - `--max-error <n>` instructs the search to stop after `n` errors, see [Enumeration of counterexamples][]. Default: 1.  
+    - `--view <name>` sets the state view to `<name>`, see [Enumeration of counterexamples][].
     - `--no-deadlock` disables deadlock-checking, when `--discard-disabled=false` is on. When `--discard-disabled=true`,
       deadlocks are found in any case.
     - `--tuning` specifies the properties file that stores the options for
@@ -263,3 +265,5 @@ In this case, Apalache performs the following steps:
    .
 
 1. It pretty-prints the IR into `out-parser.tla`, see [Detailed output](#detailed).
+
+[Enumeration of counterexamples]: ./enumeration.md

mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala

@@ -178,6 +178,9 @@ object Tool extends LazyLogging {
     executor.options.set("checker.discardDisabled", check.discardDisabled)
     executor.options.set("checker.noDeadlocks", check.noDeadlocks)
     executor.options.set("checker.algo", check.algo)
+    executor.options.set("checker.maxError", check.maxError)
+    if (check.view != "")
+      executor.options.set("checker.view", check.view)
     // for now, enable polymorphic types. We probably want to disable this option for the type checker
     executor.options.set("typechecker.inferPoly", true)
 

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala

@@ -42,4 +42,14 @@ class CheckCmd extends Command(name = "check", description = "Check a TLA+ speci
         "pre-check, whether a transition is disabled, and discard it, to make SMT queries smaller, default: true")
   var noDeadlocks: Boolean =
     opt[Boolean](name = "no-deadlock", default = true, description = "do not check for deadlocks, default: true")
+
+  var maxError: Int =
+    opt[Int](name = "max-error",
+        description =
+          "do not stop on first error, but produce up to a given number of counterexamples (fine tune with --view), default: 1",
+        default = 1)
+
+  var view: String =
+    opt[String](name = "view", description = "the state view to use with --max-error=n, default: transition index",
+        default = "")
 }

test/tla/View.tla

@@ -0,0 +1,64 @@
+---- MODULE View ----
+EXTENDS Integers, Sequences
+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
+    /\ y' = y + d
+    /\ action' = "B"
+
+Next ==
+  A \/ B
+
+Inv ==
+  x + y < 10
+
+\* @type: <<Bool, Bool>>;
+View1 ==
+  <<x >= 0, y >= 0>>
+
+View2 ==
+  action
+
+\* @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
+
+\* @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
+
+\* @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
+=================

test/tla/View2.tla

@@ -0,0 +1,28 @@
+---- 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
+
+\* @type: <<Bool, Bool>>;
+View1 ==
+  <<x < 0, x > 0>>
+=================

test/tla/cli-integration-tests.md

@@ -1176,6 +1176,28 @@ The outcome is: Error
 EXITCODE: ERROR (12)
 ```
 
+### check View.tla
+
+```sh
+$ apalache-mc check --inv=Inv --max-error=50 --view=View1 View.tla | sed 's/[IEW]@.*//'
+...
+Found 37 error(s)
+The outcome is: Error
+...
+EXITCODE: ERROR (12)
+```
+
+### check View2.tla
+
+```sh
+$ apalache-mc check --inv=Inv --max-error=50 --view=View1 View2.tla | sed 's/[IEW]@.*//'
+...
+Found 20 error(s)
+The outcome is: Error
+...
+EXITCODE: ERROR (12)
+```
+
 ## running the typecheck command
 
 ### typecheck ExistTuple476.tla reports no error: regression for issues 476 and 482

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Checker.scala

@@ -1,13 +1,35 @@
 package at.forsyte.apalache.tla.bmcmt
 
 object Checker {
-  object Outcome extends Enumeration {
-    val NoError, Error, Deadlock, RuntimeError, Interrupted = Value
+
+  /**
+   * The result of running the model checker.
+   */
+  sealed trait CheckerResult {}
+
+  case class NoError() extends CheckerResult {
+    override def toString: String = "NoError"
+  }
+
+  case class Error(nerrors: Int) extends CheckerResult {
+    override def toString: String = s"Error"
+  }
+
+  case class Deadlock() extends CheckerResult {
+    override def toString: String = "Deadlock"
+  }
+
+  case class Interrupted() extends CheckerResult {
+    override def toString: String = "Interrupted"
+  }
+
+  case class RuntimeError() extends CheckerResult {
+    override def toString: String = "RuntimeError"
   }
 }
 
 trait Checker {
   import Checker._
 
-  def run(): Outcome.Value
+  def run(): CheckerResult
 }

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/CheckerInputVC.scala

@@ -8,8 +8,9 @@ import at.forsyte.apalache.tla.lir.{TlaEx, TlaOperDecl}
  * @param stateInvariantsAndNegations  a list of state invariants and their negations
  * @param actionInvariantsAndNegations a list of action invariants and their negations
  * @param traceInvariantsAndNegations  a list of trace invariants and their negations
+ * @param stateView                    optional state view that is used for enumerating counterexamples
  * @author Igor Konnov
  */
 case class CheckerInputVC(stateInvariantsAndNegations: List[(TlaEx, TlaEx)] = List(),
     actionInvariantsAndNegations: List[(TlaEx, TlaEx)] = List(),
-    traceInvariantsAndNegations: List[(TlaOperDecl, TlaOperDecl)] = List()) {}
+    traceInvariantsAndNegations: List[(TlaOperDecl, TlaOperDecl)] = List(), stateView: Option[TlaEx] = None) {}