diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs index 05d4c13a59..71e9c75789 100644 --- a/.git-blame-ignore-revs +++ b/.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 diff --git a/.github/workflows/README.md b/.github/workflows/README.md index b3226f8407..49339e90ce 100644 --- a/.github/workflows/README.md +++ b/.github/workflows/README.md @@ -9,22 +9,22 @@ - 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) - 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) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 43f314e500..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 diff --git a/.github/workflows/prepare-release.yml b/.github/workflows/prepare-release.yml index ba77106216..fa189eb981 100644 --- a/.github/workflows/prepare-release.yml +++ b/.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, diff --git a/.scalafmt.conf b/.scalafmt.conf index 11af66aa14..2f274e9290 100644 --- a/.scalafmt.conf +++ b/.scalafmt.conf @@ -1,4 +1,4 @@ -version = "3.8.0" +version = "3.8.3" runner.dialect = scala213 fileOverride { diff --git a/CHANGES.md b/CHANGES.md index e370b63d49..c4b2efee68 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,24 @@ +## 0.45.3 - 2024-08-21 + +### Features + +- Added scope-unsafe builder. + +## 0.45.2 - 2024-08-19 + +## 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 diff --git a/FUNDING.md b/FUNDING.md new file mode 100644 index 0000000000..7d6cffe670 --- /dev/null +++ b/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/ 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/README.md b/README.md index 8e119886b2..a238a32b39 100644 --- a/README.md +++ b/README.md @@ -3,7 +3,7 @@ src="https://raw.githubusercontent.com/informalsystems/apalache/99e58d6f5eebcc41f432a126a13a5f8d2ae7afe6/logo-apalache.svg" alt="Apalache Logo"> -

APALACHE

+

APALACHE

A symbolic model checker for TLA+

@@ -11,8 +11,8 @@ alt="Apalache Logo"> [![main badge][]][main-ci] -[main badge]: https://github.com/informalsystems/apalache/workflows/build/badge.svg?branch=main -[main-ci]: https://github.com/informalsystems/apalache/actions?query=branch%3Amain+workflow%3Abuild +[main badge]: https://github.com/apalache-mc/apalache/workflows/build/badge.svg?branch=main +[main-ci]: https://github.com/apalache-mc/apalache/actions?query=branch%3Amain+workflow%3Abuild Apalache translates [TLA+] into the logic supported by SMT solvers such as [Microsoft Z3]. Apalache can check inductive invariants (for fixed or bounded @@ -28,7 +28,7 @@ course]. Check the [releases page][] for our latest release. For a stable release, we recommend that you pull the latest docker image with -`docker pull ghcr.io/informalsystems/apalache:main`, use the jar from the +`docker pull ghcr.io/apalache-mc/apalache:main`, use the jar from the most recent release, or checkout the source code from the most recent release tag. @@ -49,10 +49,10 @@ manual][user-manual-installation]. ## Website -Our current website is served at https://apalache.informal.systems . +Our current website is served at https://apalache-mc.org . The site is hosted by github, and changes can be made through PRs into the -[gh-pages](https://github.com/informalsystems/apalache/tree/gh-pages) branch of +[gh-pages](https://github.com/apalache-mc/apalache/tree/gh-pages) branch of this repository. See the README.md on that branch for more information. The user documentation is automatically deployed to the website branch as per @@ -72,11 +72,11 @@ knowing too much about the internals of Apalache. Solving these issues would improve usability! Please comment in the relevant issue, if you are going to solve it. -- Writing annotations in the JSON format: [#804](https://github.com/informalsystems/apalache/issues/804) -- Add support for VIEW in the TLC config: [#851](https://github.com/informalsystems/apalache/issues/851) +- Writing annotations in the JSON format: [#804](https://github.com/apalache-mc/apalache/issues/804) +- Add support for VIEW in the TLC config: [#851](https://github.com/apalache-mc/apalache/issues/851) - Translate `\E x \in STRING: P` and `\A x \in STRING: P`: - [#844](https://github.com/informalsystems/apalache/issues/844) -- Interval analysis for `a..b`: [#446](https://github.com/informalsystems/apalache/issues/446) + [#844](https://github.com/apalache-mc/apalache/issues/844) +- Interval analysis for `a..b`: [#446](https://github.com/apalache-mc/apalache/issues/446) ## Industrial examples @@ -142,27 +142,27 @@ Past funding from [Der Wiener Wissenschafts-, Forschungs- und Technologiefonds]( [tla+]: http://lamport.azurewebsites.net/tla/tla.html [microsoft z3]: https://github.com/Z3Prover/z3 -[supported features]: https://apalache.informal.systems/docs/apalache/features.html +[supported features]: https://apalache-mc.org/docs/apalache/features.html [tlc]: http://lamport.azurewebsites.net/tla/tools.html [leslie lamport's page on tla+]: http://lamport.azurewebsites.net/tla/tla.html [video course]: http://lamport.azurewebsites.net/video/videos.html -[releases page]: https://github.com/informalsystems/apalache/releases -[master]: https://github.com/informalsystems/apalache/tree/master -[main branch]: https://github.com/informalsystems/apalache/tree/main +[releases page]: https://github.com/apalache-mc/apalache/releases +[master]: https://github.com/apalache-mc/apalache/tree/master +[main branch]: https://github.com/apalache-mc/apalache/tree/main [apalache zulip stream]: https://informal-systems.zulipchat.com/#narrow/stream/265309-apalache [tendermint specs]: https://github.com/tendermint/tendermint/tree/master/spec/light-client/accountability [tendermint blockchain]: https://github.com/tendermint [standard repository of tla+ examples]: https://github.com/tlaplus/Examples -[apalache benchmarks]: https://github.com/informalsystems/apalache-tests -[checking inductive invariants]: https://github.com/informalsystems/apalache-tests/blob/master/results/001indinv-report.md -[bounded model checking]: https://github.com/informalsystems/apalache-tests/blob/master/results/002bmc-report.md -[user-manual]: http://informalsystems.github.io/apalache/docs/index.html -[user-manual-docker]: https://apalache.informal.systems/docs/apalache/installation/docker.html -[user-manual-installation]: https://apalache.informal.systems/docs/apalache/installation/index.html -[language-manual]: https://apalache.informal.systems/docs/lang/index.html -[idioms]: https://apalache.informal.systems//docs/idiomatic/index.html +[apalache benchmarks]: https://github.com/apalache-mc/apalache-tests +[checking inductive invariants]: https://github.com/apalache-mc/apalache-tests/blob/master/results/001indinv-report.md +[bounded model checking]: https://github.com/apalache-mc/apalache-tests/blob/master/results/002bmc-report.md +[user-manual]: http://apalache-mc.org/docs/index.html +[user-manual-docker]: https://apalache-mc.org/docs/apalache/installation/docker.html +[user-manual-installation]: https://apalache-mc.org/docs/apalache/installation/index.html +[language-manual]: https://apalache-mc.org/docs/lang/index.html +[idioms]: https://apalache-mc.org/docs/idiomatic/index.html [light client specs]: https://github.com/tendermint/tendermint/tree/master/spec/light-client/verification [model-based testing]: https://github.com/informalsystems/tendermint-rs/tree/master/light-client/tests/support/model_based#light-client-model-based-testing-guide -[apalache.informal.systems]: https://apalache.informal.systems +[apalache-mc.org]: https://apalache-mc.org [TLA-Apalache workshop]: https://github.com/informalsystems/tla-apalache-workshop -[Beginner's tutorial]: https://apalache.informal.systems/docs/tutorials/entry-tutorial.html +[Beginner's tutorial]: https://apalache-mc.org/docs/tutorials/entry-tutorial.html diff --git a/VERSION b/VERSION index 93722f80fa..94212986a1 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -0.44.12-SNAPSHOT +0.45.4-SNAPSHOT diff --git a/build.sbt b/build.sbt index 83145fae79..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 @@ -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.13" +ThisBuild / scalaVersion := "2.13.14" // Add resolver for Sonatype OSS Snapshots and Releases Maven repository ThisBuild / resolvers ++= Resolver.sonatypeOssRepos("snapshots") @@ -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/docs/src/apalache/tuning.md b/docs/src/apalache/tuning.md index d3a60c5eeb..22aa77b99a 100644 --- a/docs/src/apalache/tuning.md +++ b/docs/src/apalache/tuning.md @@ -22,14 +22,6 @@ The following options are supported: `smt.randomSeed=` passes the random seed to `z3` (via `z3`'s parameters `sat.random_seed` and `smt.random_seed`). -## Timeouts - -`search.smt.timeout=` 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 diff --git a/docs/src/lang/apalache-operators.md b/docs/src/lang/apalache-operators.md index 7166c4fc8a..41d1a8c81e 100644 --- a/docs/src/lang/apalache-operators.md +++ b/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). ---------------------------------------------------------------------------- + +## 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 +``` +---------------------------------------------------------------------------- ## Convert a set of pairs to a function diff --git a/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala b/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala index 4d676aa3c4..201e26ae1a 100644 --- a/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala +++ b/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, diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala index ea957e1bce..20a5773436 100644 --- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala +++ b/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( diff --git a/project/Dependencies.scala b/project/Dependencies.scala index 5c0269f1ce..04e04f7967 100644 --- a/project/Dependencies.scala +++ b/project/Dependencies.scala @@ -12,7 +12,7 @@ object Dependencies { object Deps { // Versions - lazy val logbackVersion = "1.5.3" + lazy val logbackVersion = "1.5.7" lazy val clistVersion = "3.5.1" // Libraries @@ -20,27 +20,27 @@ object Dependencies { 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 commonsIo = "commons-io" % "commons-io" % "2.15.1" + 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 pureConfig = "com.github.pureconfig" %% "pureconfig" % "0.17.7" + 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.12" - val shapeless = "com.chuusai" %% "shapeless" % "2.3.10" + val slf4j = "org.slf4j" % "slf4j-api" % "2.0.16" + val shapeless = "com.chuusai" %% "shapeless" % "2.3.12" 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.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" - 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) @@ -53,8 +53,8 @@ object Dependencies { object TestDeps { // 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 scalacheck = "org.scalacheck" %% "scalacheck" % "1.18.0" % Test + val easymock = "org.easymock" % "easymock" % "5.4.0" % Test val scalaTestVersion = "3.2.15" val scalatest = "org.scalatest" %% "scalatest" % scalaTestVersion % Test diff --git a/project/build.properties b/project/build.properties index 04267b14af..ee4c672cd0 100644 --- a/project/build.properties +++ b/project/build.properties @@ -1 +1 @@ -sbt.version=1.9.9 +sbt.version=1.10.1 diff --git a/project/plugins.sbt b/project/plugins.sbt index b82576ce65..9471def939 100644 --- a/project/plugins.sbt +++ b/project/plugins.sbt @@ -5,13 +5,13 @@ addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "1.2.0") // https://github.com/marcuslonnberg/sbt-docker addSbtPlugin("se.marcuslonnberg" % "sbt-docker" % "1.11.0") // https://github.com/scoverage/sbt-scoverage -addSbtPlugin("org.scoverage" % "sbt-scoverage" % "2.0.11") +addSbtPlugin("org.scoverage" % "sbt-scoverage" % "2.1.0") // 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.9.16") +addSbtPlugin("com.github.sbt" % "sbt-native-packager" % "1.10.4") // https://scalacenter.github.io/scalafix/docs/users/installation.html -addSbtPlugin("ch.epfl.scala" % "sbt-scalafix" % "0.12.0") +addSbtPlugin("ch.epfl.scala" % "sbt-scalafix" % "0.12.1") // https://scalapb.github.io/zio-grpc/docs/installation addSbtPlugin("com.thesamet" % "sbt-protoc" % "1.0.6") // https://github.com/sbt/sbt-unidoc @@ -21,7 +21,7 @@ addSbtPlugin("com.github.sbt" % "sbt-unidoc" % "0.5.0") val zioGrpcVersion = "0.5.3" libraryDependencies ++= Seq( "com.thesamet.scalapb.zio-grpc" %% "zio-grpc-codegen" % zioGrpcVersion, - "com.thesamet.scalapb" %% "compilerplugin" % "0.11.15", + "com.thesamet.scalapb" %% "compilerplugin" % "0.11.17", ) // Add the locally defined plugins diff --git a/project/sbt-changeling/build.sbt b/project/sbt-changeling/build.sbt index 2d86b9cb52..2df02ef524 100644 --- a/project/sbt-changeling/build.sbt +++ b/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(".")) diff --git a/project/sbt-changeling/project/build.properties b/project/sbt-changeling/project/build.properties index 04267b14af..ee4c672cd0 100644 --- a/project/sbt-changeling/project/build.properties +++ b/project/sbt-changeling/project/build.properties @@ -1 +1 @@ -sbt.version=1.9.9 +sbt.version=1.10.1 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/src/tla/Apalache.tla b/src/tla/Apalache.tla index b8bb5cb1c5..ea5188fb9b 100644 --- a/src/tla/Apalache.tla +++ b/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) + =============================================================================== diff --git a/test/tla/Repeat.tla b/test/tla/Repeat.tla new file mode 100644 index 0000000000..93aa7adda9 --- /dev/null +++ b/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 + +=============================================================================== diff --git a/test/tla/RepeatBad.tla b/test/tla/RepeatBad.tla new file mode 100644 index 0000000000..3951d35d80 --- /dev/null +++ b/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 +=============================================================================== diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md index 6cec251917..cfa06d6d28 100644 --- a/test/tla/cli-integration-tests.md +++ b/test/tla/cli-integration-tests.md @@ -894,6 +894,24 @@ The outcome is: NoError EXITCODE: OK ``` +### check Repeat succeeds + +```sh +$ apalache-mc check --inv=Inv --length=0 Repeat.tla | sed 's/I@.*//' +... +The outcome is: NoError +... +EXITCODE: OK +``` + +### check RepeatBad fails + +```sh +$ apalache-mc check --inv=Inv --length=0 RepeatBad.tla | sed 's/I@.*//' +... +EXITCODE: ERROR (255) +``` + ### check Counter.tla errors (array-encoding) ```sh @@ -1752,6 +1770,18 @@ The outcome is: NoError EXITCODE: OK ``` +### simulate Paxos.tla with timeout succeeds + +While we cannot rely on an actual timeout happening or not, we can make sure that the option is properly parsed. + +```sh +$ apalache-mc simulate --timeout-smt=1 --length=10 --inv=Inv Paxos.tla | sed 's/I@.*//' +... +The outcome is: NoError +... +EXITCODE: OK +``` + ### simulate y2k with --output-traces succeeds ```sh @@ -3874,6 +3904,7 @@ checker { smt-encoding { type=oopsla-19 } + timeout-smt-sec=0 tuning { "search.outputTraces"="false" } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Checker.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Checker.scala index 1723856d11..8bef8a9b07 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Checker.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Checker.scala @@ -23,6 +23,8 @@ object Checker { Obj("checking_result" -> "Error", "counterexamples" -> counterexamples, "nerrors" -> nerrors) case Deadlock(counterexample) => Obj("checking_result" -> "Deadlock", "counterexamples" -> counterexample.toList) + case SmtTimeout(nTimeouts) => + Obj("checking_result" -> "SmtTimeout", "ntimeouts" -> nTimeouts) case other => Obj("checking_result" -> other.toString()) } @@ -60,6 +62,20 @@ object Checker { override val isOk: Boolean = true } + /** + * The SMT solver reported a timeout. It should still be possible to check other verification conditions. + * @param nTimeouts + * the number of timeouts, normally, just 1. + */ + case class SmtTimeout(nTimeouts: Int) extends CheckerResult { + override def toString: String = "SmtTimeout" + + /** + * Whether this result shall be reported as success (`true`) or error (`false`). + */ + override val isOk: Boolean = true + } + case class Interrupted() extends CheckerResult { override def toString: String = "Interrupted" diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala index e50e21db89..b4d09c0825 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala @@ -8,8 +8,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._ import at.forsyte.apalache.tla.bmcmt.rules.aux.{ProtoSeqOps, RecordAndVariantOps} import at.forsyte.apalache.tla.bmcmt.types._ import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} import scalaz.unused import scala.collection.immutable.SortedMap @@ -41,7 +40,7 @@ class LazyEquality(rewriter: SymbStateRewriter) * @return * tla.eql(left, right), provided that left and right can be compared */ - def safeEq(left: ArenaCell, right: ArenaCell): TBuilderInstruction = { + def safeEq(left: ArenaCell, right: ArenaCell): BuilderT = { if (left == right) { tla.bool(true) // this is just true } else { @@ -319,14 +318,14 @@ class LazyEquality(rewriter: SymbStateRewriter) // inAndEq checks if lelem is in right val inAndEqList = rightElems.map(inAndEq(rewriter, _, lelem, right, lazyEq = true)) // There are plenty of valid subformulas. Simplify! - tla.or(inAndEqList: _*).map(simplifier.simplifyShallow) + simplifier.applySimplifyShallowToBuilderEx(tla.or(inAndEqList: _*)) } def notInOrExists(lelem: ArenaCell) = { val notInOrExists = - tla - .or(tla.not(tla.selectInSet(lelem.toBuilder, left.toBuilder)), exists(lelem)) - .map(simplifier.simplifyShallow) + simplifier.applySimplifyShallowToBuilderEx( + tla.or(tla.not(tla.selectInSet(lelem.toBuilder, left.toBuilder)), exists(lelem)) + ) if (simplifier.isBoolConst(notInOrExists)) { notInOrExists // just return the constant @@ -340,7 +339,8 @@ class LazyEquality(rewriter: SymbStateRewriter) } } - val forEachNotInOrExists = tla.and(leftElems.map(notInOrExists): _*).map(simplifier.simplifyShallow) + val forEachNotInOrExists = + simplifier.applySimplifyShallowToBuilderEx(tla.and(leftElems.map(notInOrExists): _*)) newState = newState.updateArena(_.appendCell(BoolT1)) val pred = newState.arena.topCell rewriter.solverContext.assertGroundExpr(tla.eql(pred.toBuilder, forEachNotInOrExists)) @@ -471,7 +471,7 @@ class LazyEquality(rewriter: SymbStateRewriter) val commonKeys = leftType.fieldTypes.keySet.intersect(rightType.fieldTypes.keySet) var newState = state - def keyEq(key: String): TBuilderInstruction = { + def keyEq(key: String): BuilderT = { val leftIndex = leftType.fieldTypes.keySet.toList.indexOf(key) val rightIndex = rightType.fieldTypes.keySet.toList.indexOf(key) @@ -522,7 +522,7 @@ class LazyEquality(rewriter: SymbStateRewriter) leftRec: ArenaCell, rightRec: ArenaCell): SymbState = { var nextState = state - def fieldsEq(name: String): TBuilderInstruction = { + def fieldsEq(name: String): BuilderT = { val leftField = recordOps.getField(nextState.arena, leftRec, name) val rightField = recordOps.getField(nextState.arena, rightRec, name) // The field values may be non-basic expressions. Use lazy equality over them too. @@ -545,7 +545,7 @@ class LazyEquality(rewriter: SymbStateRewriter) val leftTag = recordOps.getVariantTag(nextState.arena, leftVar) val rightTag = recordOps.getVariantTag(nextState.arena, rightVar) - def valuesEq(tagName: String): TBuilderInstruction = { + def valuesEq(tagName: String): BuilderT = { val leftValue = recordOps.getUnsafeVariantValue(nextState.arena, leftVar, tagName) val rightValue = recordOps.getUnsafeVariantValue(nextState.arena, rightVar, tagName) // The field values may be non-basic expressions. Use lazy equality over them too. @@ -569,7 +569,7 @@ class LazyEquality(rewriter: SymbStateRewriter) private def mkTupleEq(state: SymbState, left: ArenaCell, right: ArenaCell): SymbState = { var newState = state - def elemEq(lelem: ArenaCell, relem: ArenaCell): TBuilderInstruction = { + def elemEq(lelem: ArenaCell, relem: ArenaCell): BuilderT = { newState = cacheOneEqConstraint(newState, lelem, relem) safeEq(lelem, relem) } @@ -602,7 +602,7 @@ class LazyEquality(rewriter: SymbStateRewriter) val len1Ex = len1.toBuilder val len2Ex = len2.toBuilder - def eqPairwise(indexBase1: Int, cells: (ArenaCell, ArenaCell)): TBuilderInstruction = { + def eqPairwise(indexBase1: Int, cells: (ArenaCell, ArenaCell)): BuilderT = { nextState = cacheOneEqConstraint(nextState, cells._1, cells._2) // Either (1) one of the lengths is below the index, or (2) the elements are equal. // The case (1) is compensated with the constraint sizesEq below. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala index e7360504ff..1d96cdf622 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala @@ -10,8 +10,8 @@ import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper.{TlaBoolOper, TlaOper} import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker import at.forsyte.apalache.tla.lir.transformations.standard.ReplaceFixed -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.typecomp._ +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} import com.typesafe.scalalogging.LazyLogging import scala.util.Random @@ -94,7 +94,7 @@ class SeqModelChecker[ExecutorContextT]( */ private def outputExampleRun(): Unit = { logger.info("Constructing an example run") - trex.sat(params.smtTimeoutSec) match { + trex.sat(params.timeoutSmtSec) match { case Some(true) => listeners.foreach(_.onExample(checkerInput.rootModule, trex.decodedExecution(), searchState.nRunsLeft)) case Some(false) => @@ -128,8 +128,8 @@ class SeqModelChecker[ExecutorContextT]( if (!params.discardDisabled && params.checkForDeadlocks) { // We do this check only if all transitions are unconditionally enabled. // Otherwise, we should have found it already. - logger.info(s"Step %d: checking for deadlocks".format(trex.stepNo)) - trex.sat(params.smtTimeoutSec) match { + logger.info(f"Step ${trex.stepNo}: checking for deadlocks") + trex.sat(params.timeoutSmtSec) match { case Some(true) => () // OK case Some(false) => @@ -145,7 +145,8 @@ class SeqModelChecker[ExecutorContextT]( searchState.onResult(Deadlock(counterexample)) case None => - searchState.onResult(RuntimeError()) + logger.info(f"Step ${trex.stepNo}: checking for deadlocks => TIMEOUT") + searchState.onResult(SmtTimeout(1)) } } @@ -204,6 +205,9 @@ class SeqModelChecker[ExecutorContextT]( val transitionIndices = if (params.isRandomSimulation) Random.shuffle(transitions.indices.toList) else transitions.indices + // keep track of SMT timeouts + var nTimeouts = 0 + for (no <- transitionIndices) { var snapshot: Option[SnapshotT] = None if (params.discardDisabled) { @@ -221,7 +225,7 @@ class SeqModelChecker[ExecutorContextT]( val assumeSnapshot = trex.snapshot() // assume that the transition is fired and check, whether the constraints are satisfiable trex.assumeTransition(no) - trex.sat(params.smtTimeoutSec) match { + trex.sat(params.timeoutSmtSec) match { case Some(true) => logger.debug(s"Step ${trex.stepNo}: Transition #$no is enabled") // recover to the state before the transition was fired @@ -263,7 +267,8 @@ class SeqModelChecker[ExecutorContextT]( case None => if (params.isRandomSimulation) { - logger.info(s"Step ${trex.stepNo}: Transition #$no enabledness is UNKNOWN; assuming it is disabled") + logger.info(s"Step ${trex.stepNo}: Transition #$no => TIMEOUT. Transition ignored.") + nTimeouts += 1 } else { searchState.onResult(RuntimeError()) return (Set.empty, Set.empty) // UNKNOWN or timeout @@ -284,7 +289,13 @@ class SeqModelChecker[ExecutorContextT]( } if (trex.preparedTransitionNumbers.isEmpty) { - if (params.checkForDeadlocks) { + if (nTimeouts > 0 || !params.checkForDeadlocks) { + // Either (1) there were timeouts, and we cannot claim to have found a deadlock, + // or (2) the user does not care about deadlocks + val msg = "All executions are shorter than the provided bound." + logger.warn(msg) + searchState.onResult(ExecutionsTooShort()) + } else { val counterexample = if (trex.sat(0).contains(true)) { val cx = Counterexample(checkerInput.rootModule, trex.decodedExecution(), tla.bool(true)) notifyOnError(cx, searchState.nFoundErrors) @@ -295,10 +306,6 @@ class SeqModelChecker[ExecutorContextT]( None } searchState.onResult(Deadlock(counterexample)) - } else { - val msg = "All executions are shorter than the provided bound." - logger.warn(msg) - searchState.onResult(ExecutionsTooShort()) } (Set.empty, Set.empty) } else { @@ -355,7 +362,7 @@ class SeqModelChecker[ExecutorContextT]( // check the invariant trex.assertState(notInv) - trex.sat(params.smtTimeoutSec) match { + trex.sat(params.timeoutSmtSec) match { case Some(true) => val counterexample = Counterexample(checkerInput.rootModule, trex.decodedExecution(), notInv) searchState.onResult(Error(1, Seq(counterexample))) @@ -369,8 +376,10 @@ class SeqModelChecker[ExecutorContextT]( logger.info(f"State ${stateNo}: ${kind} invariant ${invNo} holds.") case None => - // UNKNOWN or timeout - searchState.onResult(RuntimeError()) + // UNKNOWN or timeout. Assume that the invariant holds true, so we can continue. + invariantHolds = true + logger.info(f"State ${stateNo}: ${kind} invariant ${invNo} => TIMEOUT. Assuming it holds true.") + searchState.onResult(SmtTimeout(1)) } // rollback the context @@ -401,7 +410,7 @@ class SeqModelChecker[ExecutorContextT]( val traceInvApp = applyTraceInv(notInv) trex.assertState(traceInvApp) - trex.sat(params.smtTimeoutSec) match { + trex.sat(params.timeoutSmtSec) match { case Some(true) => val counterexample = Counterexample(checkerInput.rootModule, trex.decodedExecution(), traceInvApp) searchState.onResult(Error(1, Seq(counterexample))) @@ -415,7 +424,10 @@ class SeqModelChecker[ExecutorContextT]( invariantHolds = true case None => - searchState.onResult(RuntimeError()) + // Timeout. Assume that the invariant holds true, so we can continue. + invariantHolds = true + logger.info(f"State ${stateNo}: trace invariant ${invNo} => TIMEOUT. Assuming it holds true.") + searchState.onResult(SmtTimeout(1)) } // rollback the context @@ -430,7 +442,7 @@ class SeqModelChecker[ExecutorContextT]( val stateType = RecT1(checkerInput.rootModule.varDeclarations.map(d => d.name -> d.typeTag.asTlaType1()): _*) // convert a variable binding to a record - def mkRecord(b: Binding): TBuilderInstruction = { + def mkRecord(b: Binding): BuilderT = { val ctorArgs = b.toMap.map { case (key, value) => (key, tla.name(value.toString, stateType.fieldTypes(key))) } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala index 974aab97e7..ca4f5ba709 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala @@ -8,8 +8,8 @@ import at.forsyte.apalache.tla.bmcmt.types._ import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper.TlaSetOper import at.forsyte.apalache.tla.lir.values._ -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} +import at.forsyte.apalache.tla.typecomp._ import com.typesafe.scalalogging.LazyLogging import scala.collection.immutable.SortedMap @@ -24,16 +24,21 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter private val protoSeqOps = new ProtoSeqOps(rewriter) private val recordOps = new RecordAndVariantOps(rewriter) + def evalGroundExprForBuilderEx(ex: TBuilderInstruction): TBuilderInstruction = + ex.map(solverContext.evalGroundExpr) // when using TBuilderInstruction + def evalGroundExprForBuilderEx(ex: TlaEx): TlaEx = + solverContext.evalGroundExpr(ex) // when using TlaEx + def decodeStateVariables(state: SymbState): Map[String, TlaEx] = { state.binding.toMap.map(p => (p._1, reverseMapVar(decodeCellToTlaEx(state.arena, p._2), p._1, p._2))) } - def decodeCellToTlaEx(arena: PureArenaAdapter, cell: ArenaCell): TBuilderInstruction = cell.cellType match { + def decodeCellToTlaEx(arena: PureArenaAdapter, cell: ArenaCell): BuilderT = cell.cellType match { case CellTFrom(BoolT1) => - cell.toBuilder.map(solverContext.evalGroundExpr) + evalGroundExprForBuilderEx(cell.toBuilder) case CellTFrom(IntT1) => - cell.toBuilder.map(solverContext.evalGroundExpr) + evalGroundExprForBuilderEx(cell.toBuilder) case ct @ CellTFrom(StrT1 | ConstT1(_)) => // First, attempt to check the cache @@ -128,7 +133,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter throw new RewriterException("Don't know how to decode the cell %s of type %s".format(cell, cell.cellType), NullEx) } - private def decodeOldRecordToTlaEx(arena: PureArenaAdapter, cell: ArenaCell, recordT: RecT1): TBuilderInstruction = { + private def decodeOldRecordToTlaEx(arena: PureArenaAdapter, cell: ArenaCell, recordT: RecT1): BuilderT = { def exToStr(ex: TlaEx): TlaStr = ex match { case ValEx(s @ TlaStr(_)) => s case _ => throw new RewriterException("Expected a string, found: " + ex, ex) @@ -141,7 +146,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter val fieldValues = arena.getHas(cell) val keyList = recordT.fieldTypes.keySet.toList - def eachField(es: List[TBuilderInstruction], key: String): List[TBuilderInstruction] = { + def eachField(es: List[BuilderT], key: String): List[BuilderT] = { if (!dom.contains(TlaStr(key))) { es // skip } else { @@ -151,7 +156,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter } } - val keysAndValues = keyList.reverse.foldLeft(List.empty[TBuilderInstruction])(eachField) + val keysAndValues = keyList.reverse.foldLeft(List.empty[BuilderT])(eachField) if (keysAndValues.nonEmpty) { tla.recMixed(keysAndValues: _*) } else { @@ -165,7 +170,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter private def decodeRecordToTlaEx( arena: PureArenaAdapter, cell: ArenaCell, - fieldTypes: SortedMap[String, TlaType1]): TBuilderInstruction = + fieldTypes: SortedMap[String, TlaType1]): BuilderT = tla.rowRec(None, fieldTypes.keySet.toList.map { k => k -> decodeCellToTlaEx(arena, recordOps.getField(arena, cell, k)) @@ -174,7 +179,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter private def decodeVariantToTlaEx( arena: PureArenaAdapter, cell: ArenaCell, - options: SortedMap[String, TlaType1]): TBuilderInstruction = { + options: SortedMap[String, TlaType1]): BuilderT = { val tagName = decodeCellToTlaEx(arena, recordOps.getVariantTag(arena, cell)).build match { case ValEx(TlaStr(name)) => name @@ -184,7 +189,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter tla.variant(tagName, value, VariantT1(RowT1(options, None))) } - private def decodeFunToTlaEx(arena: PureArenaAdapter, cell: ArenaCell): TBuilderInstruction = { + private def decodeFunToTlaEx(arena: PureArenaAdapter, cell: ArenaCell): BuilderT = { // a function is represented with the relation {(x, f[x]) : x \in S} val relation = arena.getCdm(cell) @@ -195,7 +200,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter // given this, we query the solver about the function's domain instead val domain = arena.getDom(cell) - def inDom(elem: ArenaCell): TBuilderInstruction = { + def inDom(elem: ArenaCell): BuilderT = { val elemEx = elem.toBuilder val domEx = domain.toBuilder tla.selectInSet(elemEx, domEx) @@ -257,7 +262,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter } } - private def findCellInSet(cells: Seq[ArenaCell], ex: TBuilderInstruction): Option[ArenaCell] = { + private def findCellInSet(cells: Seq[ArenaCell], ex: BuilderT): Option[ArenaCell] = { def isEq(c: ArenaCell): Boolean = { val query = tla.and(tla.eql(c.toBuilder, ex)) tla.bool(true).build == solverContext.evalGroundExpr(query) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala index 3de414aaf6..9c399c68e4 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala @@ -303,11 +303,13 @@ class SymbStateRewriterImpl( -> List(new LabelRule(this)), key(OperEx(ApalacheOper.gen, tla.int(2))) -> List(new GenRule(this)), - // folds and MkSeq + // folds, repeat and MkSeq key(OperEx(ApalacheOper.foldSet, tla.name("A"), tla.name("v"), tla.name("S"))) -> List(new FoldSetRule(this, renaming)), key(OperEx(ApalacheOper.foldSeq, tla.name("A"), tla.name("v"), tla.name("s"))) -> List(new FoldSeqRule(this, renaming)), + key(OperEx(ApalacheOper.repeat, tla.name("Op"), tla.int(10), tla.name("s"))) + -> List(new RepeatRule(this, renaming)), key(OperEx(ApalacheOper.mkSeq, tla.int(10), tla.name("A"))) -> List(new MkSeqRule(this, renaming)), ) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PtrUtil.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PtrUtil.scala index c81c24f6ab..28f570c42b 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PtrUtil.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PtrUtil.scala @@ -1,7 +1,7 @@ package at.forsyte.apalache.tla.bmcmt.arena import at.forsyte.apalache.tla.bmcmt.{ArenaCell, ElemPtr, FixedElemPtr, SmtExprElemPtr} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Contains miscellaneous methods related to [[ElemPtr]]s. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PureArenaAdapter.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PureArenaAdapter.scala index 72f43e98f8..01b7357a5e 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PureArenaAdapter.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PureArenaAdapter.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.{ArenaCell, ElemPtr, FixedElemPtr, PureAren import at.forsyte.apalache.tla.bmcmt.types._ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Declares the same interface as [[Arena]]s (with the exception of [[ElemPtr]] usage). diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/EqCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/EqCache.scala index 21646402d3..984baef229 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/EqCache.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/EqCache.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.caches.EqCache._ import at.forsyte.apalache.tla.bmcmt.rewriter.Recoverable import at.forsyte.apalache.tla.bmcmt.{ArenaCell, StackableContext} import at.forsyte.apalache.tla.lir.TlaEx -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} import scala.collection.mutable diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntRangeCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntRangeCache.scala index 47ec20a096..5f92925f81 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntRangeCache.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntRangeCache.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.{ArenaCell, ElemPtr, FixedElemPtr} import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.lir.{IntT1, SetT1} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Cache tuple domains as well as ranges a..b. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntValueCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntValueCache.scala index 2bce3fcba9..284bf02d02 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntValueCache.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntValueCache.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.ArenaCell import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.lir.IntT1 -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * A cache for integer constants that maps an integer to an integer constant in SMT. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/ModelValueCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/ModelValueCache.scala index 3318cc1d6e..fe25ac55d0 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/ModelValueCache.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/ModelValueCache.scala @@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.bmcmt.types.CellTFrom import at.forsyte.apalache.tla.lir.{ConstT1, StrT1} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * A cache for model values that are translated as uninterpreted constants, with a unique sort per uniterpreted type. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/RecordDomainCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/RecordDomainCache.scala index 606c429769..fc68488903 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/RecordDomainCache.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/RecordDomainCache.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.{ArenaCell, ElemPtr, SmtExprElemPtr} import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.lir.{SetT1, StrT1} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} import scala.collection.immutable.SortedSet diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala index 39cebd8a91..aa2b3bb34a 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala @@ -70,6 +70,7 @@ class BoundedCheckerPassImpl @Inject() ( params.discardDisabled = options.checker.discardDisabled params.checkForDeadlocks = !options.checker.noDeadlocks params.nMaxErrors = options.checker.maxError + params.timeoutSmtSec = options.checker.timeoutSmtSec params.smtEncoding = smtEncoding val smtProfile = options.common.smtprof diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/CardinalityConstRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/CardinalityConstRule.scala index d424032ab2..5a083fdf83 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/CardinalityConstRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/CardinalityConstRule.scala @@ -6,7 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.CherryPick import at.forsyte.apalache.tla.lir.oper.{ApalacheOper, TlaArithOper, TlaFiniteSetOper} import at.forsyte.apalache.tla.lir.values.TlaInt import at.forsyte.apalache.tla.lir.{BoolT1, OperEx, ValEx} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Optimization for Cardinality(S) >= k, where k is constant. See [docs/smt/Cardinality.md]. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/DomainRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/DomainRule.scala index 7cf90cc6f9..02c19a730f 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/DomainRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/DomainRule.scala @@ -7,7 +7,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.{ProtoSeqOps, RecordAndVariantOps import at.forsyte.apalache.tla.bmcmt.types._ import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper.TlaFunOper -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Rewriting DOMAIN f, that is, translating the domain of a function, record, tuple, or sequence. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FoldSetRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FoldSetRule.scala index f1a895676b..f3e87a8484 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FoldSetRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FoldSetRule.scala @@ -7,7 +7,7 @@ import at.forsyte.apalache.tla.lir.oper.ApalacheOper import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker import at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming import at.forsyte.apalache.tla.pp.Inliner -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Rewriting rule for FoldSet. Similar to Cardinality, we need to consider element set presence and multiplicity. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRule.scala index c46e087842..3505ecee11 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRule.scala @@ -3,7 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.rules import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.bmcmt.rules.aux.{CherryPick, ProtoSeqOps, RecordAndVariantOps} import at.forsyte.apalache.tla.bmcmt.types._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} import at.forsyte.apalache.tla.lir.oper.TlaFunOper import at.forsyte.apalache.tla.lir.values.{TlaInt, TlaStr} import at.forsyte.apalache.tla.lir._ diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRuleWithArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRuleWithArrays.scala index 0f1e5531e6..6690fc4784 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRuleWithArrays.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRuleWithArrays.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._ import at.forsyte.apalache.tla.bmcmt.types._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} import at.forsyte.apalache.tla.lir.{BoolT1, FunT1, RecT1, SetT1, TlaEx} /** diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRule.scala index c823cfb84b..767a4b2ee7 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRule.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper.TlaFunOper -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * The new implementation of a function constructor that encodes a function f = [x \in S |-> e] the classical way: f = diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRuleWithArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRuleWithArrays.scala index 73b9c06aa9..e0393c441f 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRuleWithArrays.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRuleWithArrays.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._ import at.forsyte.apalache.tla.bmcmt.types._ import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Encodes the construction of a function f = [x \in S |-> e]. We carry the domain set in a separate set cell. The diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRule.scala index 36ff58c28a..a29232d67a 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRule.scala @@ -6,8 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.{ProtoSeqOps, RecordAndVariantOps import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper.TlaFunOper import at.forsyte.apalache.tla.lir.values.{TlaInt, TlaStr} -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} import scalaz.unused /** @@ -66,7 +65,7 @@ class FunExceptRule(rewriter: SymbStateRewriter) extends RewritingRule { indexCell: ArenaCell, valueCell: ArenaCell): SymbState = { // rewrite tuples <> to cells - def mkPair(indexCell: ArenaCell, resCell: ArenaCell): TBuilderInstruction = + def mkPair(indexCell: ArenaCell, resCell: ArenaCell): BuilderT = tla.tuple(indexCell.toBuilder, resCell.toBuilder) var nextState = rewriter.rewriteUntilDone(state.setRex(mkPair(indexCell, valueCell))) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRuleWithArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRuleWithArrays.scala index 86c2b6174a..8bb0385770 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRuleWithArrays.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRuleWithArrays.scala @@ -3,8 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.rules import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.bmcmt.arena.PtrUtil import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps.constrainRelationArgs -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * Rewriting EXCEPT for functions, tuples, and records. @@ -31,7 +30,7 @@ class FunExceptRuleWithArrays(rewriter: SymbStateRewriter) extends FunExceptRule nextState = nextState.updateArena(_.setDom(resultFunCell, domainCell)) // Make pair to propagate metadata - def mkPair(indexCell: ArenaCell, resCell: ArenaCell): TBuilderInstruction = + def mkPair(indexCell: ArenaCell, resCell: ArenaCell): BuilderT = tla.tuple(indexCell.toBuilder, resCell.toBuilder) nextState = rewriter.rewriteUntilDone(nextState.setRex(mkPair(indexCell, valueCell))) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IfThenElseRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IfThenElseRule.scala index 5753c1bc55..c27230be1d 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IfThenElseRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IfThenElseRule.scala @@ -6,8 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.CherryPick import at.forsyte.apalache.tla.bmcmt.types._ import at.forsyte.apalache.tla.lir.oper.TlaControlOper import at.forsyte.apalache.tla.lir.{BoolT1, ConstT1, IntT1, OperEx} -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * Rewriting rule for IF A THEN B ELSE C. @@ -63,7 +62,7 @@ class IfThenElseRule(rewriter: SymbStateRewriter) extends RewritingRule { private def iteBasic( state: SymbState, commonType: CellT, - pred: TBuilderInstruction, + pred: BuilderT, thenCell: ArenaCell, elseCell: ArenaCell) = { val newArena = state.arena.appendCellOld(commonType) @@ -78,7 +77,7 @@ class IfThenElseRule(rewriter: SymbStateRewriter) extends RewritingRule { // The cool thing is that we do not have to compare the results anymore. It is all defined by the oracle. private def iteGeneral( state: SymbState, - pred: TBuilderInstruction, + pred: BuilderT, thenCell: ArenaCell, elseCell: ArenaCell) = { def solverAssert = rewriter.solverContext.assertGroundExpr _ diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/QuantRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/QuantRule.scala index d203be5da0..717325582e 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/QuantRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/QuantRule.scala @@ -4,10 +4,10 @@ import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.bmcmt.rules.aux.{CherryPick, OracleHelper} import at.forsyte.apalache.tla.bmcmt.types._ import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} +import at.forsyte.apalache.tla.typecomp._ import at.forsyte.apalache.tla.lir.oper._ import at.forsyte.apalache.tla.lir.values.{TlaIntSet, TlaNatSet} -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction import com.typesafe.scalalogging.LazyLogging /** @@ -139,16 +139,16 @@ class QuantRule(rewriter: SymbStateRewriter) extends RewritingRule with LazyLogg val (predState: SymbState, predEsRaw: Seq[TlaEx]) = rewriter.rewriteBoundSeqUntilDone(setState, setCells.map(mkPair)) - val predEs: Seq[TBuilderInstruction] = predEsRaw.map(tla.unchecked) + val predEs: Seq[BuilderT] = predEsRaw.map(tla.unchecked) val nonEmpty = tla.or(setCells.map(c => tla.selectInSet(c.toBuilder, set.toBuilder)): _*) val empty = tla.and(setCells.map(c => tla.not(tla.selectInSet(c.toBuilder, set.toBuilder))): _*) - def elemWitnesses(elemAndPred: (ArenaCell, TBuilderInstruction)): TBuilderInstruction = { + def elemWitnesses(elemAndPred: (ArenaCell, BuilderT)): BuilderT = { tla.and(tla.selectInSet(elemAndPred._1.toBuilder, set.toBuilder), elemAndPred._2) } - def elemSatisfies(elemAndPred: (ArenaCell, TBuilderInstruction)): TBuilderInstruction = { + def elemSatisfies(elemAndPred: (ArenaCell, BuilderT)): BuilderT = { tla.or(tla.not(tla.selectInSet(elemAndPred._1.toBuilder, set.toBuilder)), elemAndPred._2) } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RecCtorRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RecCtorRule.scala index 327ceaf69a..a8b1835a96 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RecCtorRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RecCtorRule.scala @@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.RecordAndVariantOps import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper.TlaFunOper import at.forsyte.apalache.tla.lir.values.TlaStr -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} import scala.collection.immutable.{SortedMap, SortedSet} diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RepeatRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RepeatRule.scala new file mode 100644 index 0000000000..7dff798d78 --- /dev/null +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RepeatRule.scala @@ -0,0 +1,83 @@ +package at.forsyte.apalache.tla.bmcmt.rules + +import at.forsyte.apalache.tla.bmcmt._ +import at.forsyte.apalache.tla.lir._ +import at.forsyte.apalache.tla.lir.oper.ApalacheOper +import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker +import at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming +import at.forsyte.apalache.tla.lir.values.TlaInt +import at.forsyte.apalache.tla.pp.Inliner +import at.forsyte.apalache.tla.types.{tlaU => tla} + +/** + * Rewriting rule for Repeat. This rule is similar to [[FoldSeqRule]]. + * + * This rule is more efficient than the fold- rules, because it does not require an underlying data structure (Seq or + * Set). In particular, folding over 1..N, despite the overapproximation being tight by construction, still introduces + * O(N*N) constraints, since the SMT solver must assert element uniqueness (i /= j for all i,j \in 1..N). OTOH, + * RepeatRule consumes 1..N in the canonical order natively as a 1.to(N) in Scala. + * + * @author + * Jure Kukovec + */ +class RepeatRule(rewriter: SymbStateRewriter, renaming: IncrementalRenaming) extends RewritingRule { + + override def isApplicable(symbState: SymbState): Boolean = { + symbState.ex match { + case OperEx(ApalacheOper.repeat, LetInEx(NameEx(appName), TlaOperDecl(operName, params, _)), _, _) => + appName == operName && params.size == 2 + case _ => false + } + } + + override def apply(state: SymbState): SymbState = state.ex match { + // assume isApplicable + case ex @ OperEx(ApalacheOper.repeat, LetInEx(NameEx(_), opDecl), boundEx, baseEx) => + boundEx match { + case ValEx(TlaInt(n)) if n.isValidInt && n.toInt >= 0 => + // rewrite baseEx to its final cell form + val baseState = rewriter.rewriteUntilDone(state.setRex(baseEx)) + + // We need the type signature. The signature of Repeat is + // \A a : ((a,Int) => a, Int, a) => a + // so the operator type must be (a,Int) => a + val a = TlaType1.fromTypeTag(baseEx.typeTag) + val opT = OperT1(Seq(a, IntT1), a) + // sanity check + TlaType1.fromTypeTag(opDecl.typeTag) match { + case `opT` => // all good + case badType => + val msg = s"FoldSet argument ${opDecl.name} should have the tag $opT, found $badType." + throw new TypingException(msg, opDecl.ID) + } + + // expressions are transient, we don't need tracking + val inliner = new Inliner(new IdleTracker, renaming) + // We can make the scope directly, since InlinePass already ensures all is well. + val seededScope: Inliner.Scope = Map(opDecl.name -> opDecl) + + // To implement the Repeat rule, we generate a sequence of cells. + // At each step, we perform one application of the operator + // defined by `opDecl` to the previous partial result, + // and pass the iteration index as the second parameter + (1 to n.toInt).foldLeft(baseState) { case (partialState, i) => + // partialState currently holds the cell representing the previous application step + val oldResultCell = partialState.asCell + + // First, we inline the operator application, with cell names as parameters + val appEx = tla.appOp( + tla.name(opDecl.name, opT), + oldResultCell.toBuilder, + tla.int(i), + ) + + val inlinedEx = inliner.transform(seededScope)(appEx) + rewriter.rewriteUntilDone(partialState.setRex(inlinedEx)) + } + case _ => + throw new RewriterException("Apalache!Repeat expects a constant positive integer. Found: " + boundEx, ex) + } + case _ => + throw new RewriterException("%s is not applicable".format(getClass.getSimpleName), state.ex) + } +} diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SeqOpsRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SeqOpsRule.scala index affd54df27..c089426668 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SeqOpsRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SeqOpsRule.scala @@ -3,7 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.rules import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.bmcmt.rules.aux.{CherryPick, ProtoSeqOps} import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} import at.forsyte.apalache.tla.lir.oper.{ApalacheInternalOper, TlaSeqOper} /** diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetAsFunRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetAsFunRule.scala index a796dbbfdf..4f6396dd7b 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetAsFunRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetAsFunRule.scala @@ -3,9 +3,8 @@ package at.forsyte.apalache.tla.bmcmt.rules import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} import at.forsyte.apalache.tla.lir.oper.ApalacheOper -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction /** * Implements a rule for Apalache!SetAsFun. @@ -118,7 +117,7 @@ class SetAsFunRule(rewriter: SymbStateRewriter) extends RewritingRule { val key1 = nextState.arena.getHas(pair1).head // ensure that a pair with the same key has not been included in the relation yet - def keysDifferOrNotIncluded(pair2Ptr: ElemPtr): TBuilderInstruction = { + def keysDifferOrNotIncluded(pair2Ptr: ElemPtr): BuilderT = { val pair2 = pair2Ptr.elem val key2 = nextState.arena.getHas(pair2).head // pair2 \notin funRel diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCtorRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCtorRule.scala index 765734621c..8ee6c25656 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCtorRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCtorRule.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.bmcmt.types.{CellT, CellTFrom} import at.forsyte.apalache.tla.lir.oper.TlaSetOper import at.forsyte.apalache.tla.lir.{OperEx, SetT1, TlaEx, TypingException} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Rewrites the set constructor {e_1, ..., e_k}. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCupRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCupRule.scala index fad08ced10..4ee1c5f480 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCupRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCupRule.scala @@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.bmcmt.arena.PtrUtil import at.forsyte.apalache.tla.lir.oper.{TlaBoolOper, TlaSetOper} import at.forsyte.apalache.tla.lir.{OperEx, TlaType1} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Rewrites X \cup Y, that is, a union of two sets (not UNION). In the first encoding, we used a linear number of `in` diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetFilterRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetFilterRule.scala index d50920dd70..514dfad4e4 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetFilterRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetFilterRule.scala @@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.bmcmt.types._ import at.forsyte.apalache.tla.lir.oper.{TlaBoolOper, TlaSetOper} import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Rewrites a set comprehension { x \in S: P }. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRule.scala index ea88a6558e..edb0153941 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRule.scala @@ -5,8 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._ import at.forsyte.apalache.tla.bmcmt.types._ import at.forsyte.apalache.tla.lir.oper.{ApalacheInternalOper, TlaSetOper} import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * Rewrites set membership tests: x \in S, x \in SUBSET S, and x \in [S -> T]. @@ -114,7 +113,7 @@ class SetInRule(rewriter: SymbStateRewriter) extends RewritingRule { // In the new implementation, a function is a relation { <> : x \in U }. // Check that \A t \in f: t[1] \in S /\ t[2] \in T, and // `DOMAIN f = S`, since the above only implies `DOMAIN f \subseteq S` - def onPair(pair: ArenaCell): TBuilderInstruction = { + def onPair(pair: ArenaCell): BuilderT = { val tupleElems = nextState.arena.getHas(pair) val (arg, res) = (tupleElems.head, tupleElems.tail.head) nextState = rewriter.rewriteUntilDone(nextState.setRex(tla.selectInSet(arg.toBuilder, funsetDom.toBuilder))) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala index 3f0901d625..684b814e86 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala @@ -6,8 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._ import at.forsyte.apalache.tla.bmcmt.types._ import at.forsyte.apalache.tla.bmcmt.{ArenaCell, RewriterException, SymbState, SymbStateRewriter} import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * Rewrites set membership tests: x \in S, x \in SUBSET S, and x \in [S -> T]. @@ -33,16 +32,18 @@ class SetInRuleWithArrays(rewriter: SymbStateRewriter) extends SetInRule(rewrite // TODO: Inlining this method is pointless. We should consider handling tuples and other structures natively in SMT. var newState = rewriter.lazyEq.cacheEqConstraints(state, setElems.cross(powsetDomainElems)) - def isInPowset(setElem: ArenaCell): TBuilderInstruction = { + def isInPowset(setElem: ArenaCell): BuilderT = { newState = newState.updateArena(_.appendCell(BoolT1)) val pred = newState.arena.topCell - def isInAndEqSetElem(powsetDomainElem: ArenaCell): TBuilderInstruction = { + def isInAndEqSetElem(powsetDomainElem: ArenaCell): BuilderT = { // powsetDomainElem \in powsetDomain /\ powsetDomainElem = setElem - tla - .and(tla.selectInSet(powsetDomainElem.toBuilder, powsetDomain.toBuilder), - tla.eql(powsetDomainElem.toBuilder, setElem.toBuilder)) - .map(simplifier.simplifyShallow) + simplifier.applySimplifyShallowToBuilderEx( + tla.and( + tla.selectInSet(powsetDomainElem.toBuilder, powsetDomain.toBuilder), + tla.eql(powsetDomainElem.toBuilder, setElem.toBuilder), + ) + ) } val elemsInAndEqSetElem = powsetDomainElems.map(isInAndEqSetElem) @@ -53,7 +54,8 @@ class SetInRuleWithArrays(rewriter: SymbStateRewriter) extends SetInRule(rewrite pred.toBuilder } - val isSubset = tla.and(setElems.map(isInPowset): _*).map(simplifier.simplifyShallow) + val isSubset = + simplifier.applySimplifyShallowToBuilderEx(tla.and(setElems.map(isInPowset): _*)) newState = newState.updateArena(_.appendCell(BoolT1)) val pred = newState.arena.topCell.toBuilder rewriter.solverContext.assertGroundExpr(tla.eql(pred, isSubset)) @@ -88,7 +90,7 @@ class SetInRuleWithArrays(rewriter: SymbStateRewriter) extends SetInRule(rewrite // This method checks if f(x) \in T, for a given x // The goal is to ensure that \forall x \in DOMAIN f : f(x) \in T, by applying it to every arg \in DOMAIN f - def onFun(funsetDomElem: ArenaCell): TBuilderInstruction = { + def onFun(funsetDomElem: ArenaCell): BuilderT = { funsetCdm.cellType match { case _: PowSetT => nextState = rewriter diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithFunArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithFunArrays.scala index 0b2aa208a7..0000d6f9f0 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithFunArrays.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithFunArrays.scala @@ -4,8 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._ import at.forsyte.apalache.tla.bmcmt.types._ import at.forsyte.apalache.tla.bmcmt.{ArenaCell, RewriterException, SymbState, SymbStateRewriter} import at.forsyte.apalache.tla.lir.{BoolT1, FunT1} -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * Rewrites set membership tests: x \in S, x \in SUBSET S, and x \in [S -> T]. @@ -38,7 +37,7 @@ class SetInRuleWithFunArrays(rewriter: SymbStateRewriter) extends SetInRule(rewr // This method checks if there is a pair (x,y) \in RELATION f s.t. x = arg \land arg \in DOMAIN f // The goal is to ensure that f's range is a subset of T, by applying it to every arg \in DOMAIN f - def onPair(arg: ArenaCell): TBuilderInstruction = { + def onPair(arg: ArenaCell): BuilderT = { val funApp = tla.app(funCell.toBuilder, arg.toBuilder) nextState = rewriter.rewriteUntilDone(nextState.setRex(funApp)) val funAppRes = nextState.asCell diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetUnionRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetUnionRule.scala index cbb3c19ae7..417e61b650 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetUnionRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetUnionRule.scala @@ -3,10 +3,9 @@ package at.forsyte.apalache.tla.bmcmt.rules import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.bmcmt.arena.PtrUtil import at.forsyte.apalache.tla.bmcmt.types.CellTFrom -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} import at.forsyte.apalache.tla.lir.oper.TlaSetOper import at.forsyte.apalache.tla.lir.{OperEx, SetT1, TypingException} -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction /** * Implements the rule for a union of all set elements, that is, UNION S for a set S that contains sets as elements. @@ -62,7 +61,7 @@ class SetUnionRule(rewriter: SymbStateRewriter) extends RewritingRule { // add all the elements to the arena nextState = nextState.updateArena(_.appendHas(newSetCell, unionElemPtrs: _*)) - def inPointingSet(elemCell: ArenaCell, set: ArenaCell): TBuilderInstruction = { + def inPointingSet(elemCell: ArenaCell, set: ArenaCell): BuilderT = { // this is sound, because we have generated element equalities // and thus can use congruence of in(...) for free tla.and(tla.selectInSet(set.toBuilder, topSetCell.toBuilder), diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/AuxOps.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/AuxOps.scala index 0e197f5ccc..e2aa2639ea 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/AuxOps.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/AuxOps.scala @@ -3,8 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt.rewriter.ConstSimplifierForSmt import at.forsyte.apalache.tla.bmcmt.{ArenaCell, SymbState, SymbStateRewriter} -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * Auxiliary methods for handling rewriting rules. @@ -46,13 +45,13 @@ object AuxOps { val domainElems = nextState.arena.getHas(domain) val relationElems = nextState.arena.getHas(relation) - def eqAndInDomain(domainElem: ArenaCell, checkedElem: ArenaCell): TBuilderInstruction = { + def eqAndInDomain(domainElem: ArenaCell, checkedElem: ArenaCell): BuilderT = { val eq = tla.unchecked(rewriter.lazyEq.safeEq(domainElem, checkedElem)) val selectInSet = tla.selectInSet(domainElem.toBuilder, domain.toBuilder) tla.and(eq, selectInSet) } - def isInDomain(elem: ArenaCell): TBuilderInstruction = { + def isInDomain(elem: ArenaCell): BuilderT = { if (domainElems.isEmpty) { tla.bool(false) } else { @@ -99,7 +98,7 @@ object AuxOps { checkedElem: ArenaCell, setElem: ArenaCell, setCell: ArenaCell, - lazyEq: Boolean): TBuilderInstruction = { + lazyEq: Boolean): BuilderT = { val conjunction = if (lazyEq) { tla.and( @@ -112,6 +111,6 @@ object AuxOps { tla.eql(checkedElem.toBuilder, setElem.toBuilder), ) } - conjunction.map(simplifier.simplifyShallow) + simplifier.applySimplifyShallowToBuilderEx(conjunction) } } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala index abf076190b..14076b0089 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala @@ -6,8 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.arena.PtrUtil import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._ import at.forsyte.apalache.tla.bmcmt.types._ import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types._ +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT, _} import scala.collection.immutable.SortedMap @@ -39,7 +38,7 @@ class CherryPick(rewriter: SymbStateRewriter) { * @return * a new symbolic state whose expression stores a fresh cell that corresponds to the picked element. */ - def pick(set: ArenaCell, state: SymbState, elseAssert: TBuilderInstruction): SymbState = { + def pick(set: ArenaCell, state: SymbState, elseAssert: BuilderT): SymbState = { set.cellType match { // all kinds of sets that should be kept unexpanded case PowSetT(t @ SetT1(_)) => @@ -110,7 +109,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, elems: Seq[ArenaCell], - elseAssert: TBuilderInstruction): SymbState = { + elseAssert: BuilderT): SymbState = { assert(elems.nonEmpty) // this is an advanced operator -- you should know what you are doing val targetType = elems.head.cellType @@ -181,7 +180,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, elems: Seq[ArenaCell], - elseAssert: TBuilderInstruction): SymbState = { + elseAssert: BuilderT): SymbState = { rewriter.solverContext.log("; CHERRY-PICK %s FROM [%s] {".format(cellType, elems.map(_.toString).mkString(", "))) val arena = state.arena.appendCell(cellType) val resultCell = arena.topCell @@ -214,7 +213,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, tuples: Seq[ArenaCell], - elseAssert: TBuilderInstruction): SymbState = { + elseAssert: BuilderT): SymbState = { rewriter.solverContext.log("; CHERRY-PICK %s FROM [%s] {".format(cellType, tuples.map(_.toString).mkString(", "))) var newState = state @@ -262,7 +261,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, records: Seq[ArenaCell], - elseAssert: TBuilderInstruction): SymbState = { + elseAssert: BuilderT): SymbState = { // the records do not always have the same type, but they do have compatible types val commonRecordT = findCommonRecordType(records) rewriter.solverContext @@ -353,7 +352,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, records: Seq[ArenaCell], - elseAssert: TBuilderInstruction): SymbState = { + elseAssert: BuilderT): SymbState = { // new row records always have the same type val (fieldTypes, recordT) = records.head.cellType match { case CellTFrom(rt @ RecRowT1(RowT1(fieldTypes, None))) => (fieldTypes, rt) @@ -400,7 +399,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, variants: Seq[ArenaCell], - elseAssert: TBuilderInstruction): SymbState = { + elseAssert: BuilderT): SymbState = { // variants should always have the same type val (optionTypes, variantT) = variants.head.cellType match { case CellTFrom(rt @ VariantT1(RowT1(opts, None))) => (opts, rt) @@ -580,7 +579,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, memberSets: Seq[ArenaCell], - elseAssert: TBuilderInstruction, + elseAssert: BuilderT, noSmt: Boolean = false): SymbState = { if (memberSets.isEmpty) { throw new RuntimeException("Picking from a statically empty set") @@ -602,7 +601,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, memberSets: Seq[ArenaCell], - elseAssert: TBuilderInstruction, + elseAssert: BuilderT, noSMT: Boolean): SymbState = { def solverAssert(e: TlaEx): Unit = rewriter.solverContext.assertGroundExpr(e) @@ -658,7 +657,7 @@ class CherryPick(rewriter: SymbStateRewriter) { // The awesome property of the oracle is that we do not have to compare the sets directly! // Instead, we compare the oracle values. // (chosen = 1 /\ in(z_i, R) <=> in(c_i, S_1)) \/ (chosen = 2 /\ in(z_i, R) <=> in(d_i, S_2)) \/ (chosen = N <=> elseAssert) - def nthIn(elemAndSet: (ArenaCell, ArenaCell), no: Int): (TBuilderInstruction, TBuilderInstruction) = { + def nthIn(elemAndSet: (ArenaCell, ArenaCell), no: Int): (BuilderT, BuilderT) = { if (elemsOfMemberSets(no).nonEmpty) { val inSet = tla.ite(tla.selectInSet(elemAndSet._1.toBuilder, elemAndSet._2.toBuilder), membershipEx, tla.storeNotInSet(picked.toBuilder, resultCell.toBuilder)) @@ -715,7 +714,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, memberSeqs: Seq[ArenaCell], - elseAssert: TBuilderInstruction): SymbState = { + elseAssert: BuilderT): SymbState = { if (memberSeqs.isEmpty) { throw new RuntimeException("Picking a sequence from a statically empty set") } else if (memberSeqs.length == 1) { @@ -738,7 +737,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, memberSeqs: Seq[ArenaCell], - elseAssert: TBuilderInstruction): SymbState = { + elseAssert: BuilderT): SymbState = { rewriter.solverContext .log("; CHERRY-PICK %s FROM [%s] {".format(seqType, memberSeqs.map(_.toString).mkString(", "))) @@ -829,7 +828,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, funs: Seq[ArenaCell], - elseAssert: TBuilderInstruction): SymbState = { + elseAssert: BuilderT): SymbState = { rewriter.solverContext.log("; CHERRY-PICK %s FROM [%s] {".format(funType, funs.map(_.toString).mkString(", "))) var nextState = state rewriter.solverContext.config.smtEncoding match { diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/IntOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/IntOracle.scala index 6e0e31ecb4..46bfd4dce0 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/IntOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/IntOracle.scala @@ -4,8 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.bmcmt.{ArenaCell, SymbState} import at.forsyte.apalache.tla.lir.{IntT1, ValEx} import at.forsyte.apalache.tla.lir.values.TlaInt -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * An oracle that uses an integer variable. Although using integers as an oracle is the most straightforward decision, @@ -23,13 +22,13 @@ class IntOracle(val intCell: ArenaCell, nvalues: Int) extends Oracle { override def size: Int = nvalues - override def whenEqualTo(state: SymbState, position: Int): TBuilderInstruction = + override def whenEqualTo(state: SymbState, position: Int): BuilderT = tla.eql(intCell.toBuilder, tla.int(position)) override def caseAssertions( state: SymbState, - assertions: Seq[TBuilderInstruction], - elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction = { + assertions: Seq[BuilderT], + elseAssertions: Seq[BuilderT] = Seq.empty): BuilderT = { if (elseAssertions.nonEmpty && assertions.size != elseAssertions.size) { throw new IllegalStateException(s"Invalid call to Oracle, malformed elseAssertions") } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/MockOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/MockOracle.scala index c36e6ffa24..1c10c3c6d6 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/MockOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/MockOracle.scala @@ -2,8 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.tla.bmcmt.SymbState import at.forsyte.apalache.tla.bmcmt.smt.SolverContext -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * An oracle that always has the same value. This class specializes all methods to the case oracle == fixedValue. @@ -16,14 +15,14 @@ class MockOracle(fixedValue: Int) extends Oracle { override def size: Int = fixedValue + 1 - override def whenEqualTo(state: SymbState, position: Int): TBuilderInstruction = { + override def whenEqualTo(state: SymbState, position: Int): BuilderT = { tla.bool(position == fixedValue) } override def caseAssertions( state: SymbState, - assertions: Seq[TBuilderInstruction], - elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction = + assertions: Seq[BuilderT], + elseAssertions: Seq[BuilderT] = Seq.empty): BuilderT = assertions(fixedValue) override def evalPosition(solverContext: SolverContext, state: SymbState): Int = diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/Oracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/Oracle.scala index 8762c1f364..78a746876f 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/Oracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/Oracle.scala @@ -2,8 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.tla.bmcmt.SymbState import at.forsyte.apalache.tla.bmcmt.smt.SolverContext -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * An abstract version of an oracle that is used e.g. in CherryPick. @@ -30,7 +29,7 @@ trait Oracle extends Serializable { * @param position * a position the oracle should be equal to */ - def whenEqualTo(state: SymbState, position: Int): TBuilderInstruction + def whenEqualTo(state: SymbState, position: Int): BuilderT /** * Produce a ground expression that contains assertions for the possible oracle values. @@ -46,8 +45,8 @@ trait Oracle extends Serializable { */ def caseAssertions( state: SymbState, - assertions: Seq[TBuilderInstruction], - elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction = { + assertions: Seq[BuilderT], + elseAssertions: Seq[BuilderT] = Seq.empty): BuilderT = { size match { // If the oracle has no candidate values, then caseAssertions should return a no-op for SMT, i.e. TRUE. case 0 => state.arena.cellTrue().toBuilder diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/OracleHelper.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/OracleHelper.scala index 0a619b9c13..35b63d5777 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/OracleHelper.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/OracleHelper.scala @@ -1,7 +1,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.tla.bmcmt.{ArenaCell, SymbState, SymbStateRewriter} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * A helper class to create oracle values and compare them. In two previous solutions, we were using integers, then diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala index 270bccea4c..5d67003924 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala @@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.lir.SetT1 -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * This class constructs the power set of S, that is, SUBSET S. Sometimes, this is just unavoidable, e.g., consider { Q diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PropositionalOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PropositionalOracle.scala index f1f7dde250..025869aed5 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PropositionalOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PropositionalOracle.scala @@ -4,15 +4,15 @@ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.bmcmt.types.CellTFrom import at.forsyte.apalache.tla.bmcmt.{ArenaCell, SymbState, SymbStateRewriter} import at.forsyte.apalache.tla.lir.BoolT1 -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} +import at.forsyte.apalache.tla.typecomp._ class PropositionalOracle(bitCells: Seq[ArenaCell], nvalues: Int) extends Oracle { override def size: Int = nvalues - override def whenEqualTo(state: SymbState, position: Int): TBuilderInstruction = { - def mkLits(n: Int, cells: Seq[ArenaCell]): Seq[TBuilderInstruction] = { + override def whenEqualTo(state: SymbState, position: Int): BuilderT = { + def mkLits(n: Int, cells: Seq[ArenaCell]): Seq[BuilderT] = { cells match { case Nil => Nil @@ -35,8 +35,8 @@ class PropositionalOracle(bitCells: Seq[ArenaCell], nvalues: Int) extends Oracle override def caseAssertions( state: SymbState, - assertions: Seq[TBuilderInstruction], - elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction = { + assertions: Seq[BuilderT], + elseAssertions: Seq[BuilderT] = Seq.empty): BuilderT = { if (elseAssertions.nonEmpty & assertions.size != elseAssertions.size) { throw new IllegalStateException(s"Invalid call to Oracle, malformed elseAssertions") } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ProtoSeqOps.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ProtoSeqOps.scala index dbcabd98e7..a776fea7e9 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ProtoSeqOps.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ProtoSeqOps.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter import at.forsyte.apalache.tla.bmcmt.types.{CellTFrom, UnknownT} import at.forsyte.apalache.tla.bmcmt.{ArenaCell, FixedElemPtr, SymbState, SymbStateRewriter} import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} import scala.collection.immutable.ArraySeq diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/RecordAndVariantOps.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/RecordAndVariantOps.scala index 2032574ae1..8e4dd60f82 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/RecordAndVariantOps.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/RecordAndVariantOps.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.bmcmt.arena.{PtrUtil, PureArenaAdapter} import at.forsyte.apalache.tla.bmcmt.types.CellTFrom import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} import scala.collection.immutable.SortedMap diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SetOps.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SetOps.scala index 1911df2866..d347a62d66 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SetOps.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SetOps.scala @@ -2,8 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.tla.bmcmt.{ArenaCell, SymbState, SymbStateRewriter} import at.forsyte.apalache.tla.lir.BoolT1 -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** *

A small collection of operations on sets that can be reused by rewriting rules.

@@ -57,7 +56,7 @@ class SetOps(rewriter: SymbStateRewriter) { // /\ c[i] \in S // /\ \A j \in 0..(i - 1): // ~b[j] \/ c[j] /= c[i] - def notSeen(j: Int): TBuilderInstruction = { + def notSeen(j: Int): BuilderT = { tla.or(tla.not(predicates(j).toBuilder), tla.not(tla.eql(c_i.toBuilder, elems(j).toBuilder))) } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SparseOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SparseOracle.scala index 4112ea8563..b95064232b 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SparseOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SparseOracle.scala @@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.tla.bmcmt.SymbState import at.forsyte.apalache.tla.bmcmt.smt.SolverContext -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction +import at.forsyte.apalache.tla.types.{BuilderUT => BuilderT} /** * The oracle for sparse values, that is, a set S of naturals. This oracle is mapped on a smaller contiguous range @@ -23,15 +23,15 @@ class SparseOracle(oracle: Oracle, val values: Set[Int]) extends Oracle { override def size: Int = values.size - override def whenEqualTo(state: SymbState, position: Int): TBuilderInstruction = { + override def whenEqualTo(state: SymbState, position: Int): BuilderT = { assert(indexMap.contains(position)) oracle.whenEqualTo(state, indexMap(position)) } override def caseAssertions( state: SymbState, - assertions: Seq[TBuilderInstruction], - elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction = + assertions: Seq[BuilderT], + elseAssertions: Seq[BuilderT] = Seq.empty): BuilderT = oracle.caseAssertions(state, assertions, elseAssertions) override def evalPosition(solverContext: SolverContext, state: SymbState): Int = { diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/UninterpretedConstOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/UninterpretedConstOracle.scala index 4a01eb73ef..1fac909c43 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/UninterpretedConstOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/UninterpretedConstOracle.scala @@ -3,20 +3,20 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.lir.ConstT1 -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} +import at.forsyte.apalache.tla.typecomp._ class UninterpretedConstOracle(valueCells: Seq[ArenaCell], oracleCell: ArenaCell, nvalues: Int) extends Oracle { override def size: Int = nvalues - override def whenEqualTo(state: SymbState, position: Int): TBuilderInstruction = + override def whenEqualTo(state: SymbState, position: Int): BuilderT = tla.eql(oracleCell.toBuilder, valueCells(position).toBuilder) override def caseAssertions( state: SymbState, - assertions: Seq[TBuilderInstruction], - elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction = { + assertions: Seq[BuilderT], + elseAssertions: Seq[BuilderT] = Seq.empty): BuilderT = { if (elseAssertions.nonEmpty && assertions.size != elseAssertions.size) { throw new IllegalStateException(s"Invalid call to Oracle, malformed elseAssertions") } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ValueGenerator.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ValueGenerator.scala index 23784c3d16..66bd88d113 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ValueGenerator.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ValueGenerator.scala @@ -7,7 +7,7 @@ import at.forsyte.apalache.tla.bmcmt.types.{CellT, CellTFrom} import at.forsyte.apalache.tla.lir.TypedPredefs._ import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.convenience.{tla => tlaLegacy} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} import scalaz.unused import scala.collection.immutable.{SortedMap, SortedSet} diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ZipOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ZipOracle.scala index edba7f30dc..88b674f175 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ZipOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ZipOracle.scala @@ -2,8 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.tla.bmcmt.SymbState import at.forsyte.apalache.tla.bmcmt.smt.SolverContext -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * [[ZipOracle]] is an optimization of [[Oracle]]. It groups several values of the background oracle together, in order @@ -21,7 +20,7 @@ import at.forsyte.apalache.tla.types.tla class ZipOracle(backOracle: Oracle, groups: Seq[Seq[Int]]) extends Oracle { override def size: Int = groups.size - override def whenEqualTo(state: SymbState, index: Int): TBuilderInstruction = { + override def whenEqualTo(state: SymbState, index: Int): BuilderT = { assert(index < groups.size) val conds = groups(index).map(i => backOracle.whenEqualTo(state, i)) tla.or(conds: _*) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/ModelCheckerParams.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/ModelCheckerParams.scala index 2c7a052aad..8847475fb0 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/ModelCheckerParams.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/ModelCheckerParams.scala @@ -68,6 +68,11 @@ class ModelCheckerParams( */ var nMaxErrors: Int = 1 + /** + * The limit on a single SMT query. The default value is 0 (unlimited). + */ + var timeoutSmtSec: Int = 0 + /** * A timeout upon which a transition is split in its own group. This is the minimal timeout. The actual timeout is * updated at every step using `search.split.timeout.factor`. In our experiments, small timeouts lead to explosion of @@ -96,9 +101,6 @@ class ModelCheckerParams( */ def idleTimeoutMs: Long = idleTimeoutSec * 1000 - val smtTimeoutSec: Int = - tuningOptions.getOrElse("search.smt.timeout", "0").toInt - /** * The SMT encoding to be used. */ diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/SearchState.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/SearchState.scala index 0981dbf004..3a8497250d 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/SearchState.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/SearchState.scala @@ -18,6 +18,7 @@ class SearchState(params: ModelCheckerParams) { private var _result: CheckerResult = NoError() private var _nFoundErrors: Int = 0 + private var _nTimeouts: Int = 0 private val _counterexamples: ListBuffer[Counterexample] = ListBuffer.empty private var _nRunsLeft: Int = if (params.isRandomSimulation) params.nSimulationRuns else 1 @@ -30,6 +31,14 @@ class SearchState(params: ModelCheckerParams) { */ def nFoundErrors: Int = _nFoundErrors + /** + * Get the number of SMT timeouts that occurred in the search. + * + * @return + * number of timeouts + */ + def nTimeouts: Int = _nTimeouts + /** * Get the number of simulation runs to explore. * @@ -49,6 +58,8 @@ class SearchState(params: ModelCheckerParams) { case NoError() => if (_nFoundErrors > 0) { Error(_nFoundErrors, _counterexamples.toList) + } else if (_nTimeouts > 0) { + SmtTimeout(_nTimeouts) } else { NoError() } @@ -98,6 +109,11 @@ class SearchState(params: ModelCheckerParams) { _result = Deadlock(counterexample) } + case SmtTimeout(nTimeouts) => + // we still continue the search, but report incompleteness in [[this.finalResult]]. + _nTimeouts += nTimeouts + _result = NoError() + case _ => _result = result } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala index 5019b7cac4..76cac9981d 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala @@ -7,7 +7,7 @@ import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter import at.forsyte.apalache.tla.bmcmt.profiler.{IdleSmtListener, SmtListener} import at.forsyte.apalache.tla.bmcmt.rewriter.ConstSimplifierForSmt import at.forsyte.apalache.tla.bmcmt.types._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.io.UTFPrinter import at.forsyte.apalache.tla.lir.oper._ diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntRangeCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntRangeCache.scala index db962c93a1..2f3cb6662c 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntRangeCache.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntRangeCache.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.bmcmt.types.CellT import at.forsyte.apalache.tla.bmcmt.{ArenaCell, FixedElemPtr, PureArena} import at.forsyte.apalache.tla.lir.{IntT1, SetT1} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Cache ranges a..b and, as a special case, tuple domains. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntValueCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntValueCache.scala index 76e96e78fe..9002f4d476 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntValueCache.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntValueCache.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.bmcmt.types.CellT import at.forsyte.apalache.tla.bmcmt.{ArenaCell, PureArena} import at.forsyte.apalache.tla.lir.IntT1 -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * A cache for integer constants that maps an integer to an integer constant in SMT. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/RecordDomainCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/RecordDomainCache.scala index 23bef5c036..0eb8efa5c6 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/RecordDomainCache.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/RecordDomainCache.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.bmcmt.types.CellT import at.forsyte.apalache.tla.bmcmt.{ArenaCell, FixedElemPtr, PureArena} import at.forsyte.apalache.tla.lir.{SetT1, StrT1} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} import scala.collection.immutable.SortedSet diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala index 2d1a7b9dac..6a62339b86 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.bmcmt.types.{CellT, CellTFrom} import at.forsyte.apalache.tla.bmcmt.{ArenaCell, PureArena} import at.forsyte.apalache.tla.lir.{ConstT1, StrT1, TlaType1} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * A cache for uninterpreted literals, that are translated to uninterpreted SMT constants, with a unique sort per diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/IntOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/IntOracle.scala index fee661f0bb..38ad298eec 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/IntOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/IntOracle.scala @@ -5,8 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope import at.forsyte.apalache.tla.bmcmt.types.CellT import at.forsyte.apalache.tla.lir.{IntT1, ValEx} import at.forsyte.apalache.tla.lir.values.TlaInt -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * An oracle that uses an integer variable. Although using integers as an oracle is the most straightforward decision, @@ -27,7 +26,7 @@ class IntOracle(val intCell: ArenaCell, nvalues: Int) extends Oracle { * Produce an expression that states that the chosen value equals to the value `v_{index}`. The actual implementation * may be different from an integer comparison. */ - override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): TBuilderInstruction = + override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): BuilderT = tla.eql(intCell.toBuilder, tla.int(index)) override def getIndexOfChosenValueFromModel(solverContext: SolverContext): BigInt = diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/MockOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/MockOracle.scala index 53b288b0ce..09bb698e29 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/MockOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/MockOracle.scala @@ -2,8 +2,7 @@ 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 +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * An oracle that always has the same value. This class specializes all methods to the case oracle == fixedValue. @@ -17,13 +16,13 @@ class MockOracle(fixedValue: Int) extends Oracle { override def size: Int = fixedValue + 1 - override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): TBuilderInstruction = + override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): BuilderT = tla.bool(index == fixedValue) override def caseAssertions( scope: RewriterScope, - assertions: Seq[TBuilderInstruction], - elseAssertionsOpt: Option[Seq[TBuilderInstruction]] = None): TBuilderInstruction = { + assertions: Seq[BuilderT], + elseAssertionsOpt: Option[Seq[BuilderT]] = None): BuilderT = { require(assertions.size == this.size && elseAssertionsOpt.forall { _.size == this.size }, s"Invalid call to Oracle, assertion sequences must have length $size.") assertions(fixedValue) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/Oracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/Oracle.scala index 26efc705ed..74238f4c78 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/Oracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/Oracle.scala @@ -3,8 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.oracles import at.forsyte.apalache.tla.bmcmt.PureArena 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 +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * An oracle provides a means of choosing a single value, out of a finite collection of candidate values. It can @@ -29,7 +28,7 @@ trait Oracle { * Produce an expression that states that the chosen value equals to the value `v_{index}`. The actual implementation * may be different from an integer comparison. */ - def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): TBuilderInstruction + def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): BuilderT /** * Produce a ground expression that contains assertions for the possible oracle values. @@ -45,8 +44,8 @@ trait Oracle { */ def caseAssertions( scope: RewriterScope, - assertions: Seq[TBuilderInstruction], - elseAssertionsOpt: Option[Seq[TBuilderInstruction]] = None): TBuilderInstruction = { + assertions: Seq[BuilderT], + elseAssertionsOpt: Option[Seq[BuilderT]] = None): BuilderT = { require(assertions.size == this.size && elseAssertionsOpt.forall { _.size == this.size }, s"Invalid call to Oracle, assertion sequences must have length $size.") size match { 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 index 55c9255f41..e02c0ba337 100644 --- 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 @@ -2,8 +2,7 @@ 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 +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * Given a set `indices` of size `N`, sparse oracle is able to answer {{{chosenValueIsEqualToIndexedValue(_, i),}}} for @@ -30,7 +29,7 @@ class SparseOracle(mkOracle: Int => Oracle, val values: Set[Int]) extends Oracle override def size: Int = values.size - def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): TBuilderInstruction = + def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): BuilderT = indexMap .get(index.toInt) .map { @@ -40,8 +39,8 @@ class SparseOracle(mkOracle: Int => Oracle, val values: Set[Int]) extends Oracle override def caseAssertions( scope: RewriterScope, - assertions: Seq[TBuilderInstruction], - elseAssertionsOpt: Option[Seq[TBuilderInstruction]] = None): TBuilderInstruction = + assertions: Seq[BuilderT], + elseAssertionsOpt: Option[Seq[BuilderT]] = None): BuilderT = oracle.caseAssertions(scope, assertions, elseAssertionsOpt) override def getIndexOfChosenValueFromModel(solverContext: SolverContext): BigInt = { diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/UninterpretedConstOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/UninterpretedConstOracle.scala index 92e5549c93..bf1016cd91 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/UninterpretedConstOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/UninterpretedConstOracle.scala @@ -6,8 +6,8 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.UninterpretedLit import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope} import at.forsyte.apalache.tla.bmcmt.types.CellT import at.forsyte.apalache.tla.lir.ConstT1 -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} +import at.forsyte.apalache.tla.typecomp._ /** * An oracle that uses a fixed collection of potential cells. @@ -24,7 +24,7 @@ class UninterpretedConstOracle(val valueCells: Seq[ArenaCell], val oracleCell: A */ override def size: Int = valueCells.size - override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): TBuilderInstruction = + override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): BuilderT = if (valueCells.indices.contains(index)) tla.eql(oracleCell.toBuilder, valueCells(index.toInt).toBuilder) else tla.bool(false) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/ZipOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/ZipOracle.scala index 054dac080a..240251b916 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/ZipOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/ZipOracle.scala @@ -2,8 +2,7 @@ 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 +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * [[ZipOracle]] is an optimization of [[Oracle]]. It groups several values of the background oracle together, in order @@ -21,7 +20,7 @@ import at.forsyte.apalache.tla.types.tla class ZipOracle(backOracle: Oracle, groups: Seq[Seq[Int]]) extends Oracle { override def size: Int = groups.size - override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): TBuilderInstruction = + override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): BuilderT = if (groups.indices.contains(index)) { val conds = groups(index.toInt).map(i => backOracle.chosenValueIsEqualToIndexedValue(scope, i)) tla.or(conds: _*) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/IntConstStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/IntConstStratifiedRule.scala index f82de7f822..3737632188 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/IntConstStratifiedRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/IntConstStratifiedRule.scala @@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.IntValueCache import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope, StratifiedRule} import at.forsyte.apalache.tla.lir.values.TlaInt import at.forsyte.apalache.tla.lir.{TlaEx, ValEx} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Rewrites integer constants. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/AndStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/AndStratifiedRule.scala index 26ffcdf960..76bee4f8fc 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/AndStratifiedRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/AndStratifiedRule.scala @@ -6,8 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope} import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{addCell, StratifiedRule} import at.forsyte.apalache.tla.lir.oper.TlaBoolOper import at.forsyte.apalache.tla.lir.{BoolT1, OperEx, TlaEx} -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * Implements the rule for conjunction. @@ -20,8 +19,7 @@ import at.forsyte.apalache.tla.types.tla * @author * Jure Kukovec */ -class AndStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) - extends StratifiedRule[Option[TBuilderInstruction]] { +class AndStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) extends StratifiedRule[Option[BuilderT]] { private val simplifier = new ConstSimplifierForSmt() override def isApplicable(ex: TlaEx, scope: RewriterScope): Boolean = ex match { @@ -32,7 +30,7 @@ class AndStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) override def buildArena(ex: TlaEx)(startingScope: RewriterScope): ( RewriterScope, ArenaCell, - Option[TBuilderInstruction]) = simplifier.simplifyShallow(ex) match { + Option[BuilderT]) = simplifier.simplifyShallow(ex) match { case OperEx(TlaBoolOper.and, args @ _*) => if (args.isEmpty) { // empty conjunction is always true @@ -40,9 +38,9 @@ class AndStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) } else { // use short-circuiting on state-level expressions (like in TLC) - def toIte(es: Seq[TlaEx]): TBuilderInstruction = { + def toIte(es: Seq[TlaEx]): BuilderT = { // assume es is nonempty - es.map(tla.unchecked).reduceRight[TBuilderInstruction] { case (elem, partial) => + es.map(tla.unchecked).reduceRight[BuilderT] { case (elem, partial) => tla.ite(elem, partial, PureArena.cellFalse(startingScope.arena).toBuilder) } } @@ -58,7 +56,7 @@ class AndStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) val (newScope, rewrittenArgCells) = // With AND all blocks belong to the same scope, so we have to propagate it - args.foldLeft((startingScope.copy(arena = arenaWithAndCell), Seq.empty[TBuilderInstruction])) { + args.foldLeft((startingScope.copy(arena = arenaWithAndCell), Seq.empty[BuilderT])) { case ((scope, cellSeq), term) => val (newScope, termCell) = rewriter.rewrite(term)(scope) (newScope, cellSeq :+ termCell.toBuilder) @@ -74,7 +72,7 @@ class AndStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) (scope, cell, None) } - override def addConstraints(scope: RewriterScope, cell: ArenaCell, auxData: Option[TBuilderInstruction]): Unit = { + override def addConstraints(scope: RewriterScope, cell: ArenaCell, auxData: Option[BuilderT]): Unit = { // Only add constraints, if ITE rewriting didn't fire (in that case, the ITE rule does it for us) auxData.foreach { conjunction => rewriter.assert(tla.eql(cell.toBuilder, conjunction)) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/OrStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/OrStratifiedRule.scala index 187803e49c..93233c86fa 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/OrStratifiedRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/OrStratifiedRule.scala @@ -6,8 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{addCell, StratifiedRule} import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope} import at.forsyte.apalache.tla.lir.{BoolT1, OperEx, TlaEx} import at.forsyte.apalache.tla.lir.oper.TlaBoolOper -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * Implements the rule for disjunction. @@ -20,8 +19,7 @@ import at.forsyte.apalache.tla.types.tla * @author * Jure Kukovec */ -class OrStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) - extends StratifiedRule[Option[TBuilderInstruction]] { +class OrStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) extends StratifiedRule[Option[BuilderT]] { private val simplifier = new ConstSimplifierForSmt() override def isApplicable(ex: TlaEx, scope: RewriterScope): Boolean = ex match { @@ -32,7 +30,7 @@ class OrStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) override def buildArena(ex: TlaEx)(startingScope: RewriterScope): ( RewriterScope, ArenaCell, - Option[TBuilderInstruction]) = simplifier.simplifyShallow(ex) match { + Option[BuilderT]) = simplifier.simplifyShallow(ex) match { case OperEx(TlaBoolOper.or, args @ _*) => if (args.isEmpty) { // empty disjunction is always false @@ -40,9 +38,9 @@ class OrStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) } else { // use short-circuiting on state-level expressions (like in TLC) - def toIte(es: Seq[TlaEx]): TBuilderInstruction = { + def toIte(es: Seq[TlaEx]): BuilderT = { // assume es is nonempty - es.map(tla.unchecked).reduceRight[TBuilderInstruction] { case (elem, partial) => + es.map(tla.unchecked).reduceRight[BuilderT] { case (elem, partial) => tla.ite(elem, PureArena.cellTrue(startingScope.arena).toBuilder, partial) } } @@ -71,7 +69,7 @@ class OrStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) (scope, cell, None) } - override def addConstraints(scope: RewriterScope, cell: ArenaCell, auxData: Option[TBuilderInstruction]): Unit = { + override def addConstraints(scope: RewriterScope, cell: ArenaCell, auxData: Option[BuilderT]): Unit = { // Only add constraints, if ITE rewriting didn't fire (in that case, the ITE rule does it for us) auxData.foreach { disjunction => rewriter.assert(tla.eql(cell.toBuilder, disjunction)) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCtorStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCtorStratifiedRule.scala index f0fb928416..88572fa324 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCtorStratifiedRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCtorStratifiedRule.scala @@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope} import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{addCell, StratifiedRule} import at.forsyte.apalache.tla.lir.oper.TlaSetOper import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Rewrites the set constructor {e_1, ..., e_k}. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCupStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCupStratifiedRule.scala index ad4d437819..73d284806a 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCupStratifiedRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCupStratifiedRule.scala @@ -6,6 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope, S import at.forsyte.apalache.tla.bmcmt.types.CellT import at.forsyte.apalache.tla.lir.oper.TlaSetOper import at.forsyte.apalache.tla.lir.{OperEx, TlaEx} +import at.forsyte.apalache.tla.typecomp._ /** * Rewrites X \cup Y, that is, a union of two sets (not UNION). diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetFilterStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetFilterStratifiedRule.scala index 78156496c8..63b3520b1e 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetFilterStratifiedRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetFilterStratifiedRule.scala @@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{addCell, Rewriter, Rewrite import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper.TlaSetOper import at.forsyte.apalache.tla.lir.values.{TlaIntSet, TlaNatSet} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Rewrites a set comprehension { x \in S: P }. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/util/TlaExUtil.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/util/TlaExUtil.scala index 4010c2c726..68662f3919 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/util/TlaExUtil.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/util/TlaExUtil.scala @@ -32,6 +32,11 @@ object TlaExUtil { findRec(localBody) baseExAndCollectionEx.foreach(findRec) + // ignore the names in the auxiliary let-in definition + case OperEx(ApalacheOper.repeat, LetInEx(_, TlaOperDecl(_, _, localBody)), boundAndBaseEx @ _*) => + findRec(localBody) + boundAndBaseEx.foreach(findRec) + // ignore the names in the auxiliary let-in definition case OperEx(ApalacheOper.mkSeq, len, LetInEx(_, TlaOperDecl(_, _, localBody))) => findRec(localBody) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/RewriterBase.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/RewriterBase.scala index 911ede25ce..c540f12e9d 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/RewriterBase.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/RewriterBase.scala @@ -3,10 +3,10 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter import at.forsyte.apalache.tla.bmcmt.smt.SolverContext -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} +import at.forsyte.apalache.tla.typecomp._ import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker import at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction import org.scalatest.funsuite.FixtureAnyFunSuite import java.io.StringWriter @@ -19,7 +19,7 @@ trait RewriterBase extends FixtureAnyFunSuite { protected val renaming = new IncrementalRenaming(new IdleTracker) - protected def assertBuildEqual(a: TBuilderInstruction, b: TBuilderInstruction): Unit = + protected def assertBuildEqual(a: BuilderT, b: BuilderT): Unit = assert(a.build == b.build) protected def create(rewriterType: SMTEncoding): SymbStateRewriter = { diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestCherryPick.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestCherryPick.scala index cacf67134a..bef6f6dabc 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestCherryPick.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestCherryPick.scala @@ -3,10 +3,9 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt.rules.aux.{CherryPick, Oracle, OracleFactory} import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla._ import at.forsyte.apalache.tla.types.parser.DefaultType1Parser -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} +import at.forsyte.apalache.tla.types.tlaU._ trait TestCherryPick extends RewriterBase { private val parser = DefaultType1Parser @@ -171,7 +170,7 @@ trait TestCherryPick extends RewriterBase { state = oracleState def mkRecord(i: Int, j: Int): ArenaCell = { - val rec = tla.rec("a" -> int(i), "b" -> int(j)).map(_.withTag(Typed(recordT))) + val rec = tla.rec("a" -> int(i), "b" -> int(j)).withTag(Typed(recordT)) state = rewriter.rewriteUntilDone(state.setRex(rec)) state.asCell } @@ -351,7 +350,7 @@ trait TestCherryPick extends RewriterBase { val (oracleState, oracle) = new OracleFactory(rewriter).newConstOracle(state, 2) state = oracleState - def mkFun(dom: TBuilderInstruction, map: TBuilderInstruction): ArenaCell = { + def mkFun(dom: BuilderT, map: BuilderT): ArenaCell = { val fun = funDef(map, name("x", IntT1) -> dom) state = rewriter.rewriteUntilDone(state.setRex(fun)) state.asCell diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithArrays.scala index 1a79c4efd5..f146e7cbb6 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithArrays.scala @@ -18,7 +18,7 @@ class TestRewriterWithArrays with TestSymbStateRewriterPowerset with TestSymbStateRewriterRecord with TestSymbStateRewriterSequence with TestSymbStateRewriterSet with TestSymbStateRewriterStr with TestSymbStateRewriterTuple with TestPropositionalOracle with TestSparseOracle with TestUninterpretedConstOracle - with TestSymbStateRewriterApalache with TestSymbStateRewriterMkSeq { + with TestSymbStateRewriterApalache with TestSymbStateRewriterMkSeq with TestSymbStateRewriterRepeat { override protected def withFixture(test: OneArgTest): Outcome = { solverContext = new PreproSolverContext(new Z3SolverContext(SolverConfig.default.copy(debug = true, smtEncoding = SMTEncoding.Arrays))) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithFunArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithFunArrays.scala index a7647d39c6..43b6cc0a18 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithFunArrays.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithFunArrays.scala @@ -18,7 +18,7 @@ class TestRewriterWithFunArrays with TestSymbStateRewriterPowerset with TestSymbStateRewriterRecord with TestSymbStateRewriterSequence with TestSymbStateRewriterSet with TestSymbStateRewriterStr with TestSymbStateRewriterTuple with TestPropositionalOracle with TestSparseOracle with TestUninterpretedConstOracle - with TestSymbStateRewriterApalache with TestSymbStateRewriterMkSeq { + with TestSymbStateRewriterApalache with TestSymbStateRewriterMkSeq with TestSymbStateRewriterRepeat { override protected def withFixture(test: OneArgTest): Outcome = { solverContext = new PreproSolverContext(new Z3SolverContext(SolverConfig.default.copy(debug = true, smtEncoding = SMTEncoding.FunArrays))) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithOOPSLA19.scala index 468aabb431..b455b76665 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithOOPSLA19.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithOOPSLA19.scala @@ -19,7 +19,7 @@ class TestRewriterWithOOPSLA19 with TestSymbStateRewriterVariant with TestSymbStateRewriterSequence with TestSymbStateRewriterSet with TestSymbStateRewriterStr with TestSymbStateRewriterTuple with TestPropositionalOracle with TestSparseOracle with TestUninterpretedConstOracle with TestSymbStateRewriterApalache with TestSymbStateRewriterMkSeq - with TestDefaultValueFactory { + with TestDefaultValueFactory with TestSymbStateRewriterRepeat { override protected def withFixture(test: OneArgTest): Outcome = { solverContext = new PreproSolverContext(new Z3SolverContext(SolverConfig.default.copy(debug = true, smtEncoding = SMTEncoding.OOPSLA19))) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateDecoder.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateDecoder.scala index b3de34187d..a83152a9d7 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateDecoder.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateDecoder.scala @@ -3,19 +3,19 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper.TlaSetOper -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction import at.forsyte.apalache.tla.types.parser.DefaultType1Parser -import at.forsyte.apalache.tla.types.tla -import at.forsyte.apalache.tla.types.tla._ +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} +import at.forsyte.apalache.tla.typecomp._ +import at.forsyte.apalache.tla.types.tlaU._ trait TestSymbStateDecoder extends RewriterBase { private val parser = DefaultType1Parser private val int2 = parser("<>") - private def pair(i: Int, j: Int): TBuilderInstruction = tuple(int(i), int(j)) + private def pair(i: Int, j: Int): BuilderT = tuple(int(i), int(j)) test("decode bool") { rewriterType: SMTEncoding => - val originalEx: TBuilderInstruction = bool(true) + val originalEx: BuilderT = bool(true) val state = new SymbState(originalEx, arena, Binding()) val rewriter = create(rewriterType) val nextState = rewriter.rewriteUntilDone(state) @@ -45,7 +45,7 @@ trait TestSymbStateDecoder extends RewriterBase { } test("decode str") { rewriterType: SMTEncoding => - val originalEx: TBuilderInstruction = str("hello") + val originalEx: BuilderT = str("hello") val state = new SymbState(originalEx, arena, Binding()) val rewriter = create(rewriterType) val nextState = rewriter.rewriteUntilDone(state) @@ -141,7 +141,7 @@ trait TestSymbStateDecoder extends RewriterBase { val decoder = new SymbStateDecoder(solverContext, rewriter) val decodedEx = decoder.decodeCellToTlaEx(nextState.arena, cell) - val expectedOutcome: TBuilderInstruction = setAsFun(enumSet(pair(1, 2), pair(2, 3))) + val expectedOutcome: BuilderT = setAsFun(enumSet(pair(1, 2), pair(2, 3))) assertBuildEqual(expectedOutcome, decodedEx) } @@ -180,7 +180,7 @@ trait TestSymbStateDecoder extends RewriterBase { test("decode dynamically empty fun") { rewriterType: SMTEncoding => // this domain is not empty at the arena level, but it is in every SMT model - def dynEmpty(left: TBuilderInstruction): TBuilderInstruction = + def dynEmpty(left: BuilderT): BuilderT = filter(name("t", IntT1), left, bool(false)) val domEx = dynEmpty(enumSet(int(1))) @@ -246,7 +246,7 @@ trait TestSymbStateDecoder extends RewriterBase { val recEx = rec( "a" -> int(1), "b" -> bool(true), - ).map(_.withTag(Typed(parser("{ a: Int, b: Bool }")))) + ).withTag(Typed(parser("{ a: Int, b: Bool }"))) val state = new SymbState(recEx, arena, Binding()) val rewriter = create(rewriterType) val nextState = rewriter.rewriteUntilDone(state) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAction.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAction.scala index b741f7255f..cbd771fabb 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAction.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAction.scala @@ -3,7 +3,8 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt.SymbStateRewriter.Continue import at.forsyte.apalache.tla.lir.IntT1 -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} +import at.forsyte.apalache.tla.typecomp._ trait TestSymbStateRewriterAction extends RewriterBase { test("""x' is rewritten to the binding of x'""") { rewriterType: SMTEncoding => diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterApalacheGen.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterApalacheGen.scala index 063e46ec2e..5d64a3a6be 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterApalacheGen.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterApalacheGen.scala @@ -6,7 +6,8 @@ import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.convenience.{tla => tlaLegacy} import at.forsyte.apalache.tla.lir.oper.ApalacheOper import at.forsyte.apalache.tla.types.parser.DefaultType1Parser -import at.forsyte.apalache.tla.types.tla._ +import at.forsyte.apalache.tla.types.tlaU._ +import at.forsyte.apalache.tla.typecomp._ trait TestSymbStateRewriterApalacheGen extends RewriterBase { private val parser = DefaultType1Parser diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAssignment.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAssignment.scala index 09dac17186..ede1eb8a8b 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAssignment.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAssignment.scala @@ -2,8 +2,8 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla._ +import at.forsyte.apalache.tla.types.{BuilderUT => BuilderT} +import at.forsyte.apalache.tla.types.tlaU._ /** * Tests for assignments. The assignments were at the core of Apalache 0.5.x. In Apalache 0.6.x, they are preprocessed @@ -12,19 +12,19 @@ import at.forsyte.apalache.tla.types.tla._ trait TestSymbStateRewriterAssignment extends RewriterBase { val ibI: TlaType1 = TupT1(IntT1, BoolT1, SetT1(IntT1)) - private val set12: TBuilderInstruction = enumSet(int(1), int(2)) - private val x_prime: TBuilderInstruction = prime(name("x", IntT1)) - private val x_primeS: TBuilderInstruction = prime(name("x", SetT1(IntT1))) - private val x_primeFbi: TBuilderInstruction = prime(name("x", FunT1(BoolT1, IntT1))) - private val x_primeFii: TBuilderInstruction = prime(name("x", FunT1(IntT1, IntT1))) - private val x_primeFib: TBuilderInstruction = prime(name("x", FunT1(IntT1, BoolT1))) - private val y_prime: TBuilderInstruction = prime(name("y", IntT1)) - private val boundName: TBuilderInstruction = name("t", IntT1) - private val boundNameS: TBuilderInstruction = name("t", SetT1(IntT1)) - private val boundNameFbi: TBuilderInstruction = name("t", FunT1(BoolT1, IntT1)) - private val boundNameFii: TBuilderInstruction = name("t", FunT1(IntT1, IntT1)) - private val boundNameFib: TBuilderInstruction = name("t", FunT1(IntT1, BoolT1)) - private val boolset: TBuilderInstruction = enumSet(bool(false), bool(true)) + private val set12: BuilderT = enumSet(int(1), int(2)) + private val x_prime: BuilderT = prime(name("x", IntT1)) + private val x_primeS: BuilderT = prime(name("x", SetT1(IntT1))) + private val x_primeFbi: BuilderT = prime(name("x", FunT1(BoolT1, IntT1))) + private val x_primeFii: BuilderT = prime(name("x", FunT1(IntT1, IntT1))) + private val x_primeFib: BuilderT = prime(name("x", FunT1(IntT1, BoolT1))) + private val y_prime: BuilderT = prime(name("y", IntT1)) + private val boundName: BuilderT = name("t", IntT1) + private val boundNameS: BuilderT = name("t", SetT1(IntT1)) + private val boundNameFbi: BuilderT = name("t", FunT1(BoolT1, IntT1)) + private val boundNameFii: BuilderT = name("t", FunT1(IntT1, IntT1)) + private val boundNameFib: BuilderT = name("t", FunT1(IntT1, BoolT1)) + private val boolset: BuilderT = enumSet(bool(false), bool(true)) test("""\E t \in {1, 2}: x' \in {t} ~~> TRUE and [x -> $C$k]""") { rewriterType: SMTEncoding => val asgn = skolem(exists(boundName, set12, assign(x_prime, boundName))) @@ -98,7 +98,7 @@ trait TestSymbStateRewriterAssignment extends RewriterBase { test("""\E t \in \in {t_2 \in {1}: FALSE}: x' \in {t} ~~> FALSE""") { rewriterType: SMTEncoding => // a regression test - def empty(set: TBuilderInstruction): TBuilderInstruction = { + def empty(set: BuilderT): BuilderT = { filter(name("t_2", IntT1), set, bool(false)) } @@ -181,7 +181,7 @@ trait TestSymbStateRewriterAssignment extends RewriterBase { test("""\E t \in {{1, 2}, {1+1, 2, 3}} \ {{2, 3}}: x' \in {t} ~~> TRUE and [x -> $C$k]""") { rewriterType: SMTEncoding => // equal elements in different sets mess up picking from a set - def setminus(left: TBuilderInstruction, right: TBuilderInstruction): TBuilderInstruction = { + def setminus(left: BuilderT, right: BuilderT): BuilderT = { // this is how Keramelizer translates setminus filter(name("t_2", SetT1(IntT1)), left, not(eql(name("t_2", SetT1(IntT1)), right))) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterChooseOrGuess.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterChooseOrGuess.scala index 8d60b6fdca..0181f58083 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterChooseOrGuess.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterChooseOrGuess.scala @@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.lir.IntT1 -import at.forsyte.apalache.tla.types.tla._ +import at.forsyte.apalache.tla.types.tlaU._ trait TestSymbStateRewriterChooseOrGuess extends RewriterBase { test("""CHOOSE x \in { 1, 2, 3 }: x > 1""") { rewriterType: SMTEncoding => diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterFunSet.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterFunSet.scala index 6a712f5161..57699ff2e0 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterFunSet.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterFunSet.scala @@ -3,8 +3,8 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt.types._ import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla._ +import at.forsyte.apalache.tla.types.{BuilderUT => BuilderT} +import at.forsyte.apalache.tla.types.tlaU._ trait TestSymbStateRewriterFunSet extends RewriterBase { val i_to_B: TlaType1 = FunT1(IntT1, SetT1(BoolT1)) @@ -172,7 +172,7 @@ trait TestSymbStateRewriterFunSet extends RewriterBase { // this should be redundant in the presence of #91 test("""[x \in {0, 1, 2} \ {0} |-> 3] \in [{1, 2} -> {3, 4}]""") { rewriterType: SMTEncoding => // although 0 is in the function domain at the arena level, it does not belong to the set difference - def setminus(set: TBuilderInstruction, intVal: BigInt): TBuilderInstruction = { + def setminus(set: BuilderT, intVal: BigInt): BuilderT = { filter(name("t", IntT1), set, not(eql(name("t", IntT1), int(intVal)))) } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRecord.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRecord.scala index fbe0d667d2..16e37f9ded 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRecord.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRecord.scala @@ -3,7 +3,7 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt.types._ import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla._ +import at.forsyte.apalache.tla.types.tlaU._ import scala.collection.immutable.{SortedMap, SortedSet, TreeMap} @@ -82,7 +82,7 @@ trait TestSymbStateRewriterRecord extends RewriterBase { val record = rec( "a" -> int(1), "b" -> bool(false), - ).map { _.withTag(Typed(ribs)) } + ).withTag(Typed(ribs)) // We assume that record has the type RecT1("a" -> IntT1, "b" -> BoolT1, "c" -> StrT1). // This can happen due to type unification. The record access should still work, // though the access is expected to produce an arbitrary value (of proper type). @@ -130,7 +130,7 @@ trait TestSymbStateRewriterRecord extends RewriterBase { val record1 = rec( "a" -> int(1), "b" -> bool(false), - ).map { _.withTag(Typed(ribs)) } + ).withTag(Typed(ribs)) val record2 = rec( "a" -> int(2), "b" -> bool(true), @@ -165,7 +165,7 @@ trait TestSymbStateRewriterRecord extends RewriterBase { // and then -- when knowing the type of the filtered records -- map them somewhere. // Although, it is not easy to do in a symbolic encoding, we support this idiom. // We require though that all the records have type-compatible fields. - val record1 = rec("a" -> int(1)).map { _.withTag(Typed(rii)) } + val record1 = rec("a" -> int(1)).withTag(Typed(rii)) val record2 = rec("a" -> int(2), "c" -> int(3)) // Records in a set can have different sets of keys. This requires a type annotation. val setEx = enumSet(record1, record2) @@ -207,7 +207,7 @@ trait TestSymbStateRewriterRecord extends RewriterBase { "b" -> bool(false), "c" -> str("d"), ) - val record2 = rec("a" -> int(1)).map { _.withTag(Typed(ribs)) } + val record2 = rec("a" -> int(1)).withTag(Typed(ribs)) val eq = not(eql(record1, record2)) val state = new SymbState(eq, arena, Binding()) val rewriter = create(rewriterType) @@ -229,7 +229,7 @@ trait TestSymbStateRewriterRecord extends RewriterBase { } test("""DOMAIN [a |-> 1] = {"a"} under type annotations!""") { rewriterType: SMTEncoding => - val record = rec("a" -> int(1)).map(_.withTag(Typed(ribs))) + val record = rec("a" -> int(1)).withTag(Typed(ribs)) val domain = dom(record) val eq = eql(domain, enumSet(str("a"))) val state = new SymbState(eq, arena, Binding()) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRepeat.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRepeat.scala new file mode 100644 index 0000000000..29c525816b --- /dev/null +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRepeat.scala @@ -0,0 +1,45 @@ +package at.forsyte.apalache.tla.bmcmt + +import at.forsyte.apalache.infra.passes.options.SMTEncoding +import at.forsyte.apalache.tla.lir._ +import at.forsyte.apalache.tla.types.{tlaU => tla} + +trait TestSymbStateRewriterRepeat extends RewriterBase { + test("""Repeat(LET Op(a,i) == a + 1 IN Op, 5, 0) = 5""") { rewriterType: SMTEncoding => + // Op(x, i) == x + 1 + val opT = OperT1(Seq(IntT1, IntT1), IntT1) + + val plusOneEx = tla.plus(tla.name("x", IntT1), tla.int(1)) + val plusOneOper = tla.decl("Op", plusOneEx, tla.param("x", IntT1), tla.param("i", IntT1)) + val letEx = tla.letIn(tla.name(plusOneOper.name, opT), plusOneOper) + val repeatEx = tla.repeat(letEx, 5, tla.int(0)) + + val rewriter = create(rewriterType) + var state = new SymbState(repeatEx, arena, Binding()) + state = rewriter.rewriteUntilDone(state) + val asCell = state.asCell + + // compare the value + val eqn = tla.eql(asCell.toBuilder, tla.int(5)) + assertTlaExAndRestore(rewriter, state.setRex(eqn)) + } + + test("""Repeat(LET Op(a,i) == a + i IN Op, 5, 0) = 15""") { rewriterType: SMTEncoding => + // Op(x, i) == x + i + val opT = OperT1(Seq(IntT1, IntT1), IntT1) + + val plusiEx = tla.plus(tla.name("x", IntT1), tla.name("i", IntT1)) + val plusiOper = tla.decl("Op", plusiEx, tla.param("x", IntT1), tla.param("i", IntT1)) + val letEx = tla.letIn(tla.name(plusiOper.name, opT), plusiOper) + val repeatEx = tla.repeat(letEx, 5, tla.int(0)) + + val rewriter = create(rewriterType) + var state = new SymbState(repeatEx, arena, Binding()) + state = rewriter.rewriteUntilDone(state) + val asCell = state.asCell + + // compare the value + val eqn = tla.eql(asCell.toBuilder, tla.int(15)) + assertTlaExAndRestore(rewriter, state.setRex(eqn)) + } +} diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestPropositionalOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestPropositionalOracle.scala index 04a8b1f0f7..1302906eac 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestPropositionalOracle.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestPropositionalOracle.scala @@ -3,7 +3,8 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt.{Binding, RewriterBase, SymbState} import at.forsyte.apalache.tla.lir.{BoolT1, TestingPredefs} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} +import at.forsyte.apalache.tla.typecomp._ trait TestPropositionalOracle extends RewriterBase with TestingPredefs { test("""Propositional Oracle.create""") { rewriterType: SMTEncoding => diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestSparseOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestSparseOracle.scala index 23715cdc85..2bfbe1256e 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestSparseOracle.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestSparseOracle.scala @@ -3,7 +3,8 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt.{Binding, RewriterBase, SymbState} import at.forsyte.apalache.tla.lir.{BoolT1, TestingPredefs} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} +import at.forsyte.apalache.tla.typecomp._ trait TestSparseOracle extends RewriterBase with TestingPredefs { test("""Sparse Oracle.create""") { rewriterType: SMTEncoding => diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestUninterpretedConstOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestUninterpretedConstOracle.scala index 9c25fbee6c..8533863012 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestUninterpretedConstOracle.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestUninterpretedConstOracle.scala @@ -3,7 +3,8 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt.{Binding, RewriterBase, SymbState} import at.forsyte.apalache.tla.lir.{BoolT1, TestingPredefs} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} +import at.forsyte.apalache.tla.typecomp._ trait TestUninterpretedConstOracle extends RewriterBase with TestingPredefs { test("""UninterpretedConst Oracle.create""") { rewriterType: SMTEncoding => diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContext.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContext.scala index 56052ad099..4149cd7fa7 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContext.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContext.scala @@ -2,8 +2,8 @@ package at.forsyte.apalache.tla.bmcmt.smt import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter import at.forsyte.apalache.tla.lir.IntT1 -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} +import at.forsyte.apalache.tla.typecomp._ import org.scalatest.funsuite.AnyFunSuite /** @@ -13,7 +13,7 @@ import org.scalatest.funsuite.AnyFunSuite trait TestRecordingSolverContext extends AnyFunSuite { protected var solverConfig: SolverConfig = _ - private val int42: TBuilderInstruction = tla.int(42) + private val int42: BuilderT = tla.int(42) test("operations proxied") { val solver = RecordingSolverContext.createZ3(None, solverConfig) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/ApalacheRewriterTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/ApalacheRewriterTest.scala index b7868f2683..dfeb025d37 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/ApalacheRewriterTest.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/ApalacheRewriterTest.scala @@ -3,8 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules import at.forsyte.apalache.tla.bmcmt.stratifiedRules.apalache.AssignmentStratifiedRule import at.forsyte.apalache.tla.bmcmt.{ArenaCell, Binding, PureArena} import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} import org.junit.runner.RunWith import org.scalatest.BeforeAndAfterEach import org.scalatest.funsuite.AnyFunSuite @@ -27,7 +26,7 @@ class ApalacheRewriterTest extends AnyFunSuite with BeforeAndAfterEach { val rule = new AssignmentStratifiedRule(rewriter) - def assignTo(lhs: TBuilderInstruction, rhs: TBuilderInstruction = tla.int(1)): TBuilderInstruction = + def assignTo(lhs: BuilderT, rhs: BuilderT = tla.int(1)): BuilderT = tla.assign(tla.prime(lhs), rhs) val startScope = RewriterScope.initial() diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/BoolRewriterTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/BoolRewriterTest.scala index 9736d3d815..04a12f6a2b 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/BoolRewriterTest.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/BoolRewriterTest.scala @@ -2,7 +2,8 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules import at.forsyte.apalache.tla.bmcmt.{ArenaCell, Binding, PureArena} import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} +import at.forsyte.apalache.tla.typecomp._ import org.junit.runner.RunWith import org.scalatest.BeforeAndAfterEach import org.scalatest.funsuite.AnyFunSuite diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/IntRewriterTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/IntRewriterTest.scala index 21e75e24cd..916f15299c 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/IntRewriterTest.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/IntRewriterTest.scala @@ -1,7 +1,8 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules import at.forsyte.apalache.tla.lir.{IntT1, NameEx, SetT1, Typed} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} +import at.forsyte.apalache.tla.typecomp._ import org.junit.runner.RunWith import org.scalatest.BeforeAndAfterEach import org.scalatest.funsuite.AnyFunSuite diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/SetRewriterTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/SetRewriterTest.scala index 562a148bf3..7332b32b19 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/SetRewriterTest.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/SetRewriterTest.scala @@ -4,7 +4,8 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.set.SetFilterStratifiedRule import at.forsyte.apalache.tla.bmcmt.types.CellT import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} +import at.forsyte.apalache.tla.typecomp._ import org.junit.runner.RunWith import org.scalatest.BeforeAndAfterEach import org.scalatest.funsuite.AnyFunSuite diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntRangeCacheTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntRangeCacheTest.scala index 4b83e8acb8..6494248f02 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntRangeCacheTest.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntRangeCacheTest.scala @@ -2,7 +2,8 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux import at.forsyte.apalache.tla.bmcmt.PureArena import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.{IntRangeCache, IntValueCache} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} +import at.forsyte.apalache.tla.typecomp._ import org.junit.runner.RunWith import org.scalatest.BeforeAndAfterEach import org.scalatest.funsuite.AnyFunSuite diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntValueCacheTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntValueCacheTest.scala index 7895f465c8..2193bb49cb 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntValueCacheTest.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntValueCacheTest.scala @@ -2,7 +2,8 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux import at.forsyte.apalache.tla.bmcmt.PureArena import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.IntValueCache -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} +import at.forsyte.apalache.tla.typecomp._ import org.junit.runner.RunWith import org.scalatest.BeforeAndAfterEach import org.scalatest.funsuite.AnyFunSuite diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/RecordDomainCacheTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/RecordDomainCacheTest.scala index 004243cf2a..f99923ad5b 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/RecordDomainCacheTest.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/RecordDomainCacheTest.scala @@ -3,7 +3,8 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux import at.forsyte.apalache.tla.bmcmt.PureArena import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.{RecordDomainCache, UninterpretedLiteralCache} import at.forsyte.apalache.tla.lir.{StrT1, TlaType1} -import at.forsyte.apalache.tla.types.{tla, ModelValueHandler} +import at.forsyte.apalache.tla.types.{tlaU => tla, ModelValueHandler} +import at.forsyte.apalache.tla.typecomp._ import org.junit.runner.RunWith import org.scalatest.BeforeAndAfterEach import org.scalatest.funsuite.AnyFunSuite diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/UninterpretedLiteralCacheTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/UninterpretedLiteralCacheTest.scala index 868cfa9e87..a9083a80d5 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/UninterpretedLiteralCacheTest.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/UninterpretedLiteralCacheTest.scala @@ -3,7 +3,8 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux import at.forsyte.apalache.tla.bmcmt.PureArena import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.UninterpretedLiteralCache import at.forsyte.apalache.tla.lir.{StrT1, TlaType1} -import at.forsyte.apalache.tla.types.{tla, ModelValueHandler} +import at.forsyte.apalache.tla.types.{tlaU => tla, ModelValueHandler} +import at.forsyte.apalache.tla.typecomp._ import org.junit.runner.RunWith import org.scalatest.BeforeAndAfterEach import org.scalatest.funsuite.AnyFunSuite diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestIntOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestIntOracle.scala index 8485c3f3e4..d24d073693 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestIntOracle.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestIntOracle.scala @@ -7,8 +7,8 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope import at.forsyte.apalache.tla.lir.{BoolT1, NameEx, OperEx, TlaEx, ValEx} import at.forsyte.apalache.tla.lir.oper.TlaOper import at.forsyte.apalache.tla.lir.values.TlaInt -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} +import at.forsyte.apalache.tla.typecomp._ import org.junit.runner.RunWith import org.scalacheck.{Gen, Prop} import org.scalacheck.Prop.forAll @@ -62,7 +62,7 @@ class TestIntOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers { } - val (assertionsA, assertionsB): (Seq[TBuilderInstruction], Seq[TBuilderInstruction]) = 0 + val (assertionsA, assertionsB): (Seq[BuilderT], Seq[BuilderT]) = 0 .to(10) .map { i => (tla.name(s"A$i", BoolT1), tla.name(s"B$i", BoolT1)) @@ -70,7 +70,7 @@ class TestIntOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers { .unzip test("caseAssertions requires assertion sequences of equal length") { - val assertionsGen: Gen[(Seq[TBuilderInstruction], Option[Seq[TBuilderInstruction]])] = for { + val assertionsGen: Gen[(Seq[BuilderT], Option[Seq[BuilderT]])] = for { i <- Gen.choose(0, assertionsA.size) j <- Gen.choose(0, assertionsB.size) opt <- Gen.option(Gen.const(assertionsB.take(j))) @@ -91,7 +91,7 @@ class TestIntOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers { } test("caseAssertions constructs a collection of ITEs, or shorthands") { - val gen: Gen[(Int, Seq[TBuilderInstruction], Option[Seq[TBuilderInstruction]])] = for { + val gen: Gen[(Int, Seq[BuilderT], Option[Seq[BuilderT]])] = for { size <- nonNegIntGen opt <- Gen.option(Gen.const(assertionsB.take(size))) } yield (size, assertionsA.take(size), opt) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestMockOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestMockOracle.scala index 74afa816a8..a1c065d805 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestMockOracle.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestMockOracle.scala @@ -4,8 +4,8 @@ import at.forsyte.apalache.tla.bmcmt.smt.{SolverConfig, Z3SolverContext} import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.values.TlaBool -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} +import at.forsyte.apalache.tla.typecomp._ import org.junit.runner.RunWith import org.scalacheck.Prop.forAll import org.scalacheck.{Gen, Prop} @@ -58,7 +58,7 @@ class TestMockOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers { check(prop, minSuccessful(1000), sizeRange(4)) } - val (assertionsA, assertionsB): (Seq[TBuilderInstruction], Seq[TBuilderInstruction]) = 0 + val (assertionsA, assertionsB): (Seq[BuilderT], Seq[BuilderT]) = 0 .to(10) .map { i => (tla.name(s"A$i", BoolT1), tla.name(s"B$i", BoolT1)) @@ -66,7 +66,7 @@ class TestMockOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers { .unzip test("caseAssertions requires assertion sequences of equal length") { - val assertionsGen: Gen[(Seq[TBuilderInstruction], Option[Seq[TBuilderInstruction]])] = for { + val assertionsGen: Gen[(Seq[BuilderT], Option[Seq[BuilderT]])] = for { i <- Gen.choose(0, assertionsA.size) j <- Gen.choose(0, assertionsB.size) opt <- Gen.option(Gen.const(assertionsB.take(j))) @@ -86,7 +86,7 @@ class TestMockOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers { } test("caseAssertions always shorthands") { - val gen: Gen[(Int, Seq[TBuilderInstruction], Option[Seq[TBuilderInstruction]])] = for { + val gen: Gen[(Int, Seq[BuilderT], Option[Seq[BuilderT]])] = for { fixed <- nonNegIntGen opt <- Gen.option(Gen.const(assertionsB.take(fixed + 1))) } yield (fixed, assertionsA.take(fixed + 1), opt) 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 index c2c40e1007..a7b09be08c 100644 --- 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 @@ -6,8 +6,8 @@ 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 at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} +import at.forsyte.apalache.tla.typecomp._ import org.junit.runner.RunWith import org.scalacheck.Gen import org.scalacheck.Prop.forAll @@ -59,7 +59,7 @@ class TestSparseOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers check(prop, minSuccessful(1000), sizeRange(4)) } - val (assertionsA, assertionsB): (Seq[TBuilderInstruction], Seq[TBuilderInstruction]) = 0 + val (assertionsA, assertionsB): (Seq[BuilderT], Seq[BuilderT]) = 0 .to(10) .map { i => (tla.name(s"A$i", BoolT1), tla.name(s"B$i", BoolT1)) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestUninterpretedConstOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestUninterpretedConstOracle.scala index 6688fbc3df..4b047c464c 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestUninterpretedConstOracle.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestUninterpretedConstOracle.scala @@ -7,8 +7,8 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.UninterpretedLit import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope, TestingRewriter} import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper.TlaOper -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} +import at.forsyte.apalache.tla.typecomp._ import org.junit.runner.RunWith import org.scalacheck.Prop.forAll import org.scalacheck.{Gen, Prop} @@ -69,7 +69,7 @@ class TestUninterpretedConstOracle extends AnyFunSuite with BeforeAndAfterEach w check(prop, minSuccessful(200), sizeRange(4)) } - val (assertionsA, assertionsB): (Seq[TBuilderInstruction], Seq[TBuilderInstruction]) = 0 + val (assertionsA, assertionsB): (Seq[BuilderT], Seq[BuilderT]) = 0 .to(10) .map { i => (tla.name(s"A$i", BoolT1), tla.name(s"B$i", BoolT1)) @@ -77,7 +77,7 @@ class TestUninterpretedConstOracle extends AnyFunSuite with BeforeAndAfterEach w .unzip test("caseAssertions requires assertion sequences of equal length") { - val assertionsGen: Gen[(Seq[TBuilderInstruction], Option[Seq[TBuilderInstruction]])] = for { + val assertionsGen: Gen[(Seq[BuilderT], Option[Seq[BuilderT]])] = for { i <- Gen.choose(0, assertionsA.size) j <- Gen.choose(0, assertionsB.size) opt <- Gen.option(Gen.const(assertionsB.take(j))) @@ -97,7 +97,7 @@ class TestUninterpretedConstOracle extends AnyFunSuite with BeforeAndAfterEach w } test("caseAssertions constructs a collection of ITEs, or shorthands") { - val gen: Gen[(Int, Seq[TBuilderInstruction], Option[Seq[TBuilderInstruction]])] = for { + val gen: Gen[(Int, Seq[BuilderT], Option[Seq[BuilderT]])] = for { size <- nonNegIntGen opt <- Gen.option(Gen.const(assertionsB.take(size))) } yield (size, assertionsA.take(size), opt) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala index 0b544e080a..ed9044555b 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala @@ -2,8 +2,8 @@ package at.forsyte.apalache.tla.bmcmt.trex import at.forsyte.apalache.tla.bmcmt.{Binding, StateInvariant} import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} +import at.forsyte.apalache.tla.typecomp._ /** * An abstract test suite that is parameterized by the snapshot type. @@ -16,8 +16,8 @@ import at.forsyte.apalache.tla.types.tla */ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] { - def nX: TBuilderInstruction = tla.name("x", IntT1) - def nY: TBuilderInstruction = tla.name("y", IntT1) + def nX: BuilderT = tla.name("x", IntT1) + def nY: BuilderT = tla.name("y", IntT1) test("constant initialization") { exeCtx: ExecutorContextT => // N' <- 1 @@ -129,7 +129,7 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] { // state 1 is produced by transition 1 assert(1 == decPath(1)._2) - def mapWithBuild(pairs: (String, TBuilderInstruction)*): Map[String, TlaEx] = + def mapWithBuild(pairs: (String, BuilderT)*): Map[String, TlaEx] = pairs.map { case (a, b) => a -> b.build }.toMap assert(mapWithBuild("x" -> tla.int(1), "y" -> tla.int(1)) == decPath(1)._1) @@ -225,9 +225,9 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] { assert(!mayChange2) } - private def mkAssign(name: String, value: Int): TBuilderInstruction = + private def mkAssign(name: String, value: Int): BuilderT = tla.assign(tla.prime(tla.name(name, IntT1)), tla.int(value)) - private def mkAssignInt(name: String, rhs: TBuilderInstruction) = + private def mkAssignInt(name: String, rhs: BuilderT) = tla.assign(tla.prime(tla.name(name, IntT1)), rhs) } diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/json/BuilderCallByName.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/json/BuilderCallByName.scala index 94a2443f74..600d10911c 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/io/json/BuilderCallByName.scala +++ b/tla-io/src/main/scala/at/forsyte/apalache/io/json/BuilderCallByName.scala @@ -103,6 +103,7 @@ object BuilderCallByName { ApalacheOper.mkSeq.name -> ApalacheOper.mkSeq, ApalacheOper.foldSet.name -> ApalacheOper.foldSet, ApalacheOper.foldSeq.name -> ApalacheOper.foldSeq, + ApalacheOper.repeat.name -> ApalacheOper.repeat, ApalacheInternalOper.selectInSet.name -> ApalacheInternalOper.selectInSet, ApalacheInternalOper.selectInFun.name -> ApalacheInternalOper.selectInFun, ApalacheInternalOper.storeInSet.name -> ApalacheInternalOper.storeInSet, @@ -375,6 +376,15 @@ object BuilderCallByName { case ApalacheOper.foldSeq => val Seq(f, v, s) = args tla.foldSeq(f, v, s) + case ApalacheOper.repeat => + val Seq(f, n, x) = args + val nEx: TlaEx = n + nEx match { + case ValEx(TlaInt(n)) => + tla.repeat(f, n, x) + // should never happen, for case-completeness + case _ => throw new JsonDeserializationError(s"${oper.name} requires an integer argument.") + } case ApalacheInternalOper.selectInSet => val Seq(x, s) = args tla.selectInSet(x, s) diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala index fc16c54ec2..5c965f921f 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala +++ b/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala @@ -655,9 +655,13 @@ class Quint(quintOutput: QuintOutput) { // Convert Quint's nondet variable binding // - // val nondet name = oneOf(domain); scope + // nondet name = oneOf(domain); scope // ~~> // \E name \in domain: scope + // + // nondet name = generate(sz, typeSet); scope + // ~~> + // \E name \in { Apalache!Gen(sz) }: scope private val nondetBinding: (QuintDef.QuintOpDef, QuintEx) => NullaryOpReader[TBuilderInstruction] = { case (QuintDef.QuintOpDef(_, name, "nondet", QuintApp(id, "oneOf", Seq(domain))), scope) => val elemType = typeConv.convert(types(id).typ) @@ -666,6 +670,19 @@ class Quint(quintOutput: QuintOutput) { tlaDomain <- tlaExpression(domain) tlaScope <- tlaExpression(scope) } yield tla.exists(tlaName, tlaDomain, tlaScope) + + case (QuintDef.QuintOpDef(_, name, "nondet", QuintApp(id, "generate", Seq(bound, _))), scope) => + val elemType = typeConv.convert(types(id).typ) + val boundIntConst = intFromExpr(bound) + if (boundIntConst.isEmpty) { + throw new QuintIRParseError(s"nondet $name = generate($bound) ... expects an integer constant") + } + val genExpr = tla.enumSet(tla.gen(boundIntConst.get, elemType)) + val tlaName = tla.name(name, elemType) + for { + tlaScope <- tlaExpression(scope) + } yield tla.exists(tlaName, genExpr, tlaScope) + case invalidValue => throw new QuintIRParseError(s"nondet keyword used to bind invalid value ${invalidValue}") } @@ -804,4 +821,14 @@ class Quint(quintOutput: QuintOutput) { .reverse // Return the declarations to their original order } } yield TlaModule(module.name, declarations) + + private def intFromExpr(expr: QuintEx): Option[BigInt] = { + expr match { + case QuintInt(_, value) => + Some(value) + + case _ => + None + } + } } diff --git a/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/StandardLibrary.scala b/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/StandardLibrary.scala index 380e43075d..2c601465a4 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/StandardLibrary.scala +++ b/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/StandardLibrary.scala @@ -67,6 +67,7 @@ object StandardLibrary { ("Apalache", "ApaFoldSet") -> ApalacheOper.foldSet, ("__apalache_folds", "__ApalacheFoldSet") -> ApalacheOper.foldSet, ("Apalache", "ApaFoldSeqLeft") -> ApalacheOper.foldSeq, + ("Apalache", "Repeat") -> ApalacheOper.repeat, // Variants ("Variants", "Variant") -> VariantOper.variant, ("Variants", "VariantFilter") -> VariantOper.variantFilter, diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala index 06dfd20177..ee84a40fb5 100644 --- a/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala +++ b/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala @@ -172,7 +172,15 @@ class TestQuintEx extends AnyFunSuite { val chooseSomeFromIntSet = app("chooseSome", intSet)(QuintIntT()) val oneOfSet = app("oneOf", intSet)(QuintIntT()) val nondetBinding = - e(QuintLet(uid, d(QuintDef.QuintOpDef(uid, "n", "nondet", oneOfSet), QuintIntT()), nIsGreaterThan0), QuintIntT()) + e(QuintLet(uid, d(QuintDef.QuintOpDef(uid, "n", "nondet", oneOfSet), QuintIntT()), nIsGreaterThan0), QuintBoolT()) + val generateSet = app("generate", _42, app("Set", _42)(QuintSetT(QuintIntT())))(QuintSetT(QuintIntT())) + val nondetGenerateId = uid + val appGenSet = + app("eq", e(QuintName(uid, "S"), QuintSetT(QuintIntT())), app("Set")(QuintSetT(QuintIntT())))(QuintBoolT()) + val nondetGenerate = + e(QuintLet(uid, + d(QuintDef.QuintOpDef(nondetGenerateId, "S", "nondet", generateSet), + QuintOperT(Seq(), QuintSetT(QuintIntT()))), appGenSet), QuintBoolT()) // Requires ID registered with type val selectGreaterThanZero = app("select", intList, intIsGreaterThanZero)(QuintSeqT(QuintIntT())) val addOne = app("iadd", name, _1)(QuintIntT()) @@ -710,10 +718,14 @@ class TestQuintEx extends AnyFunSuite { assert(convert(Q.app("put", Q.intMap, Q._3, Q._42)(intMapT)) == expected) } - test("can convert nondet bindings") { + test("can convert nondet...oneOf") { assert(convert(Q.nondetBinding) == "∃n ∈ {1, 2, 3}: (n > 0)") } + test("can convert nondet...generate") { + assert(convert(Q.nondetGenerate) == "∃S ∈ {Apalache!Gen(42)}: (S = {})") + } + test("can convert let binding with reference to name in scope") { assert(convert(Q.letNbe42inNisGreaterThan0) == "LET n ≜ 42 IN n() > 0") } diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ConstSimplifierBase.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ConstSimplifierBase.scala index ad8a5209c2..23cbe6f36b 100644 --- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ConstSimplifierBase.scala +++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ConstSimplifierBase.scala @@ -3,7 +3,7 @@ package at.forsyte.apalache.tla.pp import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper._ import at.forsyte.apalache.tla.lir.values.{TlaBool, TlaInt, TlaStr} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderT, BuilderUT} /** *

A base class for constant simplification that is shared by more specialized simplifiers.

@@ -239,4 +239,9 @@ abstract class ConstSimplifierBase { case ex => ex } + + def applySimplifyShallowToBuilderEx(ex: BuilderUT): BuilderUT = + simplifyShallow(ex) // when using TlaEx + def applySimplifyShallowToBuilderEx(ex: BuilderT): BuilderT = + ex.map(simplifyShallow) // when using TBuilderInstruction } 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/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala index fe66a87847..118d33d251 100644 --- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala +++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/SetMembershipSimplifier.scala @@ -87,7 +87,7 @@ class SetMembershipSimplifier(tracker: TransformationTracker) extends AbstractTr // x \in TDS ~> TRUE case set if isTypeDefining(set) => trueVal - // n \in Nat ~> x >= 0 + // x \in Nat ~> x >= 0 case ValEx(TlaNatSet) => OperEx(TlaArithOper.ge, name, ValEx(TlaInt(0))(intTag))(boolTag) // fun \in [Dom -> TDS] ~> DOMAIN fun = Dom (fun \in [TDS1 -> TDS2] is handled above) 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) } diff --git a/tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala b/tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala index 50765b5387..780320bf44 100644 --- a/tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala +++ b/tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala @@ -810,6 +810,12 @@ class ToEtcExpr( mkExRefApp(opsig, Seq(v, variantEx, defaultEx)) // ******************************************** Apalache ************************************************** + case OperEx(ApalacheOper.repeat, op, bound, base) => + val a = varPool.fresh + // ((a, Int) => a, Int, a) => a + val opsig = OperT1(Seq(OperT1(Seq(a, IntT1), a), IntT1, a), a) + mkExRefApp(opsig, Seq(op, bound, base)) + case OperEx(ApalacheOper.mkSeq, len, ctor) => val a = varPool.fresh // (Int, (Int => a)) => Seq(a) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ArenaCell.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ArenaCell.scala index 44f917e358..6e9e9a9d47 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ArenaCell.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ArenaCell.scala @@ -2,9 +2,9 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.tla.bmcmt.PureArena.namePrefix import at.forsyte.apalache.tla.lir.{NameEx, TlaEx} -import at.forsyte.apalache.tla.typecomp -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} import at.forsyte.apalache.tla.bmcmt.types.CellT +import at.forsyte.apalache.tla.typecomp._ object ArenaCell { def isValidName(name: String): Boolean = { @@ -44,7 +44,7 @@ class ArenaCell(val id: Int, val cellType: CellT, val isUnconstrained: Boolean = * @return * a builder instruction that can be used with the typed builder */ - def toBuilder: typecomp.TBuilderInstruction = tla.name(toString, cellType.toTlaType1) + def toBuilder: BuilderT = tla.name(toString, cellType.toTlaType1) def mkTlaEq(rhs: ArenaCell): TlaEx = tla.eql(this.toBuilder, rhs.toBuilder) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ElemPtr.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ElemPtr.scala index c35692625e..6e97dce712 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ElemPtr.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ElemPtr.scala @@ -1,7 +1,6 @@ package at.forsyte.apalache.tla.bmcmt -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * An abstract membership pointer. @@ -18,7 +17,7 @@ sealed trait ElemPtr { /** * Translate the membership test into an expression that can be understood by Z3SolverContext. */ - def toSmt: TBuilderInstruction + def toSmt: BuilderT /** * After certain set operations, every pointer must become a SmtExprElemPtr, because the operation invalidates the @@ -31,7 +30,7 @@ sealed trait ElemPtr { * filter). `ptr.restrict(x)` returns `ptr2`, such that `ptr2.toSmt` is logically equivalent (but not necessarily * syntactically equal) to `tla.and(ptr.toSmt, x)`, while `ptr.elem = ptr2.elem`. */ - def restrict(cond: TBuilderInstruction): SmtExprElemPtr + def restrict(cond: BuilderT): SmtExprElemPtr } /** @@ -42,9 +41,9 @@ sealed trait ElemPtr { * the element this pointer is pointing to. */ case class FixedElemPtr(elem: ArenaCell) extends ElemPtr { - override def toSmt: TBuilderInstruction = tla.bool(true) + override def toSmt: BuilderT = tla.bool(true) - override def restrict(cond: TBuilderInstruction): SmtExprElemPtr = SmtExprElemPtr(elem, cond) + override def restrict(cond: BuilderT): SmtExprElemPtr = SmtExprElemPtr(elem, cond) } /** @@ -56,7 +55,7 @@ case class FixedElemPtr(elem: ArenaCell) extends ElemPtr { * @param smtEx * the corresponding SMT expression. */ -case class SmtExprElemPtr(elem: ArenaCell, smtEx: TBuilderInstruction) extends ElemPtr { - override def toSmt: TBuilderInstruction = smtEx - def restrict(cond: TBuilderInstruction): SmtExprElemPtr = this.copy(smtEx = tla.and(smtEx, cond)) +case class SmtExprElemPtr(elem: ArenaCell, smtEx: BuilderT) extends ElemPtr { + override def toSmt: BuilderT = smtEx + def restrict(cond: BuilderT): SmtExprElemPtr = this.copy(smtEx = tla.and(smtEx, cond)) } diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/ApalacheOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/ApalacheOper.scala index bd291c2241..f17344c907 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/ApalacheOper.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/ApalacheOper.scala @@ -167,6 +167,19 @@ object ApalacheOper { override val precedence: (Int, Int) = (100, 100) } + /** + * Repeated applicaiton of an operator. + * + * The type signature is: `\forall T: Repeat: ((T, Int) => T, Int, T) => T` + */ + object repeat extends ApalacheOper { + override def name: String = "Apalache!Repeat" + + override def arity: OperArity = FixedArity(3) + + override val precedence: (Int, Int) = (100, 100) + } + /** *

The operator SetAsFun converts a set of pairs `R` to a function `F`. The function `F` could be expressed as * follows:

diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeraLanguagePred.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeraLanguagePred.scala index 3a1cd4b1fd..7ca7451a75 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeraLanguagePred.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeraLanguagePred.scala @@ -59,6 +59,11 @@ class KeraLanguagePred extends ContextualLanguagePred { isOkInContext(letDefs, opName) .and(isOkInContext(letDefs, len)) + case OperEx(ApalacheOper.repeat, opName, bound, base) => + isOkInContext(letDefs, opName) + .and(isOkInContext(letDefs, bound)) + .and(isOkInContext(letDefs, base)) + case OperEx(oper, args @ _*) if oper == TlaSetOper.map || oper == TlaFunOper.funDef || oper == TlaFunOper.recFunDef => val evenArgs = args.zipWithIndex.filter { p => p._2 % 2 == 0 }.map { diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ParamUtil.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ParamUtil.scala new file mode 100644 index 0000000000..a3dadd3420 --- /dev/null +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ParamUtil.scala @@ -0,0 +1,75 @@ +package at.forsyte.apalache.tla.typecomp + +import at.forsyte.apalache.tla.lir.{ + BoolT1, ConstT1, FunT1, IntT1, OperParam, OperT1, RealT1, RecRowT1, RecT1, RowT1, SeqT1, SetT1, SparseTupT1, StrT1, + TlaType1, TupT1, VarT1, VariantT1, +} + +object ParamUtil { + + type TypedParam = (OperParam, TlaType1) + + /** + * Evaluates whether a parameter type satisfies the type restrictions on operator parameters in TLA+. + * + * Parameters of TLA+ operators must: + * - have a non-operator type, unless they are (syntactically) marked higher-order (HO) + * - have a top-level operator type (OperT1) if they are marked HO + * - not contain `OperT1` in the type's syntax-tree in either case, except possibly at the root (if HO). In + * particular, a parameter to a HO operator with an `OperT1` type may not be HO itself. + */ + def isAcceptableParamType(canContainOper: Boolean): TlaType1 => Boolean = { + case FunT1(arg, res) => isAcceptableParamType(false)(arg) && isAcceptableParamType(false)(res) + case SetT1(elem) => isAcceptableParamType(false)(elem) + case SeqT1(elem) => isAcceptableParamType(false)(elem) + case TupT1(elems @ _*) => elems.forall(isAcceptableParamType(false)) + case SparseTupT1(fieldTypes) => fieldTypes.values.forall(isAcceptableParamType(false)) + case RecT1(fieldTypes) => fieldTypes.values.forall(isAcceptableParamType(false)) + case OperT1(args, res) => + if (canContainOper) + args.nonEmpty && + args.forall(isAcceptableParamType(false)) && + isAcceptableParamType(false)(res) + else false + case RowT1(fieldTypes, _) => fieldTypes.values.forall(isAcceptableParamType(false)) + case RecRowT1(row) => isAcceptableParamType(false)(row) + case VariantT1(row) => isAcceptableParamType(false)(row) + case IntT1 | StrT1 | BoolT1 | RealT1 | VarT1(_) | ConstT1(_) => true + } + + /** + * Throws if parameters don't satisfy [[isAcceptableParamType]]. Permits operator types iff the parameter arity is + * positive. + */ + def validateParamType(tp: TypedParam): Unit = { + val (OperParam(name, arity), tt) = tp + if (!isAcceptableParamType(canContainOper = arity > 0)(tt)) + throw new TBuilderTypeException( + s"Parameter $name type $tt and arity $arity are inconsistent. Parameters have operator types iff their arity is positive." + ) + } + + /** + * Determines the parameter arity, if the type is an operator type. We distinguish nullary operators from + * non-operators in this method. + */ + def typeAsOperArity(tt: TlaType1): Option[Int] = tt match { + case OperT1(args, _) => Some(args.size) + case _ => None + } + + /** + * Operator parameter with type information. Checks that parameters have permissible types. + */ + def param(name: String, tt: TlaType1): TypedParam = { + val arityOpt = typeAsOperArity(tt) + // operator parameters may not be nullary operators + if (arityOpt.contains(0)) + throw new TBuilderTypeException(s"Parameter $name may not have a nullary operator type $tt.") + val arity = arityOpt.getOrElse(0) // 0 here means not-an-operator + val ret = (OperParam(name, arity), tt) + validateParamType(ret) + ret + } + +} diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopeUnsafeBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopeUnsafeBuilder.scala new file mode 100644 index 0000000000..81438d1217 --- /dev/null +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopeUnsafeBuilder.scala @@ -0,0 +1,128 @@ +package at.forsyte.apalache.tla.typecomp + +import at.forsyte.apalache.tla.lir.TypedPredefs.TypeTagAsTlaType1 +import at.forsyte.apalache.tla.lir._ +import at.forsyte.apalache.tla.typecomp.unsafe.{ + UnsafeActionBuilder, UnsafeApalacheBuilder, UnsafeApalacheInternalBuilder, UnsafeArithmeticBuilder, UnsafeBaseBuilder, + UnsafeBoolBuilder, UnsafeControlBuilder, UnsafeFiniteSetBuilder, UnsafeFunBuilder, UnsafeLiteralAndNameBuilder, + UnsafeSeqBuilder, UnsafeSetBuilder, UnsafeTemporalBuilder, UnsafeVariantBuilder, +} + +/** + * Scope-unsafe Builder for TLA+ (Quint) IR expressions. + * + * The following guarantees hold for any IR tree successfully generated exclusively via ScopeUnsafeBuilder methods: + * - Typed-ness: All subexpressions will have a `Typed(_)` tag + * - Type correctness: + * - All literal expressions will have the correct type, as determined by their value ( `1: Int`, `"a" : Str`, etc.) + * - For each operator application expression `OperEx(oper, args:_*)(Typed(resultType))`, the following holds: + * - `oper(args:_*)` corresponds to some TNT operator with a signature `(T1,...,Tn) => T` + * - There exists some substitution `s`, such that: `s(T1) = typeof(args[1]), ..., s(Tn) = typeof(args[n])` and + * `s(T) = resultType`. Example: For `e @ OperEx(TlaSetOper.union, 1..4, {5})` the subexpressions `1..4, {5}` + * and `e` will all have types `Set(Int)`, since + * [[at.forsyte.apalache.tla.lir.oper.TlaSetOper.union TlaSetOper.union]] corresponds to `\union`, which has the + * signature `(Set(t), Set(t)) => Set(t)`, and the substitution required is `t -> Int`. + * + * If `strict` mode is enabled, the builder rejects inputs for ApalacheOper methods, which do not adhere to the method + * requirements ("... must be ..."), even if their types are correct. If `strict` mode is disabled, the builder should + * allow for the construction of any expression, which may be present in a freshly parsed specification (i.e. before + * preprocessing). + * + * @author + * Jure Kukovec + * @param strict + * If true, performs method requirement checks + */ +class ScopeUnsafeBuilder(val strict: Boolean = true) + extends UnsafeBaseBuilder with UnsafeBoolBuilder with UnsafeArithmeticBuilder with UnsafeSetBuilder + with UnsafeFiniteSetBuilder with UnsafeSeqBuilder with UnsafeActionBuilder with UnsafeFunBuilder + with UnsafeControlBuilder with UnsafeTemporalBuilder with UnsafeApalacheInternalBuilder with UnsafeApalacheBuilder + with UnsafeVariantBuilder with UnsafeLiteralAndNameBuilder { + + // The following two methods are included in the unsafe builder for interface compatibility with the + // scope-safe builder. They are both no-ops + def unchecked(ex: TlaEx): TlaEx = ex + def uncheckedDecl(decl: TlaOperDecl): TlaOperDecl = decl + + //////////////////// + // HYBRID METHODS // + //////////////////// + + /** x' = y */ + def primeEq(x: TlaEx, y: TlaEx): TlaEx = eql(prime(x), y) + + import ParamUtil._ + + def param(name: String, tt: TlaType1): TypedParam = ParamUtil.param(name, tt) + + /** opName(params[1],...,params[n]) == body */ + def decl(opName: String, body: TlaEx, params: TypedParam*): TlaOperDecl = { + params.foreach(validateParamType) + TlaOperDecl(opName, params.map(_._1).toList, body)( + Typed( + OperT1(params.map { _._2 }, body.typeTag.asTlaType1()) + ) + ) + } + + /** + * Creates an expression of the form + * + * {{{ + * LET uniqueName(p1,...,pn) == body IN uniqueName + * }}} + * + * Matching the representation of LAMBDAs produced by SANY. + * + * NOTE: It is left up to the caller to ensure `uniqueName` is unique. + * + * Failure to ensure uniqueness of names can lead to name collisions in case lambdas are nested. + */ + def lambda(uniqueName: String, body: TlaEx, params: TypedParam*): TlaEx = { + params.foreach(validateParamType) + val paramTypes = params.map(_._2) + val operType = OperT1(paramTypes, body.typeTag.asTlaType1()) + letIn(name(uniqueName, operType), decl(uniqueName, body, params: _*)) + } + + /** {{{LET decl(...) = ... IN body}}} */ + def letIn(body: TlaEx, decl: TlaOperDecl): TlaEx = + LetInEx(body, decl)(body.typeTag) + + /** + * {{{LET F_1(a_1^1,...,a_{n_1}^1) == X_1 F_2(a_1^2,...,b_{n_2}^2) == X_2 ... F_N(a_1^N,...,z_{n_N}^N) == X_N IN e}}} + * is equivalently translated to + * {{{ + * LET F_1(a_1^1,...,a_{n_1}^1) == X_1 IN + * LET F_2(a_1^2,...,b_{n_2}^2) == X_2 IN + * ... + * LET F_N(a_1^N,...,z_{n_N}^N) == X_N IN + * e + * }}} + */ + def letIn(body: TlaEx, decls: TlaOperDecl*): TlaEx = { + require(decls.nonEmpty, "decls must be nonempty.") + decls.foldRight(body) { case (decl, partial) => + letIn(partial, decl) + } + } + + /** + * [f EXCEPT ![a1] = e1, ![a2] = e2 ... ![an] = en] + * + * Is equivalent to {{{[[f EXCEPT ![a1] = e1] EXCEPT ![a2] = e2] EXCEPT ... ![an] = en]}}} + */ + def exceptMany( + f: TlaEx, + args: (TlaEx, TlaEx)*): TlaEx = { + require(args.nonEmpty, s"args must be nonempty.") + args.foldLeft(f) { case (fn, (ai, ei)) => + except(fn, ai, ei) + } + } + + /** + * A name expression referring to the TlaVarDecl + */ + def varDeclAsNameEx(decl: TlaVarDecl): TlaEx = name(decl.name, decl.typeTag.asTlaType1()) +} diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopedBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopedBuilder.scala index 0a407d5319..6bfa4845cf 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopedBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopedBuilder.scala @@ -168,70 +168,9 @@ class ScopedBuilder(val strict: Boolean = true) /** x' = y */ def primeEq(x: TBuilderInstruction, y: TBuilderInstruction): TBuilderInstruction = eql(prime(x), y) - type TypedParam = (OperParam, TlaType1) + import ParamUtil._ - /** - * Evaluates whether a parameter type satisfies the type restrictions on operator parameters in TLA+. - * - * Parameters of TLA+ operators must: - * - have a non-operator type, unless they are (syntactically) marked higher-order (HO) - * - have a top-level operator type (OperT1) if they are marked HO - * - not contain `OperT1` in the type's syntax-tree in either case, except possibly at the root (if HO). In - * particular, a parameter to a HO operator with an `OperT1` type may not be HO itself. - */ - private def isAcceptableParamType(canContainOper: Boolean): TlaType1 => Boolean = { - case FunT1(arg, res) => isAcceptableParamType(false)(arg) && isAcceptableParamType(false)(res) - case SetT1(elem) => isAcceptableParamType(false)(elem) - case SeqT1(elem) => isAcceptableParamType(false)(elem) - case TupT1(elems @ _*) => elems.forall(isAcceptableParamType(false)) - case SparseTupT1(fieldTypes) => fieldTypes.values.forall(isAcceptableParamType(false)) - case RecT1(fieldTypes) => fieldTypes.values.forall(isAcceptableParamType(false)) - case OperT1(args, res) => - if (canContainOper) - args.nonEmpty && - args.forall(isAcceptableParamType(false)) && - isAcceptableParamType(false)(res) - else false - case RowT1(fieldTypes, _) => fieldTypes.values.forall(isAcceptableParamType(false)) - case RecRowT1(row) => isAcceptableParamType(false)(row) - case VariantT1(row) => isAcceptableParamType(false)(row) - case IntT1 | StrT1 | BoolT1 | RealT1 | VarT1(_) | ConstT1(_) => true - } - - /** - * Throws if parameters don't satisfy [[isAcceptableParamType]]. Permits operator types iff the parameter arity is - * positive. - */ - private def validateParamType(tp: TypedParam): Unit = { - val (OperParam(name, arity), tt) = tp - if (!isAcceptableParamType(canContainOper = arity > 0)(tt)) - throw new TBuilderTypeException( - s"Parameter $name type $tt and arity $arity are inconsistent. Parameters have operator types iff their arity is positive." - ) - } - - /** - * Determines the parameter arity, if the type is an operator type. We distinguish nullary operators from - * non-operators in this method. - */ - private def typeAsOperArity(tt: TlaType1): Option[Int] = tt match { - case OperT1(args, _) => Some(args.size) - case _ => None - } - - /** - * Operator parameter with type information. Checks that parameters have permissible types. - */ - def param(name: String, tt: TlaType1): TypedParam = { - val arityOpt = typeAsOperArity(tt) - // operator parameters may not be nullary operators - if (arityOpt.contains(0)) - throw new TBuilderTypeException(s"Parameter $name may not have a nullary operator type $tt.") - val arity = arityOpt.getOrElse(0) // 0 here means not-an-operator - val ret = (OperParam(name, arity), tt) - validateParamType(ret) - ret - } + def param(name: String, tt: TlaType1): TypedParam = ParamUtil.param(name, tt) /** opName(params[1],...,params[n]) == body */ def decl(opName: String, body: TBuilderInstruction, params: TypedParam*): TBuilderOperDeclInstruction = { diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/package.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/package.scala index 151101aa3a..ebe867a369 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/package.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/package.scala @@ -263,6 +263,11 @@ package object typecomp { def build: T = builderState } + // Included to facilitate seamless swapping between the scope-safe and unsafe builders + implicit class NoOpBuild(ex: TlaEx) { + def build: TlaEx = ex + } + /** * Apply the `build` method to a sequence. * diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/signatures/ApalacheOperSignatures.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/signatures/ApalacheOperSignatures.scala index 764794091f..e7a7a8b025 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/signatures/ApalacheOperSignatures.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/signatures/ApalacheOperSignatures.scala @@ -46,6 +46,12 @@ object ApalacheOperSignatures { // (Int, Int => t) => Seq(t) val mkSeqSig = signatureMapEntry(mkSeq, { case Seq(IntT1, OperT1(Seq(IntT1), t)) => SeqT1(t) }) + // ((t, Int) => t, Int, t) => t + val repeatSig = signatureMapEntry(repeat, + { + case Seq(OperT1(Seq(IntT1, t), t1), IntT1, t2) if compatible(t, t1) && compatible(t, t2) => t + }) + // ((a,b) => a, a, Set(b)) => a val foldSetSig = signatureMapEntry(foldSet, { @@ -72,6 +78,7 @@ object ApalacheOperSignatures { expandSig, constCardSig, mkSeqSig, + repeatSig, foldSetSig, foldSeqSig, setAsFunSig, diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ActionBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ActionBuilder.scala index 7201859d98..d9738e4e6f 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ActionBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ActionBuilder.scala @@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.typecomp.BuilderUtil.binaryFromUnsafe * Jure Kukovec */ trait ActionBuilder { - private val unsafeBuilder = new UnsafeActionBuilder + private val unsafeBuilder = new UnsafeActionBuilder {} /** {{{e'}}} */ def prime(e: TBuilderInstruction): TBuilderInstruction = e.map(unsafeBuilder.prime) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheBuilder.scala index b77bd92ece..3397a0a982 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheBuilder.scala @@ -15,7 +15,9 @@ import scalaz._ */ trait ApalacheBuilder { val strict: Boolean - private val unsafeBuilder = new UnsafeApalacheBuilder(strict) + // UnsafeApalacheBuilder is a trait with a parameter `strict`, so we create a class here to instantiate it + private case class ApalacheBuilderU(strict: Boolean) extends UnsafeApalacheBuilder + private val unsafeBuilder = ApalacheBuilderU(strict) /** * {{{lhs := rhs}}} @@ -36,6 +38,16 @@ trait ApalacheBuilder { */ def gen(n: BigInt, t: TlaType1): TBuilderInstruction = unsafeBuilder.gen(n, t).point[TBuilderInternalState] + /** + * {{{Repeat(F, N, x): t}}} + * @param n + * must be a nonnegative constant expression + * @param F + * must be an expression of the shape {{{LET Op(i) == ... IN Op}}} + */ + def repeat(F: TBuilderInstruction, n: BigInt, x: TBuilderInstruction): TBuilderInstruction = + binaryFromUnsafe(F, x)(unsafeBuilder.repeat(_, n, _)) + /** * {{{Skolem(ex)}}} * @param ex diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheInternalBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheInternalBuilder.scala index c8f96a10b9..78e6997869 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheInternalBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheInternalBuilder.scala @@ -15,7 +15,7 @@ import scalaz.Scalaz._ * Jure Kukovec */ trait ApalacheInternalBuilder { - private val unsafeBuilder = new UnsafeApalacheInternalBuilder + private val unsafeBuilder = new UnsafeApalacheInternalBuilder {} /** * {{{__NotSupportedByModelChecker(msg): t}}} diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ArithmeticBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ArithmeticBuilder.scala index 8b4d52a135..a10fcf9621 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ArithmeticBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ArithmeticBuilder.scala @@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.typecomp.BuilderUtil.binaryFromUnsafe * Jure Kukovec */ trait ArithmeticBuilder { - private val unsafeBuilder = new UnsafeArithmeticBuilder + private val unsafeBuilder = new UnsafeArithmeticBuilder {} /** {{{x + y}}} */ def plus(x: TBuilderInstruction, y: TBuilderInstruction): TBuilderInstruction = diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BaseBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BaseBuilder.scala index 3297271cb7..2f9b55d0cf 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BaseBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BaseBuilder.scala @@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeBaseBuilder * Jure Kukovec */ trait BaseBuilder { - private val unsafeBuilder = new UnsafeBaseBuilder + private val unsafeBuilder = new UnsafeBaseBuilder {} /** {{{lhs = rhs}}} */ def eql(lhs: TBuilderInstruction, rhs: TBuilderInstruction): TBuilderInstruction = diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BoolBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BoolBuilder.scala index e00c3c3b3a..7c55539a0d 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BoolBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BoolBuilder.scala @@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.typecomp.BuilderUtil._ * Jure Kukovec */ trait BoolBuilder { - private val unsafeBuilder = new UnsafeBoolBuilder + private val unsafeBuilder = new UnsafeBoolBuilder {} /** {{{args[0] /\ ... /\ args[n]}}} */ def and(args: TBuilderInstruction*): TBuilderInstruction = buildSeq(args).map(unsafeBuilder.and(_: _*)) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ControlBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ControlBuilder.scala index 0e156acac8..0fdbd539d8 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ControlBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ControlBuilder.scala @@ -12,7 +12,7 @@ import scalaz._ * Jure Kukovec */ trait ControlBuilder { - private val unsafeBuilder = new UnsafeControlBuilder + private val unsafeBuilder = new UnsafeControlBuilder {} /** {{{IF p THEN A ELSE B}}} */ def ite(p: TBuilderInstruction, A: TBuilderInstruction, B: TBuilderInstruction): TBuilderInstruction = diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FiniteSetBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FiniteSetBuilder.scala index eb3e9ecd3d..a975845573 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FiniteSetBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FiniteSetBuilder.scala @@ -10,7 +10,7 @@ import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeFiniteSetBuilder * Jure Kukovec */ trait FiniteSetBuilder { - private val unsafeBuilder = new UnsafeFiniteSetBuilder + private val unsafeBuilder = new UnsafeFiniteSetBuilder {} /** {{{IsFiniteSet(set)}}} */ def isFiniteSet(set: TBuilderInstruction): TBuilderInstruction = set.map(unsafeBuilder.isFiniteSet) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FunBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FunBuilder.scala index a4570d6c2f..846563253d 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FunBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FunBuilder.scala @@ -15,7 +15,7 @@ import at.forsyte.apalache.tla.lir.VarT1 * Jure Kukovec */ trait FunBuilder { - private val unsafeBuilder = new UnsafeFunBuilder + private val unsafeBuilder = new UnsafeFunBuilder {} /** * {{{[ args[0]._1 |-> args[0]._2, ..., args[n]._1 |-> args[n]._2 ]}}} diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala index a4204a890a..5fd4178efe 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala @@ -14,7 +14,7 @@ import scalaz._ * Jure Kukovec */ trait LiteralAndNameBuilder { - private val unsafeBuilder = new UnsafeLiteralAndNameBuilder + private val unsafeBuilder = new UnsafeLiteralAndNameBuilder {} /** {{{i : Int}}} */ def int(i: BigInt): TBuilderInstruction = unsafeBuilder.int(i).point[TBuilderInternalState] diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SeqBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SeqBuilder.scala index c3ec3d5eb4..4375f677ec 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SeqBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SeqBuilder.scala @@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeSeqBuilder * Jure Kukovec */ trait SeqBuilder { - private val unsafeBuilder = new UnsafeSeqBuilder + private val unsafeBuilder = new UnsafeSeqBuilder {} /** {{{Append(seq,elem)}}} */ def append(seq: TBuilderInstruction, elem: TBuilderInstruction): TBuilderInstruction = diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SetBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SetBuilder.scala index 293748f3ff..c1e9b6c3e1 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SetBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SetBuilder.scala @@ -14,7 +14,7 @@ import scalaz.Scalaz._ * Jure Kukovec */ trait SetBuilder { - private val unsafeBuilder = new UnsafeSetBuilder + private val unsafeBuilder = new UnsafeSetBuilder {} /** * {{{ diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/TemporalBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/TemporalBuilder.scala index 1d6de793ad..9be47382c7 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/TemporalBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/TemporalBuilder.scala @@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeTemporalBuilder * Jure Kukovec */ trait TemporalBuilder { - private val unsafeBuilder = new UnsafeTemporalBuilder + private val unsafeBuilder = new UnsafeTemporalBuilder {} /** {{{[]P}}} */ def box(P: TBuilderInstruction): TBuilderInstruction = P.map(unsafeBuilder.box) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/VariantBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/VariantBuilder.scala index 80914ec431..7295ace16c 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/VariantBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/VariantBuilder.scala @@ -12,7 +12,7 @@ import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeVariantBuilder * Jure Kukovec */ trait VariantBuilder { - private val unsafeBuilder = new UnsafeVariantBuilder + private val unsafeBuilder = new UnsafeVariantBuilder {} /** * {{{Variant(tagName, value): targetVariantType}}} diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeActionBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeActionBuilder.scala index 00fc856656..b968f16b1c 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeActionBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeActionBuilder.scala @@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir.oper.TlaActionOper * @author * Jure Kukovec */ -class UnsafeActionBuilder extends ProtoBuilder { +trait UnsafeActionBuilder extends ProtoBuilder { /** {{{e'}}} */ def prime(e: TlaEx): TlaEx = buildBySignatureLookup(TlaActionOper.prime, e) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheBuilder.scala index c42401d7e8..0808c85ea3 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheBuilder.scala @@ -10,11 +10,9 @@ import at.forsyte.apalache.tla.lir.values.TlaInt * @author * Jure Kukovec */ -class UnsafeApalacheBuilder(private val strict: Boolean = true) extends ProtoBuilder { - - // We borrow the LiteralBuilder to make TLA integers from Scala ints - private val intBuilder = new UnsafeLiteralAndNameBuilder - private def mkTlaInt: BigInt => TlaEx = intBuilder.int +trait UnsafeApalacheBuilder extends ProtoBuilder with UnsafeLiteralAndNameBuilder { + val strict: Boolean + // We extend LiteralBuilder to make TLA integers from Scala ints /** * {{{lhs := rhs}}} @@ -40,7 +38,20 @@ class UnsafeApalacheBuilder(private val strict: Boolean = true) extends ProtoBui */ def gen(n: BigInt, t: TlaType1): TlaEx = { if (strict) require(n > 0, s"Expected n to be positive, found $n.") - OperEx(ApalacheOper.gen, mkTlaInt(n))(Typed(t)) + OperEx(ApalacheOper.gen, int(n))(Typed(t)) + } + + /** + * {{{Repeat(F, N, x): t}}} + * @param n + * must be a nonnegative constant expression + * @param F + * must be an expression of the shape {{{LET Op(i) == ... IN Op}}} + */ + def repeat(F: TlaEx, n: BigInt, x: TlaEx): TlaEx = { + if (strict) require(n > 0, s"Expected n to be positive, found $n.") + if (strict) require(isNaryPassByName(n = 2)(F), s"Expected F to be a binary operator passed by name, found $F.") + buildBySignatureLookup(ApalacheOper.repeat, F, int(n), x) } /** @@ -103,7 +114,7 @@ class UnsafeApalacheBuilder(private val strict: Boolean = true) extends ProtoBui require(n >= 0, s"Expected n to be nonnegative, found $n.") require(isNaryPassByName(n = 1)(F), s"Expected F to be a unary operator passed by name, found $F.") } - buildBySignatureLookup(ApalacheOper.mkSeq, mkTlaInt(n), F) + buildBySignatureLookup(ApalacheOper.mkSeq, int(n), F) } /** diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheInternalBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheInternalBuilder.scala index 68fdcf22d7..6b12d9000c 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheInternalBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheInternalBuilder.scala @@ -9,11 +9,8 @@ import at.forsyte.apalache.tla.lir.oper.{ApalacheInternalOper, TlaOper} * @author * Jure Kukovec */ -class UnsafeApalacheInternalBuilder extends ProtoBuilder { - - // We borrow the LiteralBuilder to make TLA strings from Scala strings - private val strBuilder = new UnsafeLiteralAndNameBuilder - private def mkTlaStr: String => TlaEx = strBuilder.str +trait UnsafeApalacheInternalBuilder extends ProtoBuilder with UnsafeLiteralAndNameBuilder { + // We extend LiteralBuilder to make TLA strings from Scala strings /** * {{{__NotSupportedByModelChecker(msg): t}}} @@ -22,7 +19,7 @@ class UnsafeApalacheInternalBuilder extends ProtoBuilder { * argument. */ def notSupportedByModelChecker(msg: String, tt: TlaType1): TlaEx = - OperEx(ApalacheInternalOper.notSupportedByModelChecker, mkTlaStr(msg))(Typed(tt)) + OperEx(ApalacheInternalOper.notSupportedByModelChecker, str(msg))(Typed(tt)) /** * distinct diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeArithmeticBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeArithmeticBuilder.scala index 7a6e1dcdba..cd4fc08636 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeArithmeticBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeArithmeticBuilder.scala @@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir.oper.TlaArithOper * @author * Jure Kukovec */ -class UnsafeArithmeticBuilder extends ProtoBuilder { +trait UnsafeArithmeticBuilder extends ProtoBuilder { /** {{{x + y}}} */ def plus(x: TlaEx, y: TlaEx): TlaEx = buildBySignatureLookup(TlaArithOper.plus, x, y) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBaseBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBaseBuilder.scala index 24ed493673..8da8399d03 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBaseBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBaseBuilder.scala @@ -11,11 +11,8 @@ import at.forsyte.apalache.tla.types.{Substitution, TypeUnifier, TypeVarPool} * @author * Jure Kukovec */ -class UnsafeBaseBuilder extends ProtoBuilder { - - // We borrow the LiteralBuilder to make TLA strings from Scala strings - private val strBuilder = new UnsafeLiteralAndNameBuilder - private def mkTlaStr: String => TlaEx = strBuilder.str +trait UnsafeBaseBuilder extends ProtoBuilder with UnsafeLiteralAndNameBuilder { + // We extend the LiteralBuilder to make TLA strings from Scala strings /** {{{lhs = rhs}}} */ def eql(lhs: TlaEx, rhs: TlaEx): TlaEx = buildBySignatureLookup(TlaOper.eq, lhs, rhs) @@ -84,7 +81,7 @@ class UnsafeBaseBuilder extends ProtoBuilder { */ def label(ex: TlaEx, args: String*): TlaEx = { require(args.nonEmpty, s"args must be nonempty.") - val argsAsStringExs = args.map { mkTlaStr } + val argsAsStringExs = args.map { str } buildBySignatureLookup(TlaOper.label, ex +: argsAsStringExs: _*) } } diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBoolBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBoolBuilder.scala index 48dfcb446d..5ff07224d4 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBoolBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBoolBuilder.scala @@ -10,7 +10,7 @@ import at.forsyte.apalache.tla.typecomp.BuilderUtil * @author * Jure Kukovec */ -class UnsafeBoolBuilder extends ProtoBuilder { +trait UnsafeBoolBuilder extends ProtoBuilder { /** {{{args[0] /\ ... /\ args[n]}}} */ def and(args: TlaEx*): TlaEx = buildBySignatureLookup(TlaBoolOper.and, args: _*) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeControlBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeControlBuilder.scala index 6b016cced2..5d55941202 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeControlBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeControlBuilder.scala @@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir.oper.TlaControlOper * @author * Jure Kukovec */ -class UnsafeControlBuilder extends ProtoBuilder { +trait UnsafeControlBuilder extends ProtoBuilder { /** {{{IF p THEN A ELSE B}}} */ def ite(p: TlaEx, A: TlaEx, B: TlaEx): TlaEx = buildBySignatureLookup(TlaControlOper.ifThenElse, p, A, B) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFiniteSetBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFiniteSetBuilder.scala index 2e26ca8a59..6d7e258d18 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFiniteSetBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFiniteSetBuilder.scala @@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir.oper.TlaFiniteSetOper * @author * Jure Kukovec */ -class UnsafeFiniteSetBuilder extends ProtoBuilder { +trait UnsafeFiniteSetBuilder extends ProtoBuilder { /** {{{IsFiniteSet(set)}}} */ def isFiniteSet(set: TlaEx): TlaEx = buildBySignatureLookup(TlaFiniteSetOper.isFiniteSet, set) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFunBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFunBuilder.scala index f2b4bfa763..e596000136 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFunBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFunBuilder.scala @@ -16,11 +16,8 @@ import scala.collection.immutable.SortedMap * @author * Jure Kukovec */ -class UnsafeFunBuilder extends ProtoBuilder { - - // We borrow the LiteralBuilder to make TLA strings from Scala strings - private val strBuilder = new UnsafeLiteralAndNameBuilder - private def mkTlaStr: String => TlaEx = strBuilder.str +trait UnsafeFunBuilder extends ProtoBuilder with UnsafeLiteralAndNameBuilder { + // We extend the LiteralBuilder to make TLA strings from Scala strings private def formRecordFieldTypes(args: Seq[TlaEx]): SortedMap[String, TlaType1] = { require(TlaFunOper.rec.arity.cond(args.size), s"Expected record args to have even arity, found $args.") @@ -57,7 +54,7 @@ class UnsafeFunBuilder extends ProtoBuilder { def rowRec(rowVar: Option[VarT1], args: (String, TlaEx)*): TlaEx = { // _recMixed does all the require checks val flatArgs = args.flatMap { case (k, v) => - Seq(mkTlaStr(k), v) + Seq(str(k), v) } rowRecMixed(rowVar, flatArgs: _*) } @@ -82,7 +79,7 @@ class UnsafeFunBuilder extends ProtoBuilder { def rec(args: (String, TlaEx)*): TlaEx = { // _recMixed does all the require checks val flatArgs = args.flatMap { case (k, v) => - Seq(mkTlaStr(k), v) + Seq(str(k), v) } recMixed(flatArgs: _*) } diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeLiteralAndNameBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeLiteralAndNameBuilder.scala index 058d0dff38..cef4cedcad 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeLiteralAndNameBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeLiteralAndNameBuilder.scala @@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.types.ModelValueHandler * @author * Jure Kukovec */ -class UnsafeLiteralAndNameBuilder { +trait UnsafeLiteralAndNameBuilder { /** {{{i : Int}}} */ def int(i: BigInt): TlaEx = ValEx(TlaInt(i))(Typed(IntT1)) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSeqBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSeqBuilder.scala index 8dee27c310..55ccf2c1b0 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSeqBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSeqBuilder.scala @@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir.oper.TlaSeqOper * @author * Jure Kukovec */ -class UnsafeSeqBuilder extends ProtoBuilder { +trait UnsafeSeqBuilder extends ProtoBuilder { /** {{{Append(seq,elem)}}} */ def append(seq: TlaEx, elem: TlaEx): TlaEx = buildBySignatureLookup(TlaSeqOper.append, seq, elem) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSetBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSetBuilder.scala index 8c852397f1..f422985fdc 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSetBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSetBuilder.scala @@ -14,11 +14,8 @@ import scala.collection.immutable.SortedMap * @author * Jure Kukovec */ -class UnsafeSetBuilder extends ProtoBuilder { - - // We borrow the LiteralBuilder to make TLA strings from Scala strings - private val strBuilder = new UnsafeLiteralAndNameBuilder - private def mkTlaStr: String => TlaEx = strBuilder.str +trait UnsafeSetBuilder extends ProtoBuilder with UnsafeLiteralAndNameBuilder { + // We extend the LiteralBuilder to make TLA strings from Scala strings /** * {{{ @@ -109,7 +106,7 @@ class UnsafeSetBuilder extends ProtoBuilder { def recSet(kvs: (String, TlaEx)*): TlaEx = { // _recSetMixed does all the require checks val args = kvs.flatMap { case (k, v) => - Seq(mkTlaStr(k), v) + Seq(str(k), v) } recSetMixed(args: _*) } diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeTemporalBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeTemporalBuilder.scala index 38e1139f26..fb5aa72f73 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeTemporalBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeTemporalBuilder.scala @@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir.{NameEx, TlaEx} * @author * Jure Kukovec */ -class UnsafeTemporalBuilder extends ProtoBuilder { +trait UnsafeTemporalBuilder extends ProtoBuilder { /** {{{[]P}}} */ def box(P: TlaEx): TlaEx = buildBySignatureLookup(TlaTempOper.box, P) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeVariantBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeVariantBuilder.scala index 2d8d2a3a5e..a344cd8cc6 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeVariantBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeVariantBuilder.scala @@ -12,11 +12,8 @@ import at.forsyte.apalache.tla.typecomp.{BuilderUtil, PartialSignature} * @author * Jure Kukovec */ -class UnsafeVariantBuilder extends ProtoBuilder { - - // We borrow the LiteralBuilder to make TLA strings from name tags (Scala strings) - private val strBuilder = new UnsafeLiteralAndNameBuilder - private def mkTlaStr: String => TlaEx = strBuilder.str +trait UnsafeVariantBuilder extends ProtoBuilder with UnsafeLiteralAndNameBuilder { + // We extend the LiteralBuilder to make TLA strings from name tags (Scala strings) /** * {{{Variant(tagName, value): targetVariantType}}} @@ -35,7 +32,7 @@ class UnsafeVariantBuilder extends ProtoBuilder { } val sig = completePartial(VariantOper.variant.name, partialSig) - BuilderUtil.composeAndValidateTypes(VariantOper.variant, sig, mkTlaStr(tagName), value) + BuilderUtil.composeAndValidateTypes(VariantOper.variant, sig, str(tagName), value) } /** {{{VariantFilter(tagName, set)}}} */ @@ -46,7 +43,7 @@ class UnsafeVariantBuilder extends ProtoBuilder { } val sig = completePartial(VariantOper.variantFilter.name, partialSig) - BuilderUtil.composeAndValidateTypes(VariantOper.variantFilter, sig, mkTlaStr(tagName), set) + BuilderUtil.composeAndValidateTypes(VariantOper.variantFilter, sig, str(tagName), set) } /** {{{VariantTag(variant)}}} */ @@ -59,7 +56,7 @@ class UnsafeVariantBuilder extends ProtoBuilder { case Seq(StrT1, VariantT1(RowT1(fields, _)), a) if fields.get(tagName).contains(a) => a } val sig = completePartial(VariantOper.variantGetOrElse.name, partialSig) - BuilderUtil.composeAndValidateTypes(VariantOper.variantGetOrElse, sig, mkTlaStr(tagName), variant, defaultValue) + BuilderUtil.composeAndValidateTypes(VariantOper.variantGetOrElse, sig, str(tagName), variant, defaultValue) } /** {{{VariantGetUnsafe(tagName, variant)}}} */ @@ -69,6 +66,6 @@ class UnsafeVariantBuilder extends ProtoBuilder { case Seq(StrT1, VariantT1(RowT1(fields, _))) if fields.contains(tagName) => fields(tagName) } val sig = completePartial(VariantOper.variantGetUnsafe.name, partialSig) - BuilderUtil.composeAndValidateTypes(VariantOper.variantGetUnsafe, sig, mkTlaStr(tagName), variant) + BuilderUtil.composeAndValidateTypes(VariantOper.variantGetUnsafe, sig, str(tagName), variant) } } diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/types/package.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/types/package.scala index bbd898b721..d39d3a411e 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/types/package.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/types/package.scala @@ -1,5 +1,7 @@ package at.forsyte.apalache.tla +import at.forsyte.apalache.tla.lir.TlaEx + /** * Defines a premade instance of [[at.forsyte.apalache.tla.typecomp.ScopedBuilder ScopedBuilder]], named [[tla]]. * @@ -132,6 +134,9 @@ package object types { import at.forsyte.apalache.tla.typecomp._ + type BuilderT = TBuilderInstruction + type BuilderUT = TlaEx + /** * A short-hand to the instance of the typed builder, so one can easily construct expressions. * @@ -150,4 +155,5 @@ package object types { * [[at.forsyte.apalache.tla.typecomp.ScopedBuilder ScopedBuilder]] for implementation details. */ val tla: ScopedBuilder = new ScopedBuilder(strict = true) + val tlaU: ScopeUnsafeBuilder = new ScopeUnsafeBuilder(strict = true) } diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestApalacheBuilder.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestApalacheBuilder.scala index f8e4cf684a..c61d3035ea 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestApalacheBuilder.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestApalacheBuilder.scala @@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.typecomp import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper.ApalacheOper -import at.forsyte.apalache.tla.types.tla.TypedParam +import at.forsyte.apalache.tla.typecomp.ParamUtil.TypedParam import org.junit.runner.RunWith import org.scalatestplus.junit.JUnitRunner import scalaz.unused diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestHybrid.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestHybrid.scala index 0b6400fd95..809da08b76 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestHybrid.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestHybrid.scala @@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.typecomp import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper.{TlaActionOper, TlaBoolOper, TlaOper} -import at.forsyte.apalache.tla.types.tla.TypedParam +import at.forsyte.apalache.tla.typecomp.ParamUtil.TypedParam import org.junit.runner.RunWith import org.scalacheck.Prop.forAll import org.scalatestplus.junit.JUnitRunner diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestSetBuilder.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestSetBuilder.scala index 2fee63793c..6ebb57ec76 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestSetBuilder.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestSetBuilder.scala @@ -292,7 +292,7 @@ class TestSetBuilder extends BuilderTest { builder.name(s"x$i", ti), builder.name(s"S$i", InvalidTypeMethods.notSet), ) - } + }, ) } @@ -441,7 +441,7 @@ class TestSetBuilder extends BuilderTest { ts.zipWithIndex.map { case ((ti, _), i) => builder.name(s"x$i", ti) -> builder.name(s"S$i", InvalidTypeMethods.notSet) - } + }, ) }