From f5110eedc1aabb5aa38e111dcd6eb7d8389c2083 Mon Sep 17 00:00:00 2001 From: Scala Steward Date: Tue, 12 Sep 2023 19:00:51 +0000 Subject: [PATCH 01/11] Update sbt-scalafix to 0.11.1 --- project/plugins.sbt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/project/plugins.sbt b/project/plugins.sbt index 7b65d12b78..90d977f882 100644 --- a/project/plugins.sbt +++ b/project/plugins.sbt @@ -11,7 +11,7 @@ addSbtPlugin("com.eed3si9n" % "sbt-buildinfo" % "0.11.0") // https://github.com/sbt/sbt-native-packager addSbtPlugin("com.github.sbt" % "sbt-native-packager" % "1.9.16") // https://scalacenter.github.io/scalafix/docs/users/installation.html -addSbtPlugin("ch.epfl.scala" % "sbt-scalafix" % "0.11.0") +addSbtPlugin("ch.epfl.scala" % "sbt-scalafix" % "0.11.1") // https://scalapb.github.io/zio-grpc/docs/installation addSbtPlugin("com.thesamet" % "sbt-protoc" % "1.0.6") // https://github.com/sbt/sbt-unidoc From 2b0e63f5a124cd3a87753a79076d54e2ae7b3414 Mon Sep 17 00:00:00 2001 From: Scala Steward Date: Tue, 12 Sep 2023 19:01:08 +0000 Subject: [PATCH 02/11] Update scala-library to 2.13.12 --- build.sbt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.sbt b/build.sbt index 9b03e8d4f7..af4414d61c 100644 --- a/build.sbt +++ b/build.sbt @@ -20,7 +20,7 @@ ThisBuild / versionFile := (ThisBuild / baseDirectory).value / "VERSION" ThisBuild / version := scala.io.Source.fromFile(versionFile.value).mkString.trim ThisBuild / organization := "at.forsyte" -ThisBuild / scalaVersion := "2.13.11" +ThisBuild / scalaVersion := "2.13.12" // Add resolver for Sonatype OSS Snapshots and Releases Maven repository ThisBuild / resolvers ++= Resolver.sonatypeOssRepos("snapshots") From 1db427e43d0292a5aaf098175a10b4d8a51801b5 Mon Sep 17 00:00:00 2001 From: shonfeder Date: Mon, 18 Sep 2023 13:57:37 +0000 Subject: [PATCH 03/11] [release] 0.43.0 --- RELEASE.md | 5 +++++ VERSION | 2 +- 2 files changed, 6 insertions(+), 1 deletion(-) create mode 100644 RELEASE.md diff --git a/RELEASE.md b/RELEASE.md new file mode 100644 index 0000000000..27d64e3b00 --- /dev/null +++ b/RELEASE.md @@ -0,0 +1,5 @@ +## 0.43.0 - 2023-09-18 + +### Features + +- - Revise the ITF format: Use only `{ "#bigint": "num" }`, even for small integers` diff --git a/VERSION b/VERSION index ebe902dc1d..8298bb08b2 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -0.42.1-SNAPSHOT +0.43.0 From 34214457c983fb78fdc1ee45dc580c625caa9964 Mon Sep 17 00:00:00 2001 From: shonfeder Date: Mon, 18 Sep 2023 13:57:50 +0000 Subject: [PATCH 04/11] Bump version to 0.43.1-SNAPSHOT --- .unreleased/features/2732.md | 1 - CHANGES.md | 6 ++++++ RELEASE.md | 5 ----- VERSION | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) delete mode 100644 .unreleased/features/2732.md delete mode 100644 RELEASE.md diff --git a/.unreleased/features/2732.md b/.unreleased/features/2732.md deleted file mode 100644 index 5cd634822b..0000000000 --- a/.unreleased/features/2732.md +++ /dev/null @@ -1 +0,0 @@ -- Revise the ITF format: Use only `{ "#bigint": "num" }`, even for small integers` diff --git a/CHANGES.md b/CHANGES.md index 6d3892feb7..5dddc429ee 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,12 @@ +## 0.43.0 - 2023-09-18 + +### Features + +- - Revise the ITF format: Use only `{ "#bigint": "num" }`, even for small integers` + ## 0.42.0 - 2023-08-21 ### Breaking changes diff --git a/RELEASE.md b/RELEASE.md deleted file mode 100644 index 27d64e3b00..0000000000 --- a/RELEASE.md +++ /dev/null @@ -1,5 +0,0 @@ -## 0.43.0 - 2023-09-18 - -### Features - -- - Revise the ITF format: Use only `{ "#bigint": "num" }`, even for small integers` diff --git a/VERSION b/VERSION index 8298bb08b2..0a53b801ea 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -0.43.0 +0.43.1-SNAPSHOT From d739118a345c731af9c988d8323c26a3b2a34c94 Mon Sep 17 00:00:00 2001 From: Scala Steward Date: Mon, 18 Sep 2023 17:06:00 +0000 Subject: [PATCH 05/11] Update ujson, upickle to 3.1.3 --- project/Dependencies.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/project/Dependencies.scala b/project/Dependencies.scala index e233546232..91413b3f33 100644 --- a/project/Dependencies.scala +++ b/project/Dependencies.scala @@ -34,8 +34,8 @@ object Dependencies { val slf4j = "org.slf4j" % "slf4j-api" % "2.0.9" val shapeless = "com.chuusai" %% "shapeless" % "2.3.10" val tla2tools = "org.lamport" % "tla2tools" % "1.7.0-SNAPSHOT" - val ujson = "com.lihaoyi" %% "ujson" % "3.1.2" - val upickle = "com.lihaoyi" %% "upickle" % "3.1.2" + val ujson = "com.lihaoyi" %% "ujson" % "3.1.3" + val upickle = "com.lihaoyi" %% "upickle" % "3.1.3" val z3 = "tools.aqua" % "z3-turnkey" % "4.12.2" val zio = "dev.zio" %% "zio" % zioVersion // Keep up to sync with version in plugins.sbt From 754013e4c36ae997f43d59721b5bd6148bd7ce1e Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Mon, 18 Sep 2023 14:53:29 -0400 Subject: [PATCH 06/11] Update actions/checkout version Addresses CI deprication warning ``` The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2 ``` --- .github/workflows/container.yml | 2 +- .github/workflows/deploy.yml | 2 +- .github/workflows/main.yml | 14 +++++++------- .github/workflows/prepare-release.yml | 4 ++-- .github/workflows/release.yml | 2 +- 5 files changed, 12 insertions(+), 12 deletions(-) diff --git a/.github/workflows/container.yml b/.github/workflows/container.yml index 82e24d76cf..8a67106a92 100644 --- a/.github/workflows/container.yml +++ b/.github/workflows/container.yml @@ -27,7 +27,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@v2 + uses: actions/checkout@v4 - name: Log in to the Container registry uses: docker/login-action@f054a8b539a109f9f41c372932f1ae047eff08c9 diff --git a/.github/workflows/deploy.yml b/.github/workflows/deploy.yml index 967133a0af..9dd9ca1efa 100644 --- a/.github/workflows/deploy.yml +++ b/.github/workflows/deploy.yml @@ -11,7 +11,7 @@ jobs: deploy: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v4 - name: Setup mdBook uses: peaceiris/actions-mdbook@v1 diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 4f2b746072..44ef7f7bdc 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -15,7 +15,7 @@ jobs: build-mdbook: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v4 - name: Setup mdBook uses: peaceiris/actions-mdbook@v1 @@ -30,7 +30,7 @@ jobs: format-check: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v4 - name: Set up JDK 17 uses: actions/setup-java@v1 with: @@ -43,7 +43,7 @@ jobs: APALACHE_FATAL_WARNINGS: true runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v4 - name: Set up JDK 17 uses: actions/setup-java@v1 with: @@ -56,7 +56,7 @@ jobs: APALACHE_FATAL_WARNINGS: true runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v4 - name: Set up JDK 17 uses: actions/setup-java@v2 with: @@ -87,7 +87,7 @@ jobs: matrix: operating-system: [ubuntu-latest, macos-latest] steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v4 - name: Set up JDK 17 uses: actions/setup-java@v2 with: @@ -129,7 +129,7 @@ jobs: - operating-system: macos-latest smt-encoding: arrays steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v4 - name: Cache local m2 repository uses: actions/cache@v2 with: @@ -166,7 +166,7 @@ jobs: docker-tests: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v4 - name: Cache nix store # Workaround for cache action not playing well with permissions # See https://github.com/actions/cache/issues/324 diff --git a/.github/workflows/prepare-release.yml b/.github/workflows/prepare-release.yml index 3f0c0bab12..59493365dd 100644 --- a/.github/workflows/prepare-release.yml +++ b/.github/workflows/prepare-release.yml @@ -26,8 +26,8 @@ jobs: GITHUB_TOKEN: ${{ secrets.APALACHE_BOT_TOKEN }} runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 - - uses: actions/setup-java@v1 + - uses: actions/checkout@v4 + - uses: actions/setup-java@v3 with: java-version: 17 - name: Configure Git diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 6e7433a631..9ffa073b3b 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -11,7 +11,7 @@ jobs: if: startsWith(github.event.pull_request.title, '[release]') && github.event.pull_request.merged == true runs-on: ubuntu-latest steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v4 with: # See https://github.com/actions/checkout/issues/124#issuecomment-606277160 ref: ${{ github.event.pull_request.head.ref }} From 0de0b9680ca9cbaad6400a634fbb702aeda230b1 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Mon, 18 Sep 2023 14:59:19 -0400 Subject: [PATCH 07/11] Update actions/setup-java Addresses CI deprecation warning ``` The following actions uses node12 which is deprecated and will be forced to run on node16: actions/setup-java@v2 ``` --- .github/workflows/main.yml | 8 ++++---- .github/workflows/release.yml | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 44ef7f7bdc..d4785da477 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -32,7 +32,7 @@ jobs: steps: - uses: actions/checkout@v4 - name: Set up JDK 17 - uses: actions/setup-java@v1 + uses: actions/setup-java@v3 with: java-version: 17 - name: Check formatting @@ -45,7 +45,7 @@ jobs: steps: - uses: actions/checkout@v4 - name: Set up JDK 17 - uses: actions/setup-java@v1 + uses: actions/setup-java@v3 with: java-version: 17 - name: Check scaladoc @@ -58,7 +58,7 @@ jobs: steps: - uses: actions/checkout@v4 - name: Set up JDK 17 - uses: actions/setup-java@v2 + uses: actions/setup-java@v3 with: distribution: temurin java-version: 17 @@ -89,7 +89,7 @@ jobs: steps: - uses: actions/checkout@v4 - name: Set up JDK 17 - uses: actions/setup-java@v2 + uses: actions/setup-java@v3 with: distribution: temurin java-version: 17 diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 9ffa073b3b..7d619d05f8 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -17,7 +17,7 @@ jobs: ref: ${{ github.event.pull_request.head.ref }} # We only need the two commits of the release prep branch fetch-depth: 2 - - uses: actions/setup-java@v1 + - uses: actions/setup-java@v3 with: java-version: 17 - name: Cut Release From 701efd17d34cfe98b29e55ff45b89684834983df Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Mon, 18 Sep 2023 15:35:25 -0400 Subject: [PATCH 08/11] We need the distribution for java setup --- .github/workflows/main.yml | 2 ++ .github/workflows/prepare-release.yml | 1 + .github/workflows/release.yml | 1 + build.sbt | 4 ++-- 4 files changed, 6 insertions(+), 2 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index d4785da477..0e07f8072a 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -34,6 +34,7 @@ jobs: - name: Set up JDK 17 uses: actions/setup-java@v3 with: + distribution: temurin java-version: 17 - name: Check formatting run: make fmt-check @@ -47,6 +48,7 @@ jobs: - name: Set up JDK 17 uses: actions/setup-java@v3 with: + distribution: temurin java-version: 17 - name: Check scaladoc run: sbt unidoc diff --git a/.github/workflows/prepare-release.yml b/.github/workflows/prepare-release.yml index 59493365dd..af6a92eda6 100644 --- a/.github/workflows/prepare-release.yml +++ b/.github/workflows/prepare-release.yml @@ -29,6 +29,7 @@ jobs: - uses: actions/checkout@v4 - uses: actions/setup-java@v3 with: + distribution: temurin java-version: 17 - name: Configure Git run: | diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 7d619d05f8..539e9127da 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -19,6 +19,7 @@ jobs: fetch-depth: 2 - uses: actions/setup-java@v3 with: + distribution: temurin java-version: 17 - name: Cut Release env: diff --git a/build.sbt b/build.sbt index af4414d61c..65796d8e7d 100644 --- a/build.sbt +++ b/build.sbt @@ -23,8 +23,8 @@ ThisBuild / organization := "at.forsyte" ThisBuild / scalaVersion := "2.13.12" // Add resolver for Sonatype OSS Snapshots and Releases Maven repository -ThisBuild / resolvers ++= Resolver.sonatypeOssRepos("snapshots") -ThisBuild / resolvers ++= Resolver.sonatypeOssRepos("releases") +ThisBuild / resolvers += Resolver.sonatypeRepo("snapshots") +ThisBuild / resolvers += Resolver.sonatypeRepo("releases") // Shared dependencies accross all sub projects ThisBuild / libraryDependencies ++= Seq( From 7303626a228b1b0ef2a0cf1c015e2206c42c6d6b Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Tue, 19 Sep 2023 04:05:24 -0400 Subject: [PATCH 09/11] Account for possible output in CLI server test (#2741) It's possible for output to be printed after the welcome message in these tests. This change accounts for that. --- test/tla/cli-integration-tests.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md index 4c452d605b..9594be21b3 100644 --- a/test/tla/cli-integration-tests.md +++ b/test/tla/cli-integration-tests.md @@ -3918,6 +3918,7 @@ up and output its welcome message, before killing it: $ apalache-mc server & pid=$! && sleep 3 && kill $pid ... The Apalache server is running on port 8822. Press Ctrl-C to stop. +... ``` ### server mode: server can be started at different port @@ -3926,6 +3927,7 @@ The Apalache server is running on port 8822. Press Ctrl-C to stop. $ apalache-mc server --port=8888 & pid=$! && sleep 3 && kill $pid ... The Apalache server is running on port 8888. Press Ctrl-C to stop. +... ``` ## quint input From dcbf03467cf4b0a58416c604c6db1624ac30291d Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Tue, 19 Sep 2023 10:04:29 -0400 Subject: [PATCH 10/11] Revert sonatype resolvers This shouldn't have made it in to my PR. --- build.sbt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/build.sbt b/build.sbt index 65796d8e7d..af4414d61c 100644 --- a/build.sbt +++ b/build.sbt @@ -23,8 +23,8 @@ ThisBuild / organization := "at.forsyte" ThisBuild / scalaVersion := "2.13.12" // Add resolver for Sonatype OSS Snapshots and Releases Maven repository -ThisBuild / resolvers += Resolver.sonatypeRepo("snapshots") -ThisBuild / resolvers += Resolver.sonatypeRepo("releases") +ThisBuild / resolvers ++= Resolver.sonatypeOssRepos("snapshots") +ThisBuild / resolvers ++= Resolver.sonatypeOssRepos("releases") // Shared dependencies accross all sub projects ThisBuild / libraryDependencies ++= Seq( From 281c66dd3b2dd394556985e211efa8b756c01780 Mon Sep 17 00:00:00 2001 From: Kukovec Date: Fri, 22 Sep 2023 12:24:04 +0200 Subject: [PATCH 11/11] `SparseOracle` refactor (#2744) * SparseOracle * rework --- .../aux/oracles/SparseOracle.scala | 51 ++++++++++ .../aux/oracles/TestSparseOracle.scala | 94 +++++++++++++++++++ 2 files changed, 145 insertions(+) create mode 100644 tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/SparseOracle.scala create mode 100644 tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestSparseOracle.scala diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/SparseOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/SparseOracle.scala new file mode 100644 index 0000000000..55c9255f41 --- /dev/null +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/SparseOracle.scala @@ -0,0 +1,51 @@ +package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.oracles + +import at.forsyte.apalache.tla.bmcmt.smt.SolverContext +import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope +import at.forsyte.apalache.tla.typecomp.TBuilderInstruction +import at.forsyte.apalache.tla.types.tla + +/** + * Given a set `indices` of size `N`, sparse oracle is able to answer {{{chosenValueIsEqualToIndexedValue(_, i),}}} for + * any `i \in indices`, despite having a size, which may be smaller than some (ot all) elements of `indices`. + * {{{chosenValueIsEqualToIndexedValue(_, j),}}} for any `j` not in `indices` does not hold. + * + * Internally, every SparseOracle `s` maintains an oracle `o` of size `N-1`, such that for every scope `X`, and any + * index `i \in indices` the following holds: + * {{{s.chosenValueIsEqualToIndexedValue(X,i) = o.chosenValueIsEqualToIndexedValue(x, idxMap(i),}}} where `idxMap` is + * some bijection from `indices` to `{0,...,N-1}`. + * + * @author + * Jure Kukovec + * + * @param mkOracle + * the method to create the backend oracle, of a given size + * @param values + * the set S of oracle values + */ +class SparseOracle(mkOracle: Int => Oracle, val values: Set[Int]) extends Oracle { + private[oracles] val oracle = mkOracle(values.size) + private[oracles] val sortedValues: Seq[Int] = values.toSeq.sorted + private[oracles] val indexMap: Map[Int, Int] = Map(sortedValues.zipWithIndex: _*) + + override def size: Int = values.size + + def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): TBuilderInstruction = + indexMap + .get(index.toInt) + .map { + oracle.chosenValueIsEqualToIndexedValue(scope, _) + } + .getOrElse(tla.bool(false)) + + override def caseAssertions( + scope: RewriterScope, + assertions: Seq[TBuilderInstruction], + elseAssertionsOpt: Option[Seq[TBuilderInstruction]] = None): TBuilderInstruction = + oracle.caseAssertions(scope, assertions, elseAssertionsOpt) + + override def getIndexOfChosenValueFromModel(solverContext: SolverContext): BigInt = { + val oracleIdx = oracle.getIndexOfChosenValueFromModel(solverContext).toInt + sortedValues.applyOrElse[Int, Int](oracleIdx, _ => -1) + } +} diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestSparseOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestSparseOracle.scala new file mode 100644 index 0000000000..887557bfbb --- /dev/null +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestSparseOracle.scala @@ -0,0 +1,94 @@ +package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.oracles + +import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter +import at.forsyte.apalache.tla.bmcmt.smt.{SolverConfig, Z3SolverContext} +import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope +import at.forsyte.apalache.tla.bmcmt.types.CellT +import at.forsyte.apalache.tla.bmcmt.{ArenaCell, PureArena} +import at.forsyte.apalache.tla.lir._ +import at.forsyte.apalache.tla.typecomp.TBuilderInstruction +import at.forsyte.apalache.tla.types.tla +import org.junit.runner.RunWith +import org.scalacheck.Gen +import org.scalacheck.Prop.forAll +import org.scalatest.BeforeAndAfterEach +import org.scalatest.funsuite.AnyFunSuite +import org.scalatestplus.junit.JUnitRunner +import org.scalatestplus.scalacheck.Checkers + +@RunWith(classOf[JUnitRunner]) +class TestSparseOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers { + + var initScope: RewriterScope = RewriterScope.initial() + var intOracleCell: ArenaCell = PureArena.cellInvalid + + def mkIntOracle(n: Int): Oracle = new IntOracle(intOracleCell, n) + + override def beforeEach(): Unit = { + val scope0 = RewriterScope.initial() + initScope = scope0.copy(arena = scope0.arena.appendCell(CellT.fromType1(IntT1))) + intOracleCell = initScope.arena.topCell + } + + val intGen: Gen[Int] = Gen.choose(-10, 10) + val nonNegIntGen: Gen[Int] = Gen.choose(0, 20) + + val setGen: Gen[Set[Int]] = for { + maxSize <- nonNegIntGen + elems <- Gen.listOfN(maxSize, nonNegIntGen) + } yield elems.toSet + + val nonemptySetAndIdxGen: Gen[(Set[Int], Int)] = for { + maxSize <- Gen.choose(1, 20) + elems <- Gen.listOfN(maxSize, nonNegIntGen) + idx <- Gen.oneOf(elems) + } yield (elems.toSet, idx) + + test("chosenValueIsEqualToIndexedValue returns the correct value for any element of the constructor set") { + val prop = + forAll(Gen.zip(setGen, intGen)) { case (set, index) => + val oracle = new SparseOracle(mkIntOracle, set) + val cmp: TlaEx = oracle.chosenValueIsEqualToIndexedValue(initScope, index) + if (!set.contains(index)) + cmp == tla.bool(false).build + else { + cmp == oracle.oracle.chosenValueIsEqualToIndexedValue(initScope, oracle.indexMap(index)).build + } + } + + check(prop, minSuccessful(1000), sizeRange(4)) + } + + val (assertionsA, assertionsB): (Seq[TBuilderInstruction], Seq[TBuilderInstruction]) = 0 + .to(10) + .map { i => + (tla.name(s"A$i", BoolT1), tla.name(s"B$i", BoolT1)) + } + .unzip + + // "caseAssertions" tests ignored, since SparseOracle literally just invokes the underlying oracle's method, + // which should have its own tests + + // We cannot test getIndexOfChosenValueFromModel without running the solver + test("getIndexOfChosenValueFromModel recovers the index correctly") { + val ctx = new Z3SolverContext(SolverConfig.default) + val paa = PureArenaAdapter.create(ctx) // We use PAA, since it performs the basic context initialization + val paa2 = paa.appendCell(IntT1) // also declares the cell + intOracleCell = paa2.topCell + initScope = initScope.copy(arena = paa2.arena) + val prop = + forAll(nonemptySetAndIdxGen) { case (set, index) => + val oracle = new SparseOracle(mkIntOracle, set) + val eql = oracle.chosenValueIsEqualToIndexedValue(initScope, index) + ctx.push() + ctx.assertGroundExpr(eql) + ctx.sat() + val ret = oracle.getIndexOfChosenValueFromModel(ctx) == index + ctx.pop() + ret + } + + // 1000 is too many, since each run invokes the solver + check(prop, minSuccessful(80), sizeRange(4)) + } +}