Merge branch 'main' into parse-assume-name

apalache-mc · Jan 22, 2024 · 880d1c3 · 880d1c3
2 parents 35817ad + 99fb4d2
commit 880d1c3
Show file tree

Hide file tree

Showing 6 changed files with 44 additions and 3 deletions.
diff --git a/.unreleased/bug-fixes/fixSetInclusionwithArrays.md b/.unreleased/bug-fixes/fixSetInclusionwithArrays.md
@@ -0,0 +1 @@
+fix crash on the arrays encoding when having a subset relation containing infinite sets, see #2810
diff --git a/project/Dependencies.scala b/project/Dependencies.scala
@@ -27,7 +27,7 @@ object Dependencies {
     val logbackClassic = "ch.qos.logback" % "logback-classic" % logbackVersion
     val logbackCore = "ch.qos.logback" % "logback-core" % logbackVersion
     val logging = "com.typesafe.scala-logging" %% "scala-logging" % "3.9.5"
-    val pureConfig = "com.github.pureconfig" %% "pureconfig" % "0.17.4"
+    val pureConfig = "com.github.pureconfig" %% "pureconfig" % "0.17.5"
     val scalaParserCombinators = "org.scala-lang.modules" %% "scala-parser-combinators" % "2.3.0"
     val scalaCollectionContrib = "org.scala-lang.modules" %% "scala-collection-contrib" % "0.3.0"
     val scalaz = "org.scalaz" %% "scalaz-core" % "7.3.5"

diff --git a/test/tla/FunInInfiniteSubset.tla b/test/tla/FunInInfiniteSubset.tla
@@ -0,0 +1,22 @@
+--------------- MODULE FunInInfiniteSubset -----------------
+
+EXTENDS Integers
+
+P == {"P1_OF_P"}
+
+VARIABLE
+    \* @type: P -> Set(Int);
+    myVariable
+
+Init ==
+    myVariable = [p \in P |-> {0}]
+
+Step(p) ==
+    myVariable' = [q \in P |-> {0}]
+
+Next == \E p \in P : Step(p)
+
+TypeOkay == myVariable \in [P -> SUBSET Int]
+TypeOkay_ == TypeOkay
+
+=============================================
diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md
@@ -2812,6 +2812,18 @@ $ apalache-mc check --inv=Sanity FunExcept3.tla | sed 's/[IEW]@.*//'
 EXITCODE: OK
 ```
 
+### check FunInInfiniteSubset (array-encoding)
+
+A regression test for function membership in the presence of infinite sets.
+
+See https://github.com/informalsystems/apalache/issues/2810
+
+```sh
+$ apalache-mc check --init=TypeOkay_ --inv=TypeOkay --length=1 FunInInfiniteSubset.tla | sed 's/[IEW]@.*//'
+...
+EXITCODE: OK
+```
+
 ### check ERC20.tla
 
 ```sh

diff --git a/...bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithArrays.scala b/...bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithArrays.scala
@@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules
 
 import at.forsyte.apalache.tla.bmcmt.implicitConversions.Crossable
 import at.forsyte.apalache.tla.bmcmt.rewriter.ConstSimplifierForSmt
-import at.forsyte.apalache.tla.bmcmt.types.{CellTFrom, PowSetT, UnknownT}
+import at.forsyte.apalache.tla.bmcmt.types.{CellTFrom, InfSetT, PowSetT, UnknownT}
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, RewriterException, RewritingRule, SymbState, SymbStateRewriter}
 import at.forsyte.apalache.tla.lir.{BoolT1, OperEx, RecT1, SetT1, TlaEx, TupT1}
 import at.forsyte.apalache.tla.lir.convenience._
@@ -35,6 +35,9 @@ class SetInclusionRuleWithArrays(rewriter: SymbStateRewriter) extends RewritingR
           case (CellTFrom(SetT1(_)), CellTFrom(SetT1(_))) =>
             subset(rightState, leftCell, rightCell, false)
 
+          case (CellTFrom(SetT1(_)), InfSetT(_)) =>
+            subset(rightState, leftCell, rightCell, false)
+
           case (CellTFrom(SetT1(SetT1(t1))), PowSetT(SetT1(t2))) =>
             if (t1 != t2) {
               throw new RewriterException("Unexpected set types: %s and %s in %s"

diff --git a/...mt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithFunArrays.scala b/...mt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInclusionRuleWithFunArrays.scala
@@ -1,7 +1,7 @@
 package at.forsyte.apalache.tla.bmcmt.rules
 
 import at.forsyte.apalache.tla.bmcmt._
-import at.forsyte.apalache.tla.bmcmt.types.{CellTFrom, PowSetT}
+import at.forsyte.apalache.tla.bmcmt.types.{CellTFrom, InfSetT, PowSetT}
 import at.forsyte.apalache.tla.lir.{OperEx, SetT1}
 import at.forsyte.apalache.tla.lir.convenience._
 import at.forsyte.apalache.tla.lir.UntypedPredefs._
@@ -31,6 +31,9 @@ class SetInclusionRuleWithFunArrays(rewriter: SymbStateRewriter) extends Rewriti
           case (CellTFrom(SetT1(_)), CellTFrom(SetT1(_))) =>
             rewriter.lazyEq.subsetEq(rightState, leftCell, rightCell)
 
+          case (CellTFrom(SetT1(_)), InfSetT(_)) =>
+            rewriter.lazyEq.subsetEq(rightState, leftCell, rightCell)
+
           case (CellTFrom(SetT1(SetT1(t1))), PowSetT(SetT1(t2))) =>
             if (t1 != t2) {
               throw new RewriterException("Unexpected set types: %s and %s in %s"