From 9e8f6e23ebebbbf0ed3e4ad6dd8290253d8d4e00 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Wed, 3 Aug 2022 17:50:14 +0200 Subject: [PATCH 01/10] Use static representation of invariant kinds --- .../forsyte/apalache/tla/bmcmt/InvariantKind.scala | 11 +++++++++++ .../apalache/tla/bmcmt/SeqModelChecker.scala | 14 +++++++------- 2 files changed, 18 insertions(+), 7 deletions(-) create mode 100644 tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/InvariantKind.scala diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/InvariantKind.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/InvariantKind.scala new file mode 100644 index 0000000000..b98f18e164 --- /dev/null +++ b/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" +} diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala index 6937b7c615..2dead37976 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala +++ b/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 } @@ -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") From ab7a624b1c90f86c4ab20b7676e0144cab37d49c Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Wed, 3 Aug 2022 18:31:45 +0200 Subject: [PATCH 02/10] Rephrase comment --- .../tla/bmcmt/trex/FilteredTransitionExecutor.scala | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/FilteredTransitionExecutor.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/FilteredTransitionExecutor.scala index b9bc3bc3f7..9196e1e94c 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/FilteredTransitionExecutor.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/FilteredTransitionExecutor.scala @@ -59,9 +59,9 @@ class FilteredTransitionExecutor[SnapshotT](stepFilter: String, invFilter: Strin 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. + // 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) } From 6c48e08d796777b161a3be1dc3c4ed15a3692abd Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Thu, 4 Aug 2022 12:50:00 +0200 Subject: [PATCH 03/10] Extend invariant filter syntax From words `$stepNo` to words `${stepNo}->${invariantKind}${invariantNo}`. --- .../apalache/tla/bmcmt/SeqModelChecker.scala | 4 +- .../trex/ConstrainedTransitionExecutor.scala | 9 +++- .../trex/FilteredTransitionExecutor.scala | 42 +++++++++++++++---- .../tla/bmcmt/trex/TransitionExecutor.scala | 13 +++++- .../bmcmt/trex/TransitionExecutorImpl.scala | 10 ++++- .../trex/TestFilteredTransitionExecutor.scala | 27 ++++++------ .../trex/TestTransitionExecutorImpl.scala | 18 ++++---- 7 files changed, 85 insertions(+), 38 deletions(-) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala index 2dead37976..0af2298efc 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala @@ -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 diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/ConstrainedTransitionExecutor.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/ConstrainedTransitionExecutor.scala index 6a63131f5f..9558e8528e 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/ConstrainedTransitionExecutor.scala +++ b/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) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/FilteredTransitionExecutor.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/FilteredTransitionExecutor.scala index 9196e1e94c..c8b653efda 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/FilteredTransitionExecutor.scala +++ b/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,17 +55,34 @@ 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) + 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. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutor.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutor.scala index 1906d398a9..0e16973d16 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutor.scala +++ b/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. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutorImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutorImpl.scala index 5c7b080cd6..67847f3f6c 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutorImpl.scala +++ b/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 diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestFilteredTransitionExecutor.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestFilteredTransitionExecutor.scala index b0469f5f84..b85294339d 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestFilteredTransitionExecutor.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestFilteredTransitionExecutor.scala @@ -1,5 +1,6 @@ package at.forsyte.apalache.tla.bmcmt.trex +import at.forsyte.apalache.tla.bmcmt.StateInvariant import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.convenience.tla import at.forsyte.apalache.tla.lir.UntypedPredefs._ @@ -54,7 +55,7 @@ trait TestFilteredTransitionExecutor[SnapshotT] extends ExecutorBase[SnapshotT] val impl = new TransitionExecutorImpl(Set.empty, Set("x", "y"), exeCtx) impl.debug = true val transFilter = "" - val invFilter = "(0|2)" + val invFilter = "(0->.*|2->.*)" val trex = new FilteredTransitionExecutor[SnapshotT](transFilter, invFilter, impl) trex.prepareTransition(1, init) trex.pickTransition() @@ -62,21 +63,21 @@ trait TestFilteredTransitionExecutor[SnapshotT] extends ExecutorBase[SnapshotT] // prepare Next trex.prepareTransition(1, nextTrans) // check what has changed + what is filtered - val inv1 = tla.ge(tla.name("x"), tla.int(3)) - val mayChange1 = trex.mayChangeAssertion(1, inv1) + val inv0 = tla.ge(tla.name("x"), tla.int(3)) + val mayChange0 = trex.mayChangeAssertion(1, StateInvariant, 0, inv0) + assert(!mayChange0) + val inv1 = tla.ge(tla.name("y"), tla.name("x")) + val mayChange1 = trex.mayChangeAssertion(1, StateInvariant, 1, inv1) assert(!mayChange1) - val inv2 = tla.ge(tla.name("y"), tla.name("x")) - val mayChange2 = trex.mayChangeAssertion(1, inv2) - assert(!mayChange2) trex.pickTransition() trex.nextState() // prepare Next trex.prepareTransition(1, nextTrans) // everything could have changed as the invariant filter was applied in the previous step - val mayChange21 = trex.mayChangeAssertion(1, inv1) + val mayChange20 = trex.mayChangeAssertion(1, StateInvariant, 0, inv0) + assert(mayChange20) + val mayChange21 = trex.mayChangeAssertion(1, StateInvariant, 1, inv1) assert(mayChange21) - val mayChange22 = trex.mayChangeAssertion(1, inv2) - assert(mayChange22) } test("filtered regression on #108") { exeCtx: ExecutorContextT => @@ -85,27 +86,27 @@ trait TestFilteredTransitionExecutor[SnapshotT] extends ExecutorBase[SnapshotT] // y' <- y + 1 val nextTrans = mkAssign("y", tla.plus(tla.name("y"), tla.int(1))) // push Init - val invFilter = "(1|2)" + val invFilter = "(1->.*|2->.*)" val impl = new TransitionExecutorImpl(Set.empty, Set("y"), exeCtx) val trex = new FilteredTransitionExecutor[SnapshotT]("", invFilter, impl) trex.prepareTransition(1, init) trex.pickTransition() // the user told us not to check the invariant in state 0 val notInv = tla.bool(false) - val mayChange1 = trex.mayChangeAssertion(1, notInv) + val mayChange1 = trex.mayChangeAssertion(1, StateInvariant, 0, notInv) assert(!mayChange1) trex.nextState() // apply Next trex.prepareTransition(1, nextTrans) // we must check the invariant right now, as it was skipped earlier - val mayChange2 = trex.mayChangeAssertion(1, notInv) + val mayChange2 = trex.mayChangeAssertion(1, StateInvariant, 0, notInv) assert(mayChange2) trex.pickTransition() trex.nextState() // apply Next trex.prepareTransition(1, nextTrans) // this time we should skip the check - val mayChange3 = trex.mayChangeAssertion(1, notInv) + val mayChange3 = trex.mayChangeAssertion(1, StateInvariant, 0, notInv) assert(!mayChange3) } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala index bbea60836d..3ce96efd8f 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala @@ -1,6 +1,6 @@ package at.forsyte.apalache.tla.bmcmt.trex -import at.forsyte.apalache.tla.bmcmt.Binding +import at.forsyte.apalache.tla.bmcmt.{Binding, StateInvariant} import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.convenience.tla import at.forsyte.apalache.tla.lir.UntypedPredefs._ @@ -186,12 +186,12 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] { // prepare Next trex.prepareTransition(1, nextTrans) // check what has changed - val inv1 = tla.ge(tla.name("x"), tla.int(3)) - val mayChange1 = trex.mayChangeAssertion(1, inv1) - assert(!mayChange1) - val inv2 = tla.ge(tla.name("y"), tla.name("x")) - val mayChange2 = trex.mayChangeAssertion(1, inv2) - assert(mayChange2) + val inv0 = tla.ge(tla.name("x"), tla.int(3)) + val mayChange0 = trex.mayChangeAssertion(1, StateInvariant, 0, inv0) + assert(!mayChange0) + val inv1 = tla.ge(tla.name("y"), tla.name("x")) + val mayChange1 = trex.mayChangeAssertion(1, StateInvariant, 1, inv1) + assert(mayChange1) } test("regression on #108") { exeCtx: ExecutorContextT => @@ -206,13 +206,13 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] { // The invariant negation does not refer to any variables. // We flag that it's satisfiability may change, as it could not be checked before val notInv = tla.bool(false) - val mayChange1 = trex.mayChangeAssertion(1, notInv) + val mayChange1 = trex.mayChangeAssertion(1, StateInvariant, 0, notInv) assert(mayChange1) trex.nextState() // apply Next trex.prepareTransition(1, nextTrans) // this time the invariant's validity should not change - val mayChange2 = trex.mayChangeAssertion(1, notInv) + val mayChange2 = trex.mayChangeAssertion(1, StateInvariant, 0, notInv) assert(!mayChange2) } From 11ac49b31001fb78a11902b79710d8a91af51312 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Thu, 4 Aug 2022 12:52:43 +0200 Subject: [PATCH 04/10] Add tests --- .../trex/TestFilteredTransitionExecutor.scala | 62 +++++++++++++++++-- 1 file changed, 58 insertions(+), 4 deletions(-) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestFilteredTransitionExecutor.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestFilteredTransitionExecutor.scala index b85294339d..5a1f5564a6 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestFilteredTransitionExecutor.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestFilteredTransitionExecutor.scala @@ -1,6 +1,6 @@ package at.forsyte.apalache.tla.bmcmt.trex -import at.forsyte.apalache.tla.bmcmt.StateInvariant +import at.forsyte.apalache.tla.bmcmt.{ActionInvariant, StateInvariant} import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.convenience.tla import at.forsyte.apalache.tla.lir.UntypedPredefs._ @@ -55,14 +55,16 @@ trait TestFilteredTransitionExecutor[SnapshotT] extends ExecutorBase[SnapshotT] val impl = new TransitionExecutorImpl(Set.empty, Set("x", "y"), exeCtx) impl.debug = true val transFilter = "" - val invFilter = "(0->.*|2->.*)" + val invFilter = "(0->.*|2->.*|3->state0|4->.*|5->state1|6->action1|7->action1)" val trex = new FilteredTransitionExecutor[SnapshotT](transFilter, invFilter, impl) trex.prepareTransition(1, init) trex.pickTransition() trex.nextState() // prepare Next trex.prepareTransition(1, nextTrans) - // check what has changed + what is filtered + // Step 1: Both invariants are excluded by the filter (no word starting in `1->`). + // inv0 == x >= 3 (unchanged by `Next`) + // inv1 == y >= x (maybe changed by `Next`) val inv0 = tla.ge(tla.name("x"), tla.int(3)) val mayChange0 = trex.mayChangeAssertion(1, StateInvariant, 0, inv0) assert(!mayChange0) @@ -73,11 +75,63 @@ trait TestFilteredTransitionExecutor[SnapshotT] extends ExecutorBase[SnapshotT] trex.nextState() // prepare Next trex.prepareTransition(1, nextTrans) - // everything could have changed as the invariant filter was applied in the previous step + // Step 2: Both invariants are included by the filter. + // Both may have changed, as the invariant filter excluded them both in the previous step. val mayChange20 = trex.mayChangeAssertion(1, StateInvariant, 0, inv0) assert(mayChange20) val mayChange21 = trex.mayChangeAssertion(1, StateInvariant, 1, inv1) assert(mayChange21) + trex.pickTransition() + trex.nextState() + // prepare Next + trex.prepareTransition(1, nextTrans) + // Step 3: Only state invariant 0 is included by the filter. + // State invariant 0 is not changed by `next` (and was included in the last state). + // State invariant 1 is ignored by the filter. + val mayChange30 = trex.mayChangeAssertion(1, StateInvariant, 0, inv0) + assert(!mayChange30) + val mayChange31 = trex.mayChangeAssertion(1, StateInvariant, 1, inv1) + assert(!mayChange31) + trex.pickTransition() + trex.nextState() + // prepare Next + trex.prepareTransition(1, nextTrans) + // Step 4: Both invariants are included by the filter. + // State invariant 0 is not changed by `next` (and was included in the last state). + // State invariant 1 may have changed, as the invariant filter excluded it in the previous step. + val mayChange40 = trex.mayChangeAssertion(1, StateInvariant, 0, inv0) + assert(!mayChange40) + val mayChange41 = trex.mayChangeAssertion(1, StateInvariant, 1, inv1) + assert(mayChange41) + trex.pickTransition() + trex.nextState() + // prepare Next + trex.prepareTransition(1, nextTrans) + // Step 5: Only state invariant 1 is included by the filter. + // State invariant 0 is excluded by the filter + // State invariant 1 is included by the filter, was included at the previous step, and may change. + val mayChange50 = trex.mayChangeAssertion(1, StateInvariant, 0, inv0) + assert(!mayChange50) + val mayChange51 = trex.mayChangeAssertion(1, StateInvariant, 1, inv1) + assert(mayChange51) + trex.pickTransition() + trex.nextState() + // prepare Next + trex.prepareTransition(1, nextTrans) + // Step 6: Both state invariants are excluded by the filter. + val mayChange60 = trex.mayChangeAssertion(1, StateInvariant, 0, inv0) + assert(!mayChange60) + val mayChange61 = trex.mayChangeAssertion(1, StateInvariant, 1, inv1) + assert(!mayChange61) + trex.pickTransition() + trex.nextState() + // prepare Next + trex.prepareTransition(1, nextTrans) + // Step 7: Pretend that both invariants are action invariants; the 2nd is included by the filter. + val mayChange70 = trex.mayChangeAssertion(1, ActionInvariant, 0, inv0) + assert(!mayChange70) + val mayChange71 = trex.mayChangeAssertion(1, ActionInvariant, 1, inv1) + assert(mayChange71) } test("filtered regression on #108") { exeCtx: ExecutorContextT => From a8ce3c69cefe7bc83bd663e11c55a1aa34d6e262 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Thu, 4 Aug 2022 12:52:58 +0200 Subject: [PATCH 05/10] Update docs --- docs/src/apalache/tuning.md | 31 +++++++++++++++++++++++-------- 1 file changed, 23 insertions(+), 8 deletions(-) diff --git a/docs/src/apalache/tuning.md b/docs/src/apalache/tuning.md index f4efd90b21..882dc3d7a7 100644 --- a/docs/src/apalache/tuning.md +++ b/docs/src/apalache/tuning.md @@ -43,6 +43,10 @@ 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=`. Restrict the choice of symbolic transitions @@ -66,16 +70,23 @@ the actions in the TLA+ spec. To find the numbers, run Apalache with ### Invariant filter `search.invariantFilter=`. Check the invariant only at the steps that -satisfy the regular expression. +satisfy the regular expression. The regular expression should recognize words +over of the form 's->ki', where `s` is a step number, `k` is an invariant kind +(["state" or "action"][invariants]) and `i` is a invariant number. + +For instance, `search.invariantFilter=10->.*|15->state0|20->action1` tells the +model checker to check -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. +* 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. -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. +[Trace invariants][] are checked regardless of this filter. + +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. ## Translation to SMT @@ -86,3 +97,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 From 9925e76f68361364d0670b98d807b1a65c2a9a90 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Thu, 4 Aug 2022 13:13:07 +0200 Subject: [PATCH 06/10] Add changelog entry --- .unreleased/breaking-changes/extd-inv-filter.md | 1 + 1 file changed, 1 insertion(+) create mode 100644 .unreleased/breaking-changes/extd-inv-filter.md diff --git a/.unreleased/breaking-changes/extd-inv-filter.md b/.unreleased/breaking-changes/extd-inv-filter.md new file mode 100644 index 0000000000..722d1162f0 --- /dev/null +++ b/.unreleased/breaking-changes/extd-inv-filter.md @@ -0,0 +1 @@ +Extended the invariant filter syntax, see #2034 From de32679e8117ca232453ac507444c19ec89bb734 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Thu, 4 Aug 2022 14:56:47 +0200 Subject: [PATCH 07/10] Use new invariant filter syntax in test command --- .../scala/at/forsyte/apalache/tla/tooling/opt/TestCmd.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/TestCmd.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/TestCmd.scala index 20ba42cd93..1dcc007067 100644 --- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/TestCmd.scala +++ b/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) From a517df1dc62c934bfc3a4878960331aad2505b4a Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Fri, 5 Aug 2022 10:34:09 +0200 Subject: [PATCH 08/10] Small language tweaks Co-authored-by: Shon Feder --- docs/src/apalache/tuning.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/docs/src/apalache/tuning.md b/docs/src/apalache/tuning.md index 882dc3d7a7..e466e4e0da 100644 --- a/docs/src/apalache/tuning.md +++ b/docs/src/apalache/tuning.md @@ -51,8 +51,8 @@ In the following, step 0 corresponds to the initialization with ``Init``, step 1 `search.transitionFilter=`. 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]+->.*)` @@ -70,9 +70,9 @@ the actions in the TLA+ spec. To find the numbers, run Apalache with ### Invariant filter `search.invariantFilter=`. Check the invariant only at the steps that -satisfy the regular expression. The regular expression should recognize words -over of the form 's->ki', where `s` is a step number, `k` is an invariant kind -(["state" or "action"][invariants]) and `i` is a invariant number. +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 From b83bf3e5c7a08fbd1b41e6a013b04fc87c46aad1 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Fri, 5 Aug 2022 11:49:43 +0200 Subject: [PATCH 09/10] Explain how to find VC/invariant indices --- docs/src/apalache/tuning.md | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/docs/src/apalache/tuning.md b/docs/src/apalache/tuning.md index e466e4e0da..dd650611f5 100644 --- a/docs/src/apalache/tuning.md +++ b/docs/src/apalache/tuning.md @@ -64,7 +64,7 @@ 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/.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 @@ -83,6 +83,15 @@ model checker to check [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/.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 From 7ef9a93545c63846f7bf5c1b51cbf3c2dceb6da8 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Fri, 5 Aug 2022 11:55:50 +0200 Subject: [PATCH 10/10] Add usecase --- docs/src/apalache/tuning.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/docs/src/apalache/tuning.md b/docs/src/apalache/tuning.md index dd650611f5..3ba59f6589 100644 --- a/docs/src/apalache/tuning.md +++ b/docs/src/apalache/tuning.md @@ -96,6 +96,8 @@ 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