Merge branch 'main' into update/scala-library-2.13.14

.github/workflows/README.md

@@ -9,7 +9,7 @@
 
 - Triggered by pull requests into `main`.
 - Used for any artifacts that we deploy into production environments. Currently,
-  this only consists of our website at https://apalache.informal.systems.
+  this only consists of our website at https://apalache-mc.org.
 
 ## [./prepare-release.yml](./prepare-release.yml)
 

.github/workflows/main.yml

@@ -101,12 +101,7 @@ jobs:
         # See https://docs.github.com/en/actions/using-workflows/workflow-commands-for-github-actions#setting-an-environment-variable
         run: echo "APALACHE_HOME=$GITHUB_WORKSPACE" >> $GITHUB_ENV
       - name: Build and Unit Test
-        run: make test-coverage
-      - name: Upload coverage to Codecov
-        uses: codecov/codecov-action@v2
-        with:
-          # See https://app.codecov.io/gh/informalsystems/apalache/
-          token: ${{ secrets.CODECOV_TOKEN }} # not required for public repos
+        run: make test
       - name: Cleanup before cache
         # See https://www.scala-sbt.org/1.x/docs/GitHub-Actions-with-sbt.html#Caching
         shell: bash
@@ -166,8 +161,6 @@ 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

CHANGES.md

@@ -1,6 +1,16 @@
 <!-- NOTE: This file is generated. Do not write release notes here.
  Notes for unreleased changes go in the .unreleased/ directory. -->
 
+## 0.45.1 - 2024-08-19
+
+## 0.45.0 - 2024-08-17
+
+### Features
+
+- Handle expressions such as  S \in SUBSET [ a : Int ]  by rewriting the expression into  \A r \in S: DOMAIN r = {"a"} /\ r.a \in Int
+- Translate Quint's generate into `Apalache!Gen` (#2916)
+- Add `--timeout-smt` to limit SMT queries (#2936)
+
 ## 0.44.11 - 2024-05-06
 
 ### Features

Makefile

@@ -31,7 +31,8 @@ compile-strict: export APALACHE_FATAL_WARNINGS=true
 compile-strict:
 	sbt Test/compile compile
 
-# Run tests with scoverage report
+# Run tests with scoverage report.
+# This target is not used in the CI anymore. It needs additional devops work to re-enable it.
 test-coverage:
 	sbt coverage test coverageAggregate
 

VERSION

@@ -1 +1 @@
-0.44.12-SNAPSHOT
+0.45.2-SNAPSHOT

build.sbt

@@ -8,11 +8,11 @@ import scala.sys.process._
 ///////////////////////////
 
 name := "apalache"
-maintainer := "apalache@informal.org"
+maintainer := "apalache@konnov.phd"
 
 // See https://www.scala-sbt.org/1.x/docs/Multi-Project.html#Build-wide+settings
-ThisBuild / organizationName := "Informal Systems Inc."
-ThisBuild / organizationHomepage := Some(url("https://informal.systems"))
+ThisBuild / organizationName := "Apalache Development Team"
+ThisBuild / organizationHomepage := Some(url("https://apalache-mc.org"))
 ThisBuild / licenses += "Apache 2.0" -> url("https://www.apache.org/licenses/LICENSE-2.0")
 
 // We store the version in a bare file to make accessing and updating the version trivial
@@ -351,7 +351,7 @@ lazy val root = (project in file("."))
         log.info(s"Unpacking package ${pkg} to ${target_dir}")
         // send outputs directly to std{err,out} instead of logging here
         // to avoid misleading logging output from tar
-        // See https://github.com/informalsystems/apalache/pull/1382
+        // See https://github.com/apalache-mc/apalache/pull/1382
         (s"tar zxvf ${pkg} -C ${target_dir}" !)
         log.info(s"Symlinking ${current_pkg} -> ${unzipped}")
         if (current_pkg.exists) {
@@ -369,7 +369,7 @@ lazy val root = (project in file("."))
 docker / imageNames := {
   val img: String => ImageName = s =>
     ImageName(
-        namespace = Some("ghcr.io/informalsystems"),
+        namespace = Some("ghcr.io/apalache-mc"),
         repository = name.value,
         tag = Some(s),
     )
@@ -406,7 +406,7 @@ docker / dockerfile := {
 
     // We need sudo to run apalache using the user (created in the entrypoint script)
     run("apt", "update")
-    run("apt", "install", "sudo")
+    run("apt", "install", "-y", "sudo")
 
     entryPoint("/opt/apalache/bin/run-in-docker-container")
   }
@@ -425,7 +425,7 @@ lazy val versionFile = settingKey[File]("Location of the file tracking the proje
 // These tasks are used in our bespoke release pipeline
 // TODO(shon): Once we've changed our packaging to conform to more standard SBT structures and practices,
 // we should consider moving to a release pipeline based around sbt-release.
-// See https://github.com/informalsystems/apalache/issues/1248
+// See https://github.com/apalache-mc/apalache/issues/1248
 
 lazy val printVersion = taskKey[Unit]("Print the current version")
 printVersion := {

docs/src/apalache/installation/docker.md

@@ -14,15 +14,15 @@ suitable JVM, and the container supplies this. However, you must already have
 To get the latest Apalache image, issue the command:
 
 ```bash
-docker pull ghcr.io/informalsystems/apalache
+docker pull ghcr.io/apalache-mc/apalache
 ```
 
 ## Running the docker image
 
 To run an Apalache image, issue the command:
 
 ```bash
-$ docker run --rm -v <your-spec-directory>:/var/apalache ghcr.io/informalsystems/apalache <args>
+$ docker run --rm -v <your-spec-directory>:/var/apalache ghcr.io/apalache-mc/apalache <args>
 ```
 
 The following docker parameters are used:
@@ -38,8 +38,8 @@ The following docker parameters are used:
 
   When using SELinux, you might have to use the modified form of `-v` option:
     `-v <your-spec-directory>:/var/apalache:z`
-- `informalsystems/apalache` is the APALACHE docker image name. By default, the `latest` stable
-  version is used; you can also refer to a specific tool version, e.g., `informalsystems/apalache:0.6.0` or `informalsystems/apalache:main`
+- `apalache-mc/apalache` is the APALACHE docker image name. By default, the `latest` stable
+  version is used; you can also refer to a specific tool version, e.g., `apalache-mc/apalache:0.6.0` or `apalache-mc/apalache:main`
 - `<args>` are the tool arguments as described in [Running the Tool](../running.md).
 
 We provide a convenience wrapper for this docker command in
@@ -67,11 +67,11 @@ Apalache in docker while sharing the working directory:
 
 ###### using the latest stable
 
-$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/informalsystems/apalache'
+$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/apalache-mc/apalache'
 
 ###### using the latest main
 
-$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/informalsystems/apalache:main'
+$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/apalache-mc/apalache:main'
 ```
 
 ## Using the development branch of Apalache
@@ -82,25 +82,25 @@ branch for a report of the newest features. Since we cut releases weekly, you
 should have access to all the latest features in the last week by using the
 `latest` tag. However, if you wish to use the very latest developments as they
 are added throughout the week, you can run the image with the `main` tag: just
-type `ghcr.io/informalsystems/apalache:main` instead of
-`ghcr.io/informalsystems/apalache` everywhere.
+type `ghcr.io/apalache-mc/apalache:main` instead of
+`ghcr.io/apalache-mc/apalache` everywhere.
 
 Do not forget to pull the docker image from time to time:
 
 ```bash
-docker pull ghcr.io/informalsystems/apalache:main
+docker pull ghcr.io/apalache-mc/apalache:main
 ```
 
 Run it with the following command:
 
 ```bash
-$ docker run --rm -v <your-spec-directory>:/var/apalache ghcr.io/informalsystems/apalache:main <args>
+$ docker run --rm -v <your-spec-directory>:/var/apalache ghcr.io/apalache-mc/apalache:main <args>
 ```
 
 To create an alias pointing to the `main` version:
 
 ```bash
-$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/informalsystems/apalache:main'
+$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/apalache-mc/apalache:main'
 ```
 
 [changelog]: https://github.com/informalsystems/apalache/blob/main/CHANGES.md

project/Dependencies.scala

@@ -12,31 +12,31 @@ object Dependencies {
 
   object Deps {
     // Versions
-    lazy val logbackVersion = "1.5.6"
+    lazy val logbackVersion = "1.5.7"
     lazy val clistVersion = "3.5.1"
 
     // Libraries
     val clistCore = "org.backuity.clist" %% "clist-core" % clistVersion
     val clistMacros = "org.backuity.clist" %% "clist-macros" % clistVersion
     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 commonsConfiguration2 = "org.apache.commons" % "commons-configuration2" % "2.11.0"
     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
     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.6"
-    val scalaParserCombinators = "org.scala-lang.modules" %% "scala-parser-combinators" % "2.3.0"
+    val scalaParserCombinators = "org.scala-lang.modules" %% "scala-parser-combinators" % "2.4.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.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.6"
+    val z3 = "tools.aqua" % "z3-turnkey" % "4.13.0"
     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"
@@ -53,7 +53,7 @@ object Dependencies {
   object TestDeps {
     // Libraries
     val junit = "junit" % "junit" % "4.13.2" % Test
-    val scalacheck = "org.scalacheck" %% "scalacheck" % "1.17.1" % Test
+    val scalacheck = "org.scalacheck" %% "scalacheck" % "1.18.0" % Test
     val easymock = "org.easymock" % "easymock" % "5.4.0" % Test
 
     val scalaTestVersion = "3.2.15"

script/run-docker.sh

@@ -14,9 +14,9 @@ if [ -z "$APALACHE_TAG" ]
 then
     >&2 echo "# No docker image supplied. Defaulting to '$default_tag'"
     >&2 echo "# To run a specific docker tag set APALACHE_TAG."
-    img="ghcr.io/informalsystems/apalache:${default_tag}"
+    img="ghcr.io/apalache-mc/apalache:${default_tag}"
 else
-    img="ghcr.io/informalsystems/apalache:${APALACHE_TAG}"
+    img="ghcr.io/apalache-mc/apalache:${APALACHE_TAG}"
 fi
 
 # TODO Programmatically generate envars to expose here

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ExprOptimizer.scala

@@ -97,6 +97,34 @@ class ExprOptimizer(nameGen: UniqueNameGenerator, tracker: TransformationTracker
         }
         apply(tla.and(domEq +: fieldsEq: _*).as(b))
       }
+
+    // S ∈ SUBSET { ["a" ↦ x] : x ∈ T }
+    case memEx @ OperEx(TlaSetOper.in, setRec,
+            OperEx(TlaSetOper.powerset,
+                OperEx(TlaSetOper.map, OperEx(TlaFunOper.rec, fieldsAndValues @ _*), varsAndSets @ _*)))
+        if fieldsAndValues.length == varsAndSets.length =>
+      val (fields, values) = TlaOper.deinterleave(fieldsAndValues)
+      val (vars, sets) = TlaOper.deinterleave(varsAndSets)
+      assert(fields.length == vars.length)
+      if (values.zip(vars).exists(p => p._1 != p._2)) {
+        // The set has a more general form: { [f_1 |-> e_1, ..., f_k |-> e_k]: x_1 \in S_1, ..., x_k \in S_k }, where
+        //   e_1, ..., e_k are expressions over x_1, ..., x_k.
+        // We do not know how to optimize it.
+        memEx
+      } else {
+        val strSetT = SetT1(StrT1)
+        val b = BoolT1
+
+        val domType = getElemType(setRec)
+        val r = tla.name(nameGen.newName()).as(domType)
+
+        val domEq = tla.eql(tla.dom(r).as(SetT1(domType)), tla.enumSet(fields: _*).as(strSetT)).as(b)
+
+        val fieldsEq = fields.zip(values.zip(sets)).map { case (key, (value, set)) =>
+          tla.in(tla.appFun(r, key).as(value.typeTag.asTlaType1()), set).as(b)
+        }
+        apply(tla.forall(r, setRec, tla.and(domEq +: fieldsEq: _*).as(b)).as(b))
+      }
   }
 
   /**

tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala

@@ -87,22 +87,100 @@ class TestExprOptimizer extends AnyFunSuite with BeforeAndAfterEach {
 
   // An optimization for set membership over sets of records. Note that this is the standard form produced by Keramelizer.
   test("""r \in { [a |-> x, b |-> y]: x \in S, y \in T } becomes DOMAIN r = { "a", "b" } /\ r.a \in S /\ r.b \in T""") {
+    // ... [a |-> x, b |-> y] ...
     val recT = RecT1("a" -> IntT1, "b" -> IntT1)
-    val recSetT = SetT1(recT)
+    // ... x \in S, y \in T ...
     val record =
       enumFun(str("a"), name("x").as(intT), str("b"), name("y").as(intT)).as(recT)
+    // ... S ...
     val S = name("S").as(intSetT)
+    // ... T ...
     val T = name("T").as(intSetT)
+    // { ... }
+    val recSetT = SetT1(recT)
     val recordSet = map(record, name("x").as(intT), S, name("y").as(intT), T).as(recSetT)
+    // r ...
     val r = name("r").as(recT)
+    // ... \in ...
     val input = in(r, recordSet).as(boolT)
 
+    // ~~>
+
+    // DOMAIN r = { "a", "b" }
     val strSetT = SetT1(StrT1)
     val domEq = eql(dom(r).as(strSetT), enumSet(str("a"), str("b")).as(strSetT)).as(boolT)
+    // r.a \in S
     val memA = in(appFun(r, str("a")).as(intT), S).as(boolT)
+    // r.b \in T
     val memB = in(appFun(r, str("b")).as(intT), T).as(boolT)
+    // ... /\ ... /\ ...
     val expected = and(domEq, memA, memB).as(boolT)
     val output = optimizer.apply(input)
+
+    assert(expected == output)
+  }
+
+  // An optimization for set membership of the powerset of a record where the record has infinite co-domains.
+  test("""S \in SUBSET [a : T] ~~> \A r \in S: DOMAIN r = { "a" } /\ r.a \in T""") {
+
+    // ... { [a |-> x] : x \in T } ...
+    val recT = RecT1("a" -> IntT1)
+    val record =
+      enumFun(str("a"), name("x").as(intT)).as(recT)
+    val T = name("T").as(intSetT)
+    val recSetT = SetT1(recT)
+    val recordSet = map(record, name("x").as(intT), T).as(recSetT)
+
+    // ... SUBSET ...
+    val powSetT = powSet(recordSet).as(recSetT)
+
+    // S ...
+    val s = name("S").as(recSetT)
+
+    // ... \in ...
+    val input = in(s, powSetT).as(boolT)
+    val output = optimizer.apply(input)
+
+    // ~~>
+
+    // DOMAIN r = { "a" }
+    val r = name("t_1").as(recT)
+    val strSetT = SetT1(StrT1)
+    val domEq = eql(dom(r).as(strSetT), enumSet(str("a")).as(strSetT)).as(boolT)
+
+    // r.a \in T
+    val memA = in(appFun(r, str("a")).as(intT), T).as(boolT)
+
+    // ... /\ ...
+    val conjunct = and(domEq, memA).as(boolT)
+
+    // \A ...
+    val expected = forall(r, s, conjunct).as(boolT)
+
+    assert(expected == output)
+  }
+
+  test("""S \in SUBSET [a : T, b : U] ~~> \A r \in S: DOMAIN r = { "a", "b" } /\ r.a \in T /\ r.b \in U""") {
+    val recT = RecT1("a" -> IntT1, "b" -> IntT1)
+    val record =
+      enumFun(str("a"), name("x").as(intT), str("b"), name("y").as(intT)).as(recT)
+    val T = name("T").as(intSetT)
+    val U = name("U").as(intSetT)
+    val recSetT = SetT1(recT)
+    val recordSet = map(record, name("x").as(intT), T, name("y").as(intT), U).as(recSetT)
+    val powSetT = powSet(recordSet).as(recSetT)
+    val s = name("S").as(recSetT)
+    val input = in(s, powSetT).as(boolT)
+    val output = optimizer.apply(input)
+
+    val r = name("t_1").as(recT)
+    val strSetT = SetT1(StrT1)
+    val domEq = eql(dom(r).as(strSetT), enumSet(str("a"), str("b")).as(strSetT)).as(boolT)
+    val memA = in(appFun(r, str("a")).as(intT), T).as(boolT)
+    val memB = in(appFun(r, str("b")).as(intT), U).as(boolT)
+    val conjunct = and(domEq, memA, memB).as(boolT)
+    val expected = forall(r, s, conjunct).as(boolT)
+
     assert(expected == output)
   }