Extend the invariant filter to specify particular invariants

.unreleased/breaking-changes/extd-inv-filter.md

@@ -0,0 +1 @@
+Extended the invariant filter syntax, see #2034

docs/src/apalache/tuning.md

@@ -43,12 +43,16 @@ Apalache has enough memory. The default mode is `before`.
 
 ## Guided search
 
+### Preliminaries
+
+In the following, step 0 corresponds to the initialization with ``Init``, step 1 is the first step with ``Next``, etc.
+
 ### Transition filter
 
 `search.transitionFilter=<regex>`. Restrict the choice of symbolic transitions
 at every step with a regular expression. The regular expression should recognize
-words over of the form `s->t`, where `s` is a step number and `t` is a
-transition number.
+words of the form `s->t`, where `s` is a step number and `t` is a transition
+number.
 
 For instance,
 `search.transitionFilter=(0->0|1->5|2->(2|3)|[3-9]->.*|[1-9][0-9]+->.*)`
@@ -60,22 +64,40 @@ Note that there is no direct correspondence between the transition numbers and
 the actions in the TLA+ spec. To find the numbers, run Apalache with
 `--write-intermediate=true` and check the transition numbers in
 `_apalache-out/<MySpec>.tla/*/intermediate/XX_OutTransitionFinderPass.tla`: the
-0th transition is called `Next_si_0000`, 1st transition is called
+0th transition is called `Next_si_0000`, the 1st transition is called
 `Next_si_0001`, etc.
 
 ### Invariant filter
 
 `search.invariantFilter=<regex>`. Check the invariant only at the steps that
-satisfy the regular expression.
-
-For instance, `search.invariantFilter=10|15|20` tells the model checker to
-check the invariant only *after* exactly 10, 15, or 20 step were made. Step 0
-corresponds to the initialization with ``Init``, step 1 is the first step
-with ``Next``, etc.
-
-This option is useful for checking consensus algorithms, where the decision
-cannot be revoked. So instead of checking the invariant after each step, we can
-do that after the algorithm has made a good number of steps.
+satisfy the regular expression. The regular expression should recognize words of
+the form `s->ki`, where `s` is a step number, `k` is an invariant kind (["state"
+or "action"][invariants]), and `i` is an invariant number.
+
+For instance, `search.invariantFilter=10->.*|15->state0|20->action1` tells the
+model checker to check
+
+* all invariants only *after* exactly 10 steps have been made,
+* the *first* state invariant only after exactly 15 steps, and
+* the *second* action invariant after exactly 20 steps.
+
+[Trace invariants][] are checked regardless of this filter.
+
+Note that there is no direct correspondence between invariant numbers and the
+operators in a TLA+ spec. Rather, the numbers refer to *verification conditions*
+(i.e., broken up parts of a TLA+ invariant operator). To find these numbers, run
+Apalache with `--write-intermediate=true` and check the invariant numbers in
+`_apalache-out/<MySpec>.tla/*/intermediate/XX_OutVCGen.tla`. The 0th state
+invariant is called `VCInv_si_0`, the 1st state invariant is called
+`VCInv_si_1`, and so on. For action invariants, the declarations are named
+`VCActionInv_si_0`, `VCActionInv_si_1` etc.
+
+This option is useful, e.g., for checking consensus algorithms,
+where the decision cannot be revoked. So instead of checking the invariant
+after each step, we can do that after the algorithm has made a good number of
+steps.
+You can also use this option to check different parts of an invariant on
+different machines to speed up turnaround time.
 
 ## Translation to SMT
 
@@ -86,3 +108,7 @@ B` and `A /\ B` are translated to SMT as if-then-else expressions, e.g., `(ite A
 true B)`. Otherwise, disjunctions and conjunctions are directly translated to
 `(or ...)` and `(and ...)` respectively. By default,
 `rewriter.shortCircuit=false`.
+
+
+[invariants]: ../apalache/principles/invariants.md
+[trace invariants]: ../apalache/principles/invariants.md#trace-invariants

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

@@ -40,7 +40,7 @@ class TestCmd
     //   1. Check the invariant only after the action took place.
     //   2. Randomize
     val seed = Math.abs(System.currentTimeMillis().toInt)
-    val tuning = Map("search.invariantFilter" -> "1", "smt.randomSeed" -> seed.toString)
+    val tuning = Map("search.invariantFilter" -> "1->.*", "smt.randomSeed" -> seed.toString)
     logger.info("Tuning: " + tuning.toList.map { case (k, v) => s"$k=$v" }.mkString(":"))
 
     executor.passOptions.set("general.tuning", tuning)

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

@@ -0,0 +1,11 @@
+package at.forsyte.apalache.tla.bmcmt
+
+sealed trait InvariantKind
+
+case object StateInvariant extends InvariantKind {
+  override def toString(): String = "state"
+}
+
+case object ActionInvariant extends InvariantKind {
+  override def toString(): String = "action"
+}

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

@@ -156,7 +156,7 @@ class SeqModelChecker[ExecutorContextT](
     }
 
     if (params.invariantMode == InvariantMode.AfterJoin && isNext) {
-      checkInvariants(trex.stepNo - 1, notActionInvariants, maybeActionInvariantNos, "action")
+      checkInvariants(trex.stepNo - 1, notActionInvariants, maybeActionInvariantNos, ActionInvariant)
       if (!searchState.canContinue) {
         return
       }
@@ -167,7 +167,7 @@ class SeqModelChecker[ExecutorContextT](
 
     // check the state invariants
     if (params.invariantMode == InvariantMode.AfterJoin) {
-      checkInvariants(trex.stepNo - 1, notInvariants, maybeInvariantNos, "state")
+      checkInvariants(trex.stepNo - 1, notInvariants, maybeInvariantNos, StateInvariant)
       if (!searchState.canContinue) {
         return
       }
@@ -186,7 +186,7 @@ class SeqModelChecker[ExecutorContextT](
 
     def addMaybeInvariants(trNo: Int): Set[Int] = {
       val indices = notInvariants.zipWithIndex
-        .filter(p => trex.mayChangeAssertion(trNo, p._1))
+        .filter(p => trex.mayChangeAssertion(trNo, StateInvariant, p._2, p._1))
         .map(_._2)
       val newIndices = indices.toSet
       maybeInvariantNos ++= newIndices
@@ -195,7 +195,7 @@ class SeqModelChecker[ExecutorContextT](
 
     def addMaybeActionInvariants(trNo: Int): Set[Int] = {
       val indices = notActionInvariants.zipWithIndex
-        .filter(p => trex.mayChangeAssertion(trNo, p._1))
+        .filter(p => trex.mayChangeAssertion(trNo, ActionInvariant, p._2, p._1))
         .map(_._2)
       val newIndices = indices.toSet
       maybeActionInvariantNos ++= newIndices
@@ -233,7 +233,7 @@ class SeqModelChecker[ExecutorContextT](
               if (params.invariantMode == InvariantMode.BeforeJoin) {
                 // check the action invariants, unless we process Init
                 if (isNext) {
-                  checkInvariants(trex.stepNo - 1, notActionInvariants, transitionActionInvs, "action")
+                  checkInvariants(trex.stepNo - 1, notActionInvariants, transitionActionInvs, ActionInvariant)
                   if (!searchState.canContinue) {
                     // an invariant is violated and we cannot continue the search, return immediately
                     return (maybeInvariantNos, maybeActionInvariantNos)
@@ -242,7 +242,7 @@ class SeqModelChecker[ExecutorContextT](
 
                 // check the state invariants
                 trex.nextState() // advance to the next state
-                checkInvariants(trex.stepNo - 1, notInvariants, transitionInvs, "state")
+                checkInvariants(trex.stepNo - 1, notInvariants, transitionInvs, StateInvariant)
                 if (!searchState.canContinue) {
                   // an invariant is violated and we cannot continue the search, return immediately
                   return (maybeInvariantNos, maybeActionInvariantNos)
@@ -318,11 +318,11 @@ class SeqModelChecker[ExecutorContextT](
     trex.assumeTransition(transitionNo)
     if (isNext) {
       // check action invariants
-      checkInvariants(trex.stepNo - 1, notActionInvariants, maybeActionInvariantNos, "action")
+      checkInvariants(trex.stepNo - 1, notActionInvariants, maybeActionInvariantNos, ActionInvariant)
     }
     if (searchState.canContinue) {
       trex.nextState()
-      checkInvariants(trex.stepNo - 1, notInvariants, maybeInvariantNos, "state")
+      checkInvariants(trex.stepNo - 1, notInvariants, maybeInvariantNos, StateInvariant)
     }
     // and recover
     trex.recover(snapshot)
@@ -333,7 +333,7 @@ class SeqModelChecker[ExecutorContextT](
       stateNo: Int,
       notInvs: Seq[TlaEx],
       numbersToCheck: Set[Int],
-      kind: String): Unit = {
+      kind: InvariantKind): Unit = {
     // check the invariants
     if (numbersToCheck.nonEmpty) {
       logger.info(s"State $stateNo: Checking ${numbersToCheck.size} $kind invariants")

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/ConstrainedTransitionExecutor.scala

@@ -1,5 +1,6 @@
 package at.forsyte.apalache.tla.bmcmt.trex
 
+import at.forsyte.apalache.tla.bmcmt.InvariantKind
 import at.forsyte.apalache.tla.bmcmt.rules.aux.Oracle
 import at.forsyte.apalache.tla.lir.oper.TlaBoolOper
 import at.forsyte.apalache.tla.lir.{BoolT1, NameEx, OperEx, TlaEx, Typed}
@@ -100,8 +101,12 @@ class ConstrainedTransitionExecutor[ExecutorContext](trex: TransitionExecutor[Ex
 
   override def nextState(): Unit = trex.nextState()
 
-  override def mayChangeAssertion(transitionNo: Int, assertion: TlaEx): Boolean =
-    trex.mayChangeAssertion(transitionNo, assertion)
+  override def mayChangeAssertion(
+      transitionNo: Int,
+      invariantKind: InvariantKind,
+      invariantNo: Int,
+      assertion: TlaEx): Boolean =
+    trex.mayChangeAssertion(transitionNo, invariantKind, invariantNo, assertion)
 
   override def assertState(assertion: TlaEx): Unit = trex.assertState(assertion)
 

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/FilteredTransitionExecutor.scala

@@ -1,17 +1,21 @@
 package at.forsyte.apalache.tla.bmcmt.trex
+import at.forsyte.apalache.tla.bmcmt.InvariantKind
 import at.forsyte.apalache.tla.bmcmt.rules.aux.Oracle
 import at.forsyte.apalache.tla.lir.TlaEx
 
 /**
- * A transition executor that keeps only the steps and invariants, which are given by the regular expressions.
+ * A filtering transition executor. Keeps only transitions and invariants that match the regular expressions
+ * `stepFilter` and `invFilter`, respectively.
  *
  * @param stepFilter
- *   a string that encodes a regular expression that recognizes pairs "stepNo->transitionNo", where stepNo is a step
- *   number and transitionNo is a transition number; may be empty
+ *   a string that encodes a regular expression that recognizes pairs `\${stepNo}->\${transitionNo}`, where `\${stepNo}`
+ *   is a step number and `\${transitionNo}` is a transition number. If empty, no filtering is applied.
  * @param invFilter
- *   a string that encodes a regular expression over step numbers; may be empty
+ *   a string that encodes a regular expression that recognizes triples `\${stepNo}->\${invariantKind}\${invariantNo}`,
+ *   where `\${stepNo}` is a step number, `\${invariantKind}` is "state" or "action" (see [[InvariantKind]]), and
+ *   `\${invariantNo}` is a invariant number. If empty, no filtering is applied.
  * @param trex
- *   an implementation to delegate to
+ *   the [[TransitionExecutor]] to delegate to
  * @tparam SnapshotT
  *   a snapshot type
  */
@@ -27,6 +31,9 @@ class FilteredTransitionExecutor[SnapshotT](stepFilter: String, invFilter: Strin
    * context. It is the user's responsibility to pop the context, e.g., by recovering from a snapshot. (In an
    * incremental solver, it is cheap; in an offline solver, this may slow down the checker.)
    *
+   * Only keeps the transition if the word `\${stepNo}->\${transitionNo}` (where `\${stepNo}` is the current [[stepNo]]
+   * and `\${transitionNo}` is the given `transitionNo`) is recognized by the regular expression `stepFilter`.
+   *
    * @param transitionNo
    *   a number associated with the transition, must be unique for the current step
    * @param transitionEx
@@ -48,20 +55,37 @@ class FilteredTransitionExecutor[SnapshotT](stepFilter: String, invFilter: Strin
    * A syntactic test on whether a translated transition may change satisfiability of an assertion. It tests, whether
    * all variables mentioned in the assertion belong to the unchanged set of the transition.
    *
+   * Only keeps the invariant if the word `\${stepNo}->\${invariantKind}\${invariantNo}` (where `\${stepNo}` is the
+   * current [[FilteredTransitionExecutor.stepNo]], and `\${invariantKind}` and `\${transitionNo}` are the given
+   * parameters) is recognized by the regular expression `invFilter`.
+   *
    * @param transitionNo
    *   the index of a previously prepared transition
+   * @param invariantKind
+   *   the kind of assertion being tested
+   * @param invariantNo
+   *   an index identifying the tested assertion among those of the same `invariantKind`
    * @param assertion
    *   a state expression
    * @return
    *   true, if the transition may affect satisfiability of the assertion
    */
-  override def mayChangeAssertion(transitionNo: Int, assertion: TlaEx): Boolean = {
-    val prevExcluded = (stepNo > 0) && invFilter.nonEmpty && !invRe.pattern.matcher("%d".format(stepNo - 1)).matches
-    val thisExcluded = invFilter.nonEmpty && !invRe.pattern.matcher(s"$stepNo").matches
-    val mayChange = trex.mayChangeAssertion(transitionNo, assertion)
-    // One of the options is allowed, unless it is excluded at the current step:
-    // 1. The assertion was excluded at the previous step, or
-    // 2. The transition may have changed the assertion.
+  override def mayChangeAssertion(
+      transitionNo: Int,
+      invariantKind: InvariantKind,
+      invariantNo: Int,
+      assertion: TlaEx): Boolean = {
+    // string expressions identifying the invariant in the current and previous transitions
+    val thisWord = s"$stepNo->$invariantKind$invariantNo"
+    val prevWord = s"${stepNo - 1}->$invariantKind$invariantNo"
+    // check exclusion by the transition filter
+    val prevExcluded = (stepNo > 0) && invFilter.nonEmpty && !invRe.pattern.matcher(prevWord).matches
+    val thisExcluded = invFilter.nonEmpty && !invRe.pattern.matcher(thisWord).matches
+    // check if the current transition may change the assertion
+    val mayChange = trex.mayChangeAssertion(transitionNo, invariantKind, invariantNo, assertion)
+    // Unless the invariant is excluded at the current step, it may change satisfiability if:
+    // 1. The assertion was excluded at the previous step (it may have changed then), or
+    // 2. The current transition may change satisfiability.
     !thisExcluded && (prevExcluded || mayChange)
   }
 

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutor.scala

@@ -1,4 +1,5 @@
 package at.forsyte.apalache.tla.bmcmt.trex
+import at.forsyte.apalache.tla.bmcmt.InvariantKind
 import at.forsyte.apalache.tla.bmcmt.rewriter.Recoverable
 import at.forsyte.apalache.tla.bmcmt.rules.aux.Oracle
 import at.forsyte.apalache.tla.lir.TlaEx
@@ -78,12 +79,20 @@ trait TransitionExecutor[ExecutorContextT] extends Recoverable[ExecutionSnapshot
    *
    * @param transitionNo
    *   the index of a previously prepared transition
+   * @param invariantKind
+   *   the kind of assertion being tested
+   * @param invariantNo
+   *   an index identifying the tested assertion among those of the same `invariantKind`
    * @param assertion
-   *   a state expression
+   *   the tested assertion
    * @return
    *   true, if the transition may affect satisfiability of the assertion
    */
-  def mayChangeAssertion(transitionNo: Int, assertion: TlaEx): Boolean
+  def mayChangeAssertion(
+      transitionNo: Int,
+      invariantKind: InvariantKind,
+      invariantNo: Int,
+      assertion: TlaEx): Boolean
 
   /**
    * Push an assertion about the current controlState.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutorImpl.scala

@@ -163,12 +163,20 @@ class TransitionExecutorImpl[ExecCtxT](consts: Set[String], vars: Set[String], c
    *
    * @param transitionNo
    *   the index of a previously prepared transition
+   * @param invariantKind
+   *   the kind of assertion being tested
+   * @param invariantNo
+   *   an index identifying the tested assertion among those of the same `invariantKind`
    * @param assertion
    *   a state expression
    * @return
    *   true, if the transition may affect satisfiability of the assertion
    */
-  override def mayChangeAssertion(transitionNo: Int, assertion: TlaEx): Boolean = {
+  override def mayChangeAssertion(
+      transitionNo: Int,
+      invariantKind: InvariantKind,
+      invariantNo: Int,
+      assertion: TlaEx): Boolean = {
     val trans = preparedTransitions(transitionNo)
     val binding = trans.binding