Merge branch 'main' into jk/oracles2

.unreleased/bug-fixes/2758-sim-timeout.md

@@ -0,0 +1 @@
+Continue simulation on SMT timeout in enabledness check, see #2758

mod-infra/src/main/scala/at/forsyte/apalache/infra/tlc/config/TlcConfig.scala

@@ -1,9 +1,9 @@
 package at.forsyte.apalache.infra.tlc.config
 
 import at.forsyte.apalache.infra.tlc.config.ConfigModelValue.STR_PREFIX
-import at.forsyte.apalache.tla.lir.convenience.tla
-import at.forsyte.apalache.tla.lir.{BoolT1, IntT1, SetT1, StrT1, TlaEx, Typed, VarT1}
-import at.forsyte.apalache.tla.lir.TypedPredefs._
+import at.forsyte.apalache.tla.lir.{TlaType1, Typed, VarT1}
+import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
+import at.forsyte.apalache.tla.types.{tla, ModelValueHandler}
 
 import scala.util.parsing.input.NoPosition
 
@@ -46,7 +46,7 @@ sealed abstract class ConfigConstExpr {
    * @return
    *   the TLA IR expression that represents the parsed constant expression
    */
-  def toTlaEx: TlaEx
+  def toTla: TBuilderInstruction
 }
 
 object ConfigModelValue {
@@ -64,11 +64,11 @@ object ConfigModelValue {
  *   the name of a model value
  */
 case class ConfigModelValue(name: String) extends ConfigConstExpr {
-  override def toTlaEx: TlaEx = {
+  override def toTla: TBuilderInstruction = {
     // currently, we use the type Str for all model values.
     // In the future, we might want to distinguish between different uninterpreted types.
     // See https://github.com/informalsystems/apalache/issues/570
-    tla.str(STR_PREFIX + name).typed(StrT1)
+    tla.str(STR_PREFIX + name)
   }
 }
 
@@ -79,7 +79,7 @@ case class ConfigModelValue(name: String) extends ConfigConstExpr {
  *   an integer as BigInt
  */
 case class ConfigIntValue(num: BigInt) extends ConfigConstExpr {
-  override def toTlaEx: TlaEx = tla.bigInt(num).typed(IntT1)
+  override def toTla: TBuilderInstruction = tla.int(num)
 }
 
 /**
@@ -89,7 +89,7 @@ case class ConfigIntValue(num: BigInt) extends ConfigConstExpr {
  *   a boolean
  */
 case class ConfigBoolValue(b: Boolean) extends ConfigConstExpr {
-  override def toTlaEx: TlaEx = tla.bool(b).typed(BoolT1)
+  override def toTla: TBuilderInstruction = tla.bool(b)
 }
 
 /**
@@ -99,7 +99,13 @@ case class ConfigBoolValue(b: Boolean) extends ConfigConstExpr {
  *   a string
  */
 case class ConfigStrValue(str: String) extends ConfigConstExpr {
-  override def toTlaEx: TlaEx = tla.str(str).typed(StrT1)
+  override def toTla: TBuilderInstruction = {
+    ModelValueHandler.typeAndIndex(str) match {
+      case None                => tla.str(str)
+      case Some((constT, idx)) => tla.const(idx, constT)
+    }
+
+  }
 }
 
 /**
@@ -109,18 +115,18 @@ case class ConfigStrValue(str: String) extends ConfigConstExpr {
  *   the set elements, which are constant expression themselves.
  */
 case class ConfigSetValue(elems: ConfigConstExpr*) extends ConfigConstExpr {
-  override def toTlaEx: TlaEx = {
-    val setElems = elems.map(_.toTlaEx)
+  override def toTla: TBuilderInstruction = {
+    val setElems = elems.map(_.toTla)
     if (setElems.isEmpty) {
       // the element type is uknown, introduce a polymorphic type Set(a)
-      tla.enumSet().typed(SetT1(VarT1(0)))
+      tla.emptySet(VarT1(0))
     } else {
       // the element type should be unique
-      val headType = setElems.head.typeTag.asTlaType1()
+      val headType = TlaType1.fromTypeTag(setElems.head.typeTag)
       if (setElems.tail.exists(_.typeTag != Typed(headType))) {
         throw new TlcConfigParseError("Set elements have different types: " + setElems.mkString(", "), NoPosition)
       } else {
-        tla.enumSet(setElems: _*).typed(SetT1(headType))
+        tla.enumSet(setElems: _*)
       }
     }
   }

passes/src/main/scala/at/forsyte/apalache/tla/passes/pp/ConfigurationPassImpl.scala

@@ -19,6 +19,7 @@ import at.forsyte.apalache.infra.tlc.config.TlcConfig
 import at.forsyte.apalache.infra.tlc.config.InitNextSpec
 import at.forsyte.apalache.infra.tlc.config.TemporalSpec
 import at.forsyte.apalache.infra.tlc.config.NullSpec
+import at.forsyte.apalache.tla.typecheck.TypingInputException
 
 /**
  * The pass that collects the configuration parameters and overrides constants and definitions. This pass also
@@ -50,8 +51,33 @@ class ConfigurationPassImpl @Inject() (
       case Some((tlcConfig, tlcConfigFile)) => loadOptionsFromTlcConfig(tlaModule, tlcConfig, tlcConfigFile)
     }
 
-    val constOverrideNames = tlaModule.constDeclarations.map(_.name).map(ConstAndDefRewriter.OVERRIDE_PREFIX + _).toSet
-    val (constOverrides, otherOverrides) = overrides.partition(d => constOverrideNames.contains(d.name))
+    val constOverrideNamesAndTypes =
+      tlaModule.constDeclarations.map { decl =>
+        (ConstAndDefRewriter.OVERRIDE_PREFIX + decl.name) -> decl.typeTag
+      }.toMap
+
+    val (constOverrides, otherOverrides) = overrides.partition(d => constOverrideNamesAndTypes.contains(d.name))
+
+    // Typecheck
+    // Since config files are not typecheckable, blind override substitution can introduce type inconsistencies
+    // see #2750
+    // To circumvent this, we manually perform a type-consistency check, to verify that values overriding constants
+    // have the same type as the constant declaration
+    constOverrides.foreach { decl =>
+      val constDeclTag = constOverrideNamesAndTypes(decl.name)
+      val overrideTag = decl match {
+        case d: TlaOperDecl => d.body.typeTag
+        case _              => decl.typeTag
+      }
+
+      if (overrideTag != constDeclTag) {
+        throw new TypingInputException(
+            s"Constant ${decl.name.drop(ConstAndDefRewriter.OVERRIDE_PREFIX.length)} declared in the specification has the type tag $constDeclTag, while the value defined in the .cfg file has the type tag $overrideTag.\n" +
+              s"Please make sure the values in the .cfg file have types matching those in the specification, or use --cinit instead.",
+            decl.ID,
+        )
+      }
+    }
 
     val newDecls =
       if (constOverrides.nonEmpty) {

test/tla/Bug2750.cfg

@@ -0,0 +1,7 @@
+\* Add statements after this line.
+SPECIFICATION Spec
+CONSTANTS 
+    Producers = {p1,p2}
+    Consumers = {c1,c2}
+    BufCapacity = 1
+INVARIANT Inv

test/tla/Bug2750.tla

@@ -0,0 +1,87 @@
+--------------------------- MODULE Bug2750 ---------------------------
+(***************************************************************************)
+(* Original problem and spec by Michel Charpentier                         *)
+(* http://www.cs.unh.edu/~charpov/programming-tlabuffer.html               *)
+(***************************************************************************)
+EXTENDS Naturals, Sequences
+
+CONSTANTS 
+    \* @type: Set(PROC);
+    Producers,   (* the (nonempty) set of producers                       *)
+    \* @type: Set(PROC);
+    Consumers,   (* the (nonempty) set of consumers                       *)
+    \* @type: Int;
+    BufCapacity  (* the maximum number of messages in the bounded buffer  *)
+
+ASSUME Assumption ==
+       /\ Producers # {}                      (* at least one producer *)
+       /\ Consumers # {}                      (* at least one consumer *)
+       /\ Producers \intersect Consumers = {} (* no thread is both consumer and producer *)
+       /\ BufCapacity \in (Nat \ {0})         (* buffer capacity is at least 1 *)
+
+-----------------------------------------------------------------------------
+
+VARIABLES 
+    \* @type: Seq(PROC);
+    buffer, 
+    \* @type: Set(PROC);
+    waitP, 
+    \* @type: Set(PROC);
+    waitC
+
+(* define statement *)
+isfull(b) == Len(b) = BufCapacity
+isempty(b) == Len(b) = 0
+
+\* @type: << Seq(PROC), Set(PROC), Set(PROC) >>;
+vars == << buffer, waitP, waitC >>
+
+ProcSet == (Producers) \cup (Consumers)
+
+Init == (* Global variables *)
+        /\ buffer = << >>
+        /\ waitP = {}
+        /\ waitC = {}
+
+p(self) == /\ (self \notin waitP)
+           /\ IF isfull(buffer)
+                 THEN /\ IF self \in Producers
+                            THEN /\ waitP' = (waitP \union {self})
+                                 /\ waitC' = waitC
+                            ELSE /\ waitC' = (waitC \union {self})
+                                 /\ waitP' = waitP
+                      /\ UNCHANGED buffer
+                 ELSE /\ buffer' = Append(buffer, self)
+                      /\ IF waitC # {}
+                            THEN /\ \E t \in waitC:
+                                      waitC' = waitC \ {t}
+                            ELSE /\ TRUE
+                                 /\ waitC' = waitC
+                      /\ waitP' = waitP
+
+c(self) == /\ (self \notin waitC)
+           /\ IF isempty(buffer)
+                 THEN /\ IF self \in Producers
+                            THEN /\ waitP' = (waitP \union {self})
+                                 /\ waitC' = waitC
+                            ELSE /\ waitC' = (waitC \union {self})
+                                 /\ waitP' = waitP
+                      /\ UNCHANGED buffer
+                 ELSE /\ buffer' = Tail(buffer)
+                      /\ IF waitP # {}
+                            THEN /\ \E t \in waitP:
+                                      waitP' = waitP \ {t}
+                            ELSE /\ TRUE
+                                 /\ waitP' = waitP
+                      /\ waitC' = waitC
+
+Next == (\E self \in Producers: p(self))
+           \/ (\E self \in Consumers: c(self))
+
+Spec == Init /\ [][Next]_vars
+
+\* END TRANSLATION 
+
+Inv == ~(waitP = Producers /\ waitC = Consumers)
+
+=============================================================================

test/tla/Test2750.cfg

@@ -0,0 +1,8 @@
+INIT
+Init
+NEXT
+Next
+INVARIANT
+Inv
+CONSTANT
+C = "1_OF_A"

test/tla/Test2750.tla

@@ -0,0 +1,19 @@
+----------------------- MODULE Test2750 -----------------------------
+VARIABLES
+    \* @type: A;
+    x
+
+CONSTANT
+    \* @type: A;
+    C
+
+
+Init ==
+    /\ x = C
+
+Next ==
+    UNCHANGED x
+
+Inv == TRUE
+
+===============================================================================

test/tla/cli-integration-tests.md

@@ -2316,6 +2316,22 @@ $ apalache-mc check --length=1 --cinit=CInit Bug2268.tla | sed 's/[IEW]@.*//'
 EXITCODE: OK
 ```
 
+### check Bug2750.tla
+
+```sh
+$ apalache-mc check --config=Bug2750.cfg Bug2750.tla | sed 's/[IEW]@.*//'
+...
+EXITCODE: ERROR (255)
+```
+
+### check Test2750.tla
+
+```sh
+$ apalache-mc check --config=Test2750.cfg Test2750.tla | sed 's/[IEW]@.*//'
+...
+EXITCODE: OK
+```
+
 ### check profiling
 
 Check that the profiler output is produced as explained in

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

@@ -262,8 +262,12 @@ class SeqModelChecker[ExecutorContextT](
               logger.info(s"Step ${trex.stepNo}: Transition #$no is disabled")
 
             case None =>
-              searchState.onResult(RuntimeError())
-              return (Set.empty, Set.empty) // UNKNOWN or timeout
+              if (params.isRandomSimulation) {
+                logger.info(s"Step ${trex.stepNo}: Transition #$no enabledness is UNKNOWN; assuming it is disabled")
+              } else {
+                searchState.onResult(RuntimeError())
+                return (Set.empty, Set.empty) // UNKNOWN or timeout
+              }
           }
           // recover from the snapshot
           trex.recover(snapshot.get)