Merge pull request #2969 from apalache-mc/igor/powset-message

improve the error message about expanding powersets

.unreleased/bug-fixes/2969-powset-expansion

@@ -0,0 +1 @@
+Better error reporting for hitting the limits of `SUBSET` expansion, see #2969

test/tla/TestSets.tla

@@ -145,6 +145,11 @@ TestExists15InPowerset ==
     \E S \in SUBSET Set263:
         S = { 2, 6 }
 
+\* This test is expected to fail. It should be run separately.
+FailExpandLargePowerset ==
+    \E S \in SUBSET (1..30):
+        31 \notin S
+
 TestForallInPowerset ==
     \A S \in SUBSET Set1357:
         6 \notin S

test/tla/cli-integration-tests.md

@@ -2668,6 +2668,16 @@ $ apalache-mc check --length=0 --inv=AllTests TestSets.tla | sed 's/[IEW]@.*//'
 EXITCODE: OK
 ```
 
+### check TestSets.tla reports an error on FailExpandLargePowerset
+
+```sh
+$ apalache-mc check --length=0 --inv=FailExpandLargePowerset TestSets.tla | sed 's/[IEW]@.*//'
+...
+<unknown>: known limitation: Attempted to expand a SUBSET of size 2^30, whereas the built-in limit is 2^20
+...
+EXITCODE: ERROR (255)
+```
+
 ### check TestCommunityFunctions.tla reports no error (array-encoding)
 
 ```sh

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

@@ -13,9 +13,9 @@ object Limits {
   val MAX_PRODUCT_SIZE = 1000000
 
   /**
-   * An upper bound on the size of an expanded powerset.
+   * An upper bound on the size of a base set that is expanded to a powerset, currently, `20`.
    */
-  val POWSET_MAX_SIZE = 1000000
+  val POWSET_MAX_BASE_SIZE = 20
 
   /**
    * An upper bound on the number of rewriting steps that are applied to the same rule.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerExceptionAdapter.scala

@@ -85,6 +85,10 @@ class CheckerExceptionAdapter @Inject() (sourceStore: SourceStore, changeListene
         "%s: no rule to rewrite a TLA+ expression: %s".format(findLoc(err.causeExpr.ID), err.getMessage)
       FailureMessage(msg)
 
+    case err: RewriterKnownLimitationError =>
+      val msg = "%s: known limitation: %s".format(findLoc(err.causeExpr.ID), err.getMessage)
+      NormalErrorMessage(msg)
+
     case err: RewriterException =>
       val msg = "%s: rewriter error: %s".format(findLoc(err.causeExpr.ID), err.getMessage)
       FailureMessage(msg)

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

@@ -22,6 +22,17 @@ class CheckerException(message: String, val causeExpr: TlaEx) extends Exception(
  */
 class RewriterException(message: String, causeExpr: TlaEx) extends CheckerException(message, causeExpr)
 
+/**
+ * This exception is thrown when the rewriter meets a generally well-formed TLA+ expression that cannot be handled due
+ * to some known limitations of the model checker.
+ *
+ * @param message
+ *   error message
+ * @param causeExpr
+ *   the problematic TLA+ expression, may be NullEx
+ */
+class RewriterKnownLimitationError(message: String, causeExpr: TlaEx) extends CheckerException(message, causeExpr)
+
 /**
  * This exception is thrown when QStateRewrite cannot find an applicable rule.
  *

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala

@@ -3,6 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux
 import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.lir.SetT1
 import at.forsyte.apalache.tla.types.{tlaU => tla}
+import com.typesafe.scalalogging.LazyLogging
 
 /**
  * This class constructs the power set of S, that is, SUBSET S. Sometimes, this is just unavoidable, e.g., consider { Q
@@ -11,7 +12,7 @@ import at.forsyte.apalache.tla.types.{tlaU => tla}
  * @author
  *   Igor Konnov
  */
-class PowSetCtor(rewriter: SymbStateRewriter) {
+class PowSetCtor(rewriter: SymbStateRewriter) extends LazyLogging {
 
   // Confringo is the explosion curse from Harry Potter. To let you know that your SMT solver will probably explode.
   def confringo(state: SymbState, set: ArenaCell): SymbState = {
@@ -39,10 +40,15 @@ class PowSetCtor(rewriter: SymbStateRewriter) {
     }
 
     rewriter.solverContext.log("; %s(%s) {".format(getClass.getSimpleName, state.ex))
-    val powSetSize = BigInt(1) << elems.size
-    if (powSetSize >= Limits.POWSET_MAX_SIZE) {
-      throw new RewriterException(s"Attempted to expand a powerset of size 2^${elems.size}", state.ex)
+    if (elems.size > Limits.POWSET_MAX_BASE_SIZE) {
+      logger.error("This error typically occurs when one enumerates all subsets of a set:"
+        + " \\A S \\in SUBSET T: P or \\E S \\in SUBSET T: P")
+      logger.error("Try to decrease the cardinality of the base set T, or avoid enumeration.")
+      val msg =
+        s"Attempted to expand a SUBSET of size 2^${elems.size}, whereas the built-in limit is 2^${Limits.POWSET_MAX_BASE_SIZE}"
+      throw new RewriterKnownLimitationError(msg, state.ex)
     }
+    val powSetSize = BigInt(1) << elems.size
     val subsets =
       if (elems.nonEmpty) {
         BigInt(0).to(powSetSize - 1).map(mkSetByNum)