Merge branch 'main' into update/sbt-native-packager-1.10.4

.git-blame-ignore-revs

@@ -6,3 +6,6 @@
 
 # Scala Steward: Reformat with scalafmt 3.7.6
 1b2091c13571348b534076f2183ced2cd2ff67a9
+
+# Scala Steward: Reformat with scalafmt 3.8.3
+60dd752b3c25a2b578b9f0a967878904d6941982

.github/workflows/README.md

@@ -16,15 +16,15 @@
 - Triggered manually.
 - The workflow prepares a release and opens a `[release]` PR.
 - **Requirements**:
-  - A personal API token is required to authenticate the API call that opens the
-    PR.
-    - We use a token belonging to our machine user [@apalache-bot][]. apalache-bot
+  - A personal API token called `APALACHE_BOT_TOKEN` is required to authenticate the API
+    call that opens the PR.
+    - We use a token belonging to our machine user [@coffeeinprogress][]. coffeeinprogress
       creates the PR from their fork of the repo, and they have no permissions in
       this repo itself.
     - Secrets are configured [here][secret-config].
 
-[@apalache-bot]: https://github.com/apalache-bot
-[secret-config]: https://github.com/informalsystems/apalache/settings/secrets/actions
+[@@coffeeinprogress]: https://github.com/coffeeinprogress
+[secret-config]: https://github.com/apalache-mc/apalache/settings/secrets/actions
 
 ## [./release.yml](./release.yml)
 

.github/workflows/main.yml

@@ -166,6 +166,8 @@ jobs:
           TEST_FILTER: ${{ matrix.smt-encoding == 'arrays' && 'array-encoding' || '' }}
 
   docker-tests:
+    # provisionally disable docker tests until we repair them
+    if: false
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4

.github/workflows/prepare-release.yml

@@ -3,7 +3,7 @@ name: prepare-release
 on:
   workflow_dispatch:
     # Allows manually triggering release via
-    # https://github.com/informalsystems/apalache/actions?query=workflow%3A%22Prepare+Release%22
+    # https://github.com/apalache-mc/apalache/actions?query=workflow%3A%22Prepare+Release%22
     inputs:
       release_version:
         description: "Version (leave empty to increment patch version)"
@@ -12,7 +12,7 @@ on:
 
 jobs:
   prepare-release:
-    if: github.repository_owner == 'informalsystems'
+    if: github.repository_owner == 'apalache-mc'
     env:
       RELEASE_VERSION: ${{ github.event.inputs.release_version }}
       # NOTE: We must not use the default GITHUB_TOKEN for auth here,

.scalafmt.conf

@@ -1,4 +1,4 @@
-version = "3.8.0"
+version = "3.8.3"
 
 runner.dialect = scala213
 fileOverride {

.unreleased/features/timeout-smt.md

@@ -0,0 +1 @@
+Add `--timeout-smt` to limit SMT queries (#2936)

.unreleased/features/translate-generate.md

@@ -0,0 +1 @@
+Translate Quint's generate into `Apalache!Gen` (#2916)

FUNDING.md

@@ -0,0 +1,19 @@
+## Apalache Funding
+
+We are grateful to the following organizations for financially supporting
+the project Apalache for significant duration of time in the past:
+
+- [Informal Systems][]: 2020-2024
+- [Vienna Business Agency][]: 2021-2023
+- [Interchain Foundation][]: 2019-2023
+- [WWTF][] (Austria): Vienna Science and Technology Fund 2016-2020
+- [Inria Nancy][] and [LORIA][] (France): 2018-2019
+- [TU Wien][] (Austria): 2016-2020
+
+[WWTF]: https://wwtf.at/index.php?lang=EN
+[TU Wien]: https://www.tuwien.at/
+[Inria Nancy]: https://www.inria.fr/en/inria-centre-universite-lorraine
+[LORIA]: https://loria.fr
+[Interchain Foundation]: https://interchain.io/
+[Informal Systems]: https://informal.systems/
+[Vienna Business Agency]: https://viennabusinessagency.at/

docs/src/apalache/tuning.md

@@ -22,14 +22,6 @@ The following options are supported:
 `smt.randomSeed=<int>` passes the random seed to `z3` (via `z3`'s parameters
 `sat.random_seed` and `smt.random_seed`).
 
-##  Timeouts
-
-`search.smt.timeout=<seconds>` defines the timeout to the SMT solver in seconds.
-The default value is `0`, which stands for the unbounded timeout.  For instance,
-the timeout is used in the following cases: checking if a transition is enabled,
-checking an invariant, checking for deadlocks. If the solver times out, it
-reports 'UNKNOWN', and the model checker reports a runtime error.
-
 ## Invariant mode
 
 `search.invariant.mode=(before|after)` defines the moment when the invariant is

docs/src/lang/apalache-operators.md

@@ -142,7 +142,44 @@ IN
 The operators `ApaFoldSet` and `ApaFoldSeqLeft` are explained in more detail in a dedicated section [here](../apalache/principles/folds.md).
 
 ----------------------------------------------------------------------------
+<a name="Repeat"></a>
+## Operator iteration
 
+**Notation:** `Repeat(Op, N, x)`
+
+**LaTeX notation:** `Repeat(Op, N, x)`
+
+**Arguments:** Three arguments: An operator `Op`, an iteration counter `N` (a nonnegative constant integer expression), and an
+initial value `x`.
+
+**Apalache type:** `((a, Int), Int, a) => a`, for some type `a`.
+
+**Effect:** For a given constant bound `N`, computes the value
+`F(F(F(F(x,1), 2), ...), N)`. If `N=0` it evaluates to `x`.
+
+```tla
+Repeat(Op, N, x) ==
+    ApaFoldSeqLeft(Op, x, MkSeq(N, LAMBDA i:i))
+```
+
+Apalache implements a more efficient encoding of this operator than the default one.
+
+**Determinism:** Deterministic.
+
+**Errors:**
+If any argument is ill-typed, or `N` is not a nonnegative constant integer expression, Apalache reports an error.
+
+**Example in TLA+:**
+
+```tla
+Op(a) == a + 1
+LET OpModified(a,i) == Op(i)
+IN Repeat(OpModified, 0, 5) = 5     \* TRUE
+
+Op2(a,i) == a + i
+Repeat(Op2, 0, 5) = 15              \* TRUE
+```
+----------------------------------------------------------------------------
 <a name="SetAsFun"></a>
 
 ## Convert a set of pairs to a function

mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala

@@ -162,6 +162,8 @@ object Config {
    *   maximal number of Next steps
    * @param maxError
    *   whether to stop on the first error or to produce up to a given number of counterexamples
+   * @param timeoutSmtSec
+   *   the time limit on SMT queries in seconds
    * @param noDeadLocks
    *   do not check for deadlocks
    * @param smtEncoding
@@ -182,6 +184,7 @@ object Config {
       next: Option[String] = None,
       length: Option[Int] = Some(10),
       maxError: Option[Int] = Some(1),
+      timeoutSmtSec: Option[Int] = Some(0),
       noDeadlocks: Option[Boolean] = Some(false),
       smtEncoding: Option[SMTEncoding] = Some(SMTEncoding.OOPSLA19),
       temporalProps: Option[List[String]] = None,
@@ -660,6 +663,7 @@ object OptionGroup extends LazyLogging {
       discardDisabled: Boolean,
       length: Int,
       maxError: Int,
+      timeoutSmtSec: Int,
       noDeadlocks: Boolean,
       smtEncoding: SMTEncoding,
       tuning: Map[String, String])
@@ -684,11 +688,13 @@ object OptionGroup extends LazyLogging {
         smtEncoding <- checker.smtEncoding.toTry("checker.smtEncoding")
         tuning <- checker.tuning.toTry("checker.tuning")
         maxError <- checker.maxError.toTry("checker.maxError").flatMap(validateMaxError)
+        timeoutSmtSec <- checker.timeoutSmtSec.toTry("checker.timeoutSmtSec")
       } yield Checker(
           algo = algo,
           discardDisabled = discardDisabled,
           length = length,
           maxError = maxError,
+          timeoutSmtSec = timeoutSmtSec,
           noDeadlocks = noDeadlocks,
           smtEncoding = smtEncoding,
           tuning = tuning,

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala

@@ -69,6 +69,11 @@ class CheckCmd(name: String = "check", description: String = "Check a TLA+ speci
     opt[Boolean](name = "output-traces", description = "save an example trace for each symbolic run, default: false",
         default = false)
 
+  var timeoutSmtSec: Option[Int] =
+    opt[Option[Int]](name = "timeout-smt",
+        description = "limit the duration of a single SMT check query with `n` seconds, default: 0 (unlimited)",
+        default = None)
+
   override def toConfig(): Try[Config.ApalacheConfig] = {
     val loadedTuningOptions = tuningOptionsFile.map(f => loadProperties(f)).getOrElse(Map())
     val combinedTuningOptions = overrideProperties(loadedTuningOptions, tuningOptions.getOrElse("")) ++ Map(
@@ -83,6 +88,7 @@ class CheckCmd(name: String = "check", description: String = "Check a TLA+ speci
               discardDisabled = discardDisabled,
               noDeadlocks = noDeadlocks,
               maxError = maxError,
+              timeoutSmtSec = timeoutSmtSec,
               view = view,
           ),
           typechecker = cfg.typechecker.copy(

project/Dependencies.scala

@@ -12,7 +12,7 @@ object Dependencies {
 
   object Deps {
     // Versions
-    lazy val logbackVersion = "1.5.3"
+    lazy val logbackVersion = "1.5.6"
     lazy val clistVersion = "3.5.1"
 
     // Libraries
@@ -21,7 +21,7 @@ object Dependencies {
     val commonsBeanutils =
       "commons-beanutils" % "commons-beanutils" % "1.9.4" // Apparently an untracked dependency of commonsConfiguration2
     val commonsConfiguration2 = "org.apache.commons" % "commons-configuration2" % "2.9.0"
-    val commonsIo = "commons-io" % "commons-io" % "2.15.1"
+    val commonsIo = "commons-io" % "commons-io" % "2.16.1"
     val guice = "com.google.inject" % "guice" % "7.0.0"
     val kiama = "org.bitbucket.inkytonik.kiama" %% "kiama" % "2.5.1"
     val logbackClassic = "ch.qos.logback" % "logback-classic" % logbackVersion
@@ -31,16 +31,16 @@ object Dependencies {
     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"
-    val slf4j = "org.slf4j" % "slf4j-api" % "2.0.12"
+    val slf4j = "org.slf4j" % "slf4j-api" % "2.0.16"
     val shapeless = "com.chuusai" %% "shapeless" % "2.3.10"
     val tla2tools = "org.lamport" % "tla2tools" % "1.7.0-SNAPSHOT"
     val ujson = "com.lihaoyi" %% "ujson" % "3.2.0"
     val upickle = "com.lihaoyi" %% "upickle" % "3.2.0"
-    val z3 = "tools.aqua" % "z3-turnkey" % "4.12.5"
+    val z3 = "tools.aqua" % "z3-turnkey" % "4.12.6"
     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.62.2"
+    val grpcNetty = "io.grpc" % "grpc-netty" % "1.66.0"
     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)
@@ -54,7 +54,7 @@ object Dependencies {
     // Libraries
     val junit = "junit" % "junit" % "4.13.2" % Test
     val scalacheck = "org.scalacheck" %% "scalacheck" % "1.17.0" % Test
-    val easymock = "org.easymock" % "easymock" % "5.2.0" % Test
+    val easymock = "org.easymock" % "easymock" % "5.4.0" % Test
 
     val scalaTestVersion = "3.2.15"
     val scalatest = "org.scalatest" %% "scalatest" % scalaTestVersion % Test

project/build.properties

@@ -1 +1 @@
-sbt.version=1.9.9
+sbt.version=1.10.1

project/plugins.sbt

@@ -7,7 +7,7 @@ addSbtPlugin("se.marcuslonnberg" % "sbt-docker" % "1.11.0")
 // https://github.com/scoverage/sbt-scoverage
 addSbtPlugin("org.scoverage" % "sbt-scoverage" % "2.0.11")
 // https://github.com/sbt/sbt-buildinfo
-addSbtPlugin("com.eed3si9n" % "sbt-buildinfo" % "0.11.0")
+addSbtPlugin("com.eed3si9n" % "sbt-buildinfo" % "0.12.0")
 // https://github.com/sbt/sbt-native-packager
 addSbtPlugin("com.github.sbt" % "sbt-native-packager" % "1.10.4")
 // https://scalacenter.github.io/scalafix/docs/users/installation.html

project/sbt-changeling/build.sbt

@@ -2,7 +2,7 @@ ThisBuild / version := "0.1.0-SNAPSHOT"
 ThisBuild / organization := "systems.informal"
 
 libraryDependencies ++= Seq(
-    "org.scala-sbt" % "sbt" % "1.9.9"
+    "org.scala-sbt" % "sbt" % "1.10.1"
 )
 
 lazy val sbt_changeling = (project in file("."))

project/sbt-changeling/project/build.properties

@@ -1 +1 @@
-sbt.version=1.9.9
+sbt.version=1.10.1

src/tla/Apalache.tla

@@ -152,4 +152,17 @@ ApaFoldSeqLeft(__Op(_,_), __v, __seq) ==
     THEN __v
     ELSE ApaFoldSeqLeft(__Op, __Op(__v, Head(__seq)), Tail(__seq))
 
+(**
+ * The repetition operator, used to consecutively apply an operator, starting from
+ * an initial value.
+ *
+ * @type: ((a, Int) => a, Int, a) => a;
+ *)
+RECURSIVE Repeat(_,_,_)
+Repeat(__F(_,_), __N, __x) ==
+        \* This is the TLC implementation. Apalache does it differently.
+        IF __N <= 0
+        THEN __x
+        ELSE __F(Repeat(__F, __N - 1, __x), __N)
+
 ===============================================================================

test/tla/Repeat.tla

@@ -0,0 +1,66 @@
+------------------------ MODULE Repeat ------------------------------------
+EXTENDS Apalache, Integers
+
+Inv1 ==
+    LET Op(a, i) == a + 1
+    IN Repeat(Op, 5, 0) = 5
+
+Inv2 ==
+    LET Op(a, i) == a + i
+    IN Repeat(Op, 5, 0) = 15
+
+\* Cyclical Op: \E k: Op^k = Id
+Inv3 ==
+    LET Op(a,i) == (a + i) % 3
+    IN LET
+        v == 1
+        x0 == Repeat(Op, 0, v)
+        x3 == Repeat(Op, 3, v)
+        x6 == Repeat(Op, 6, v)
+    IN
+        /\ v = x0
+        /\ x0 = x3
+        /\ x3 = x6
+
+\* Idempotent Op: Op^2 = Op
+Inv4 ==
+    LET
+        \* @type: (Set(Set(Int)), Int) => Set(Set(Int));
+        Op(a, i) == {UNION a}
+    IN LET
+        v == {{1}, {2}, {3,4}}
+        x1 == Repeat(Op, 1, v)
+        x2 == Repeat(Op, 2, v)
+        x3 == Repeat(Op, 3, v)
+    IN
+        /\ v /= x1
+        /\ x1 = x2
+        /\ x2 = x3
+
+\* Nilpotent Op: \E k: Op^k = 0
+Inv5 ==
+    LET
+        \* @type: (Set(Int), Int) => Set(Int);
+        Op(a, i) == a \ { x \in a: \A y \in a: x <= y }
+    IN LET
+        v == {1,2,3}
+        x1 == Repeat(Op, 2, v)
+        x2 == Repeat(Op, 3, v)
+        x3 == Repeat(Op, 4, v)
+    IN
+        /\ x1 /= x2
+        /\ x2 = x3
+        /\ x3 = {}
+
+
+Init == TRUE
+Next == TRUE
+
+Inv ==
+    /\ Inv1
+    /\ Inv2
+    /\ Inv3
+    /\ Inv4
+    /\ Inv5
+
+===============================================================================

test/tla/RepeatBad.tla

@@ -0,0 +1,11 @@
+------------------------ MODULE RepeatBad ------------------------------------
+EXTENDS Apalache, Integers
+
+Inv ==
+    LET Op(a, i) == a + 1
+    \* The 2nd argument to Repeat must be an integer literal
+    IN \E x \in {5} : Repeat(Op, x, 0) = 5
+
+Init == TRUE
+Next == TRUE
+===============================================================================