Merge branch 'main' into gabriela/quint-fields-update

.scalafmt.conf

@@ -1,4 +1,4 @@
-version = "3.7.11"
+version = "3.7.12"
 
 runner.dialect = scala213
 fileOverride {

.unreleased/bug-fixes/2697-fresh-model-values.md

@@ -0,0 +1 @@
+Fix a bug with decoding unconstrained model values of uninterpreted types.

docs/src/HOWTOs/uninterpretedTypes.md

@@ -39,6 +39,8 @@ where:
 Example: `"1_OF_UT"` is a value belonging to the uninterpreted type `UT`, as is `"2_OF_UT"`. These two values are distinct by definition. On the contrary,
 `"1_OF_ut"` does _not_ meet the criteria for a value belonging to an uninterpreted type ( lowercase `ut` is not a valid identifier for an uninterpreted type), so it is treated as a string value.
 
+**Note**: Values matching the pattern `"FRESH[0-9]+_OF_TYPENAME"` are reserved for internal use, to allow Apalache to construct fresh values.
+
 ## Uninterpreted types, `Str`, and comparisons
 Importantly, while both strings and values belonging to uninterpreted types are introduced using the `"..."` notation, they are treated as having distinct, incomparable types.
 Examples:

passes/src/main/scala/at/forsyte/apalache/tla/passes/assignments/PrimingPassImpl.scala

@@ -3,12 +3,12 @@ package at.forsyte.apalache.tla.passes.assignments
 import at.forsyte.apalache.infra.passes.DerivedPredicates
 import at.forsyte.apalache.infra.passes.Pass.PassResult
 import at.forsyte.apalache.io.lir.TlaWriterFactory
-import at.forsyte.apalache.tla.lir.UntypedPredefs._
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.storage.BodyMapFactory
 import at.forsyte.apalache.tla.lir.transformations.TransformationTracker
 import at.forsyte.apalache.tla.lir.transformations.decorateWithPrime
 import at.forsyte.apalache.tla.lir.transformations.standard._
+import at.forsyte.apalache.tla.types.tla
 import com.google.inject.Inject
 import com.typesafe.scalalogging.LazyLogging
 
@@ -31,14 +31,14 @@ class PrimingPassImpl @Inject() (
 
     val bodyMap = BodyMapFactory.makeFromDecls(declarations)
 
-    val cinitPrimed = derivedPreds.cinit.map { name =>
+    val cinitPrimed: Option[TlaOperDecl] = derivedPreds.cinit.map { name =>
       val operatorBody = bodyMap(name).body
       val primeTransformer = decorateWithPrime(constSet, tracker) // add primes to constants
       val cinitPrimedName = name + "Primed"
       logger.info(s"  > Introducing $cinitPrimedName for $name'")
       val newBody = primeTransformer(deepCopy.deepCopyEx(operatorBody))
       // Safe constructor: cannot be recursive
-      TlaOperDecl(cinitPrimedName, List(), newBody)
+      tla.decl(cinitPrimedName, tla.unchecked(newBody))
     }
 
     val initName = derivedPreds.init
@@ -51,7 +51,7 @@ class PrimingPassImpl @Inject() (
     )
 
     // Safe constructor: cannot be recursive
-    val initPrimed = Some(TlaOperDecl(initPrimedName, List(), newBody))
+    val initPrimed: Option[TlaOperDecl] = Some(tla.decl(initPrimedName, tla.unchecked(newBody)))
 
     val newDeclarations: Seq[TlaDecl] = declarations ++ Seq(cinitPrimed, initPrimed).flatten
     val newModule = tlaModule.copy(declarations = newDeclarations)

project/Dependencies.scala

@@ -40,7 +40,7 @@ object Dependencies {
     val zio = "dev.zio" %% "zio" % zioVersion
     // Keep up to sync with version in plugins.sbt
     val zioGrpcCodgen = "com.thesamet.scalapb.zio-grpc" %% "zio-grpc-codegen" % "0.6.0-test3" % "provided"
-    val grpcNetty = "io.grpc" % "grpc-netty" % "1.57.0"
+    val grpcNetty = "io.grpc" % "grpc-netty" % "1.57.1"
     val scalapbRuntimGrpc =
       "com.thesamet.scalapb" %% "scalapb-runtime-grpc" % scalapb.compiler.Version.scalapbVersion
     // Ensures we have access to commonly used protocol buffers (e.g., google.protobuf.Struct)

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

@@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.TlaSetOper
 import at.forsyte.apalache.tla.lir.values._
 import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.{tla, ModelValueHandler}
+import at.forsyte.apalache.tla.types.tla
 import com.typesafe.scalalogging.LazyLogging
 
 import scala.collection.immutable.SortedMap
@@ -35,27 +35,28 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
     case CellTFrom(IntT1) =>
       cell.toBuilder.map(solverContext.evalGroundExpr)
 
-    case tt @ (CellTFrom(ConstT1(_)) | CellTFrom(StrT1)) =>
+    case ct @ CellTFrom(StrT1 | ConstT1(_)) =>
       // First, attempt to check the cache
       val found = rewriter.modelValueCache.findKey(cell)
-      if (found.isDefined) {
-        val pa @ (_, index) = found.get
-        if (tt == CellTFrom(StrT1)) tla.str(index)
-        else tla.constParsed(ModelValueHandler.construct(pa))
-      } else {
-        // if not in the cache, it might be the case that another cell, which has asserted equivalence
-        // with the original cell can be found
-        val values = rewriter.modelValueCache.values().filter(_.cellType == tt).toSeq
-        findCellInSet(values, cell.toBuilder) match {
-          // found among the cached keys
-          case Some(c) =>
-            decodeCellToTlaEx(arena, c)
-
-          case None =>
-            // not found, just use the name
-            // a value that was assigned by the solver, and not created by us
-            tla.str(cell.toString)
-        }
+      found match {
+        case Some((_, index)) =>
+          if (ct == CellTFrom(StrT1)) tla.str(index)
+          else tla.const(index, ct.tt.asInstanceOf[ConstT1])
+        case None =>
+          // if not in the cache, it might be the case that another cell, which has asserted equivalence
+          // with the original cell can be found
+          val values = rewriter.modelValueCache.values().filter(_.cellType == cell.cellType).toSeq
+          findCellInSet(values, cell.toBuilder) match {
+            case Some(c) =>
+              // found among the cached keys
+              decodeCellToTlaEx(arena, c)
+
+            case None =>
+              // not found, just use the name
+              // a value that was assigned by the solver, and not created by us
+              if (ct == CellTFrom(StrT1)) tla.str(s"FRESH${cell.id}")
+              else tla.const(s"FRESH${cell.id}", ct.tt.asInstanceOf[ConstT1])
+          }
       }
 
     case UnknownT() =>