diff --git a/.github/workflows/README.md b/.github/workflows/README.md index d8d29ba024..49339e90ce 100644 --- a/.github/workflows/README.md +++ b/.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) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 5a95199b64..2b765ef796 100644 --- a/.github/workflows/main.yml +++ b/.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 diff --git a/.unreleased/features/timeout-smt.md b/.unreleased/features/timeout-smt.md deleted file mode 100644 index dd27979cfb..0000000000 --- a/.unreleased/features/timeout-smt.md +++ /dev/null @@ -1 +0,0 @@ -Add `--timeout-smt` to limit SMT queries (#2936) diff --git a/.unreleased/features/translate-generate.md b/.unreleased/features/translate-generate.md deleted file mode 100644 index 326f24450d..0000000000 --- a/.unreleased/features/translate-generate.md +++ /dev/null @@ -1 +0,0 @@ -Translate Quint's generate into `Apalache!Gen` (#2916) diff --git a/CHANGES.md b/CHANGES.md index e370b63d49..e523bc2b40 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,14 @@ +## 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 diff --git a/Makefile b/Makefile index 0058403306..16ed465722 100644 --- a/Makefile +++ b/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 diff --git a/VERSION b/VERSION index 93722f80fa..630d1052de 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -0.44.12-SNAPSHOT +0.45.1-SNAPSHOT diff --git a/build.sbt b/build.sbt index ae0af55d5d..a052c4239b 100644 --- a/build.sbt +++ b/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 := { diff --git a/docs/src/apalache/installation/docker.md b/docs/src/apalache/installation/docker.md index d5eea19e76..c43bfbea58 100644 --- a/docs/src/apalache/installation/docker.md +++ b/docs/src/apalache/installation/docker.md @@ -14,7 +14,7 @@ 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 @@ -22,7 +22,7 @@ docker pull ghcr.io/informalsystems/apalache To run an Apalache image, issue the command: ```bash -$ docker run --rm -v :/var/apalache ghcr.io/informalsystems/apalache +$ docker run --rm -v :/var/apalache ghcr.io/apalache-mc/apalache ``` 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 :/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` - `` 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 :/var/apalache ghcr.io/informalsystems/apalache:main +$ docker run --rm -v :/var/apalache ghcr.io/apalache-mc/apalache:main ``` 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 diff --git a/project/Dependencies.scala b/project/Dependencies.scala index 77e5b146b9..ed98809c61 100644 --- a/project/Dependencies.scala +++ b/project/Dependencies.scala @@ -12,7 +12,7 @@ object Dependencies { object Deps { // Versions - lazy val logbackVersion = "1.5.6" + lazy val logbackVersion = "1.5.7" lazy val clistVersion = "3.5.1" // Libraries @@ -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" diff --git a/script/run-docker.sh b/script/run-docker.sh index 05d3df4c8b..4f8a094ffc 100755 --- a/script/run-docker.sh +++ b/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 diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ExprOptimizer.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ExprOptimizer.scala index e85d215f85..9faa5d1b68 100644 --- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ExprOptimizer.scala +++ b/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)) + } } /** diff --git a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala index 5f13923734..a38e77fefc 100644 --- a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala +++ 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) }