Merge branch 'main' into update/sbt-scoverage-2.1.1

.github/FUNDING.yml

@@ -1,6 +1,6 @@
 # These are supported funding model platforms
 
-github: # Replace with up to 4 GitHub Sponsors-enabled usernames e.g., [user1, user2]
+github: [konnov] # Replace with up to 4 GitHub Sponsors-enabled usernames e.g., [user1, user2]
 patreon: # Replace with a single Patreon username
 open_collective: # Replace with a single Open Collective username
 ko_fi: # Replace with a single Ko-fi username
@@ -9,4 +9,4 @@ community_bridge: # Replace with a single Community Bridge project-name e.g., cl
 liberapay: # Replace with a single Liberapay username
 issuehunt: # Replace with a single IssueHunt username
 otechie: # Replace with a single Otechie username
-custom: ['https://informal.systems/', 'https://viennabusinessagency.at/'] # Replace with up to 4 custom sponsorship URLs e.g., ['link1', 'link2']
+custom: # Replace with up to 4 custom sponsorship URLs e.g., ['link1', 'link2']

.unreleased/bug-fixes/2962-fix-trunc-smt-log

@@ -0,0 +1 @@
+Fix truncation of SMT logs, see #2962

.unreleased/bug-fixes/2969-powset-expansion

@@ -0,0 +1 @@
+Better error reporting for hitting the limits of `SUBSET` expansion, see #2969

.unreleased/features/rewrite.md

@@ -0,0 +1 @@
+Handle expressions such as  S \in SUBSET T  in ExprOptimizer by rewriting the expression into  \A r \in S: r \in T

CHANGES.md

@@ -317,7 +317,7 @@
 ### Breaking changes
 
 - Invalid configuration keys found in configuration sources (e.g., `apalache.cfg` files) will now produce a configuration error on load (see #2125).
-- The structure of the apalache.cfg has changed. All configuration keys that were previously supported have been moved under the `common` key. You can update your config files by prefixing each key from the previous versions with `commong.key-name`. For an example config file, see https://apalache.informal.systems/docs/apalache/config.html#file-format-and-supported-parameters. See #2065.
+- The structure of the apalache.cfg has changed. All configuration keys that were previously supported have been moved under the `common` key. You can update your config files by prefixing each key from the previous versions with `commong.key-name`. For an example config file, see https://apalache-mc.org/docs/apalache/config.html#file-format-and-supported-parameters. See #2065.
 - Introduce --features=no-rows for the old record syntax and switch to `--features=rows` by default
 
 ### Features
@@ -737,7 +737,7 @@
 ### Documentation
 
  * Restructure and update the Apalache manual:
-   https://apalache.informal.systems/docs/index.html
+   https://apalache-mc.org/docs/index.html
 
 ## 0.17.5
 

CONTRIBUTING.md

@@ -149,7 +149,7 @@ contributors and maintainers to make sure:
 ## Dependencies
 
 For setting up the local build, see the [instructions on building from
-source](https://apalache.informal.systems/docs/apalache/installation/source.html).
+source](https://apalache-mc.org/docs/apalache/installation/source.html).
 
 ### Environment
 

FUNDING.md

@@ -1,7 +1,14 @@
 ## Apalache Funding
 
+Currently, Apalache is not funded by any organization. As a result,
+it is de-facto funded by its current maintainers and contributors,
+including [Igor Konnov][], [Jure Kukovec][], and [Thomas Pani][].
+If you would like to sponsor the project, please contact us, or
+simply sponsor us on GitHub by clicking the "Sponsor" button!
+
 We are grateful to the following organizations for financially supporting
-the project Apalache for significant duration of time in the past:
+the Apalache project (in the form of grants or employment) for a significant
+duration of time in the past:
 
 - [Informal Systems][]: 2020-2024
 - [Vienna Business Agency][]: 2021-2023

README.md

@@ -12,16 +12,19 @@ alt="Apalache Logo">
 [![main badge][]][main-ci]
 
 [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
+Apalache translates [TLA+][] into the logic supported by SMT solvers such as
+[Microsoft Z3][]. Apalache can check inductive invariants (for fixed or bounded
 parameters) and check safety of bounded executions (bounded model checking). To
-see the list of supported TLA+ constructs, check the [supported features]. In
-general, Apalache runs under the same assumptions as [TLC].
+see the list of supported TLA+ constructs, check the [supported features][]. In
+general, Apalache runs under the same assumptions as [TLC][]. However, Apalache
+benefits from constraint solving and can handle potentially larger state-spaces,
+e.g., involving integer clocks and Byzantine faults.
 
-To learn more about TLA+, visit [Leslie Lamport's page on TLA+] and his [Video
-course].
+To learn more about TLA+, visit [Leslie Lamport's page on TLA+][] and his [Video
+course][].
 
 ## Releases
 
@@ -39,54 +42,57 @@ You can also find Apalache packaged via Nix at [cosmos.nix](https://github.com/i
 For more information on installation options, see [the
 manual][user-manual-installation].
 
+## Success stories
+
+Check [Apalache examples][] that demonstrate how to use the strengths of Apalache.
+Also, check the [standard repository of TLA+ examples][].
+
 ## Getting started
 
 - Read the [Beginner's tutorial][].
-- Check the material at [TLA-Apalache workshop][].
 - Read the [Apalache user manual][user-manual].
 - Consult the (WIP) [Idioms for writing better TLA+][idioms].
 - Consult the (WIP) [TLA+ language manual for engineers][language-manual].
 
-## Website
+## Community
 
-Our current website is served at https://apalache-mc.org .
+- Join the chat in the [Apalache zulip stream].
+- [Contribute](./CONTRIBUTING.md) to the development of Apalache.
 
-The site is hosted by github, and changes can be made through PRs into the
-[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.
+## Funding and Sponsorship
 
-The user documentation is automatically deployed to the website branch as per
-the [CI configuration](./.github/workflows/deploy.yml).
+Currently, Apalache is not funded by any organization. As a result,
+it is de-facto funded by its current maintainers and contributors,
+including [Igor Konnov][], [Jure Kukovec][], and [Thomas Pani][].
+If you would like to sponsor the project, please contact us, or
+simply sponsor us on GitHub by clicking the "Sponsor" button!
 
-Our old website is still available at https://forsyte.at/research/apalache/ .
+![Reloading Apalache](./assets/reloading-apalache.png)
 
-## Community
+We are grateful for the past financial support in the form of grants or
+employment from the following organizations:
 
-- Join the chat in the [Apalache zulip stream].
-- [Contribute](./CONTRIBUTING.md) to the development of Apalache.
-
-## Help wanted
+ - [Informal Systems][] (Canada/Switzerland/Austria): 2020-2024
+ - [Vienna Business Agency][] (Austria): 2021-2023
+ - [Interchain Foundation][] (Switzerland): 2019-2023
+ - [WWTF][] (Austria): Vienna Science and Technology Fund 2016-2020
+ - [Inria Nancy][] and [LORIA][] (France): 2018-2019
+ - [TU Wien][] (Austria): 2016-2020
 
-Want to contribute? Here is a list of issues that could be solved without
-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.
+More details on the [Funding page](./FUNDING.md).
 
-- 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/apalache-mc/apalache/issues/844)
-- Interval analysis for `a..b`: [#446](https://github.com/apalache-mc/apalache/issues/446)
+## Website
 
-## Industrial examples
+Our current website is served at https://apalache-mc.org .
 
-- Check [Light client specs][] and [Model-based testing][] of the Tendermint
-  light client.
+The site is hosted by github, and changes can be made through PRs into the
+[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.
 
-- Check [Tendermint specs][] to see how we use TLA+ and Apalache at Informal to
-  design and specify protocols for the [Tendermint blockchain].
+The user documentation is automatically deployed to the website branch as per
+the [CI configuration](./.github/workflows/deploy.yml).
 
-- To see more examples, check the [standard repository of TLA+ examples].
+<!-- TODO:this section should go to the website
 
 ## Talks
 
@@ -115,14 +121,9 @@ solve it.
 
 - [Bounded model checking of TLA+ specifications with SMT](https://www.youtube.com/watch?v=Xl1--arESl8)
   TLA+ Community Event 2018 (July 2018).
+-->
 
-## Performance
-
-We are collecting [apalache benchmarks]. See the Apalache performance when
-[checking inductive invariants] and running [bounded model checking]. Versions
-0.6.0 and 0.7.2 are a major improvement over version 0.5.2 (the version
-[reported at OOPSLA19](https://dl.acm.org/doi/10.1145/3360549)).
-
+<!-- TODO: This section should also go to the website
 ## Academic papers
 
 To read an academic paper about the theory behind Apalache,
@@ -131,15 +132,10 @@ For the details of our novel encoding using SMT arrays, check our
 [paper at TACAS23](https://link.springer.com/chapter/10.1007/978-3-031-30823-9_7).
 Related reports and publications can be found at the
 [Apalache page at TU Wien](http://forsyte.at/research/apalache/).
+-->
 
 ---
 
-Apalache is developed at [Informal Systems](https://informal.systems/).
-
-With additional funding from<br />[<img alt="the Vienna Business Agency" src="./Wirtschaftsagentur_Wien_logo.jpg" width="200">](https://viennabusinessagency.at/).
-
-Past funding from [Der Wiener Wissenschafts-, Forschungs- und Technologiefonds](https://wwtf.at/about/).
-
 [tla+]: http://lamport.azurewebsites.net/tla/tla.html
 [microsoft z3]: https://github.com/Z3Prover/z3
 [supported features]: https://apalache-mc.org/docs/apalache/features.html
@@ -156,7 +152,7 @@ Past funding from [Der Wiener Wissenschafts-, Forschungs- und Technologiefonds](
 [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/apalache/docs/index.html
+[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
@@ -166,3 +162,14 @@ Past funding from [Der Wiener Wissenschafts-, Forschungs- und Technologiefonds](
 [apalache-mc.org]: https://apalache-mc.org
 [TLA-Apalache workshop]: https://github.com/informalsystems/tla-apalache-workshop
 [Beginner's tutorial]: https://apalache-mc.org/docs/tutorials/entry-tutorial.html
+[Apalache examples]: https://github.com/konnov/apalache-examples
+[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/
+[Igor Konnov]: https://github.com/konnov
+[Jure Kukovec]: https://github.com/kukovec
+[Thomas Pani]: https://github.com/thpani

docs/README.md

@@ -3,7 +3,7 @@
 The Apalache documentation is written in markdown files in the [./src](./src)
 directory and compiled using [mdbook](https://github.com/rust-lang/mdBook).
 
-To view the documentation, visit https://apalache.informal.systems/docs/.
+To view the documentation, visit https://apalache-mc.org/docs/.
 
 ## Building and previewing the documentation
 

docs/src/adr/002adr-types.md

@@ -598,8 +598,8 @@ AtMostOne ==
 =============================================================================
 ```
 
-[Snowcat tutorial]: https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html
-[Snowcat HOWTO]: https://apalache.informal.systems/docs/HOWTOs/howto-write-type-annotations.html
+[Snowcat tutorial]: https://apalache-mc.org/docs/tutorials/snowcat-tutorial.html
+[Snowcat HOWTO]: https://apalache-mc.org/docs/HOWTOs/howto-write-type-annotations.html
 [ADR014]: https://github.com/informalsystems/apalache/blob/main/docs/src/adr/014adr-precise-records.md
 [Issue 401]: https://github.com/informalsystems/apalache/issues/401
 [Row polymorphism]: https://en.wikipedia.org/wiki/Row_polymorphism

docs/src/adr/003adr-trex.md

@@ -116,4 +116,4 @@ explain how the parallel checker is working. This is a subject to another ADR.
 To sum up, this layer is offering you a nice abstraction to write different
 model checking strategies.
 
-[KerA+]: https://apalache.informal.systems/docs/apalache/kera.html
+[KerA+]: https://apalache-mc.org/docs/apalache/kera.html

docs/src/adr/004adr-annotations.md

@@ -158,7 +158,7 @@ This is done because the SANY parser is pruning the linefeed character `\n`,
 so it would be otherwise impossible to find the end of an annotation.
 
 
-[ADR-002]: https://apalache.informal.systems/docs/adr/002adr-types.html
+[ADR-002]: https://apalache-mc.org/docs/adr/002adr-types.html
 [JavaTokenParsers]: https://www.scala-lang.org/api/2.12.2/scala-parser-combinators/scala/util/parsing/combinator/JavaTokenParsers.html
 
 [Java identifier]: https://docs.oracle.com/javase/specs/jls/se7/html/jls-3.html#jls-3.8

docs/src/adr/005adr-json.md

@@ -201,9 +201,9 @@ In general, for any given `oper: TlaOper` of `OperEx`, the value of the `oper` f
 The implementation of the serialization can be found in the class
 `at.forsyte.apalache.io.json.TlaToJson` of the module `tla-import`, see [TlaToJson][].
 
-[ADR-002]: https://apalache.informal.systems/docs/adr/002adr-types.html
+[ADR-002]: https://apalache-mc.org/docs/adr/002adr-types.html
 
-[ADR-004]: https://apalache.informal.systems/docs/adr/004adr-annotations.html
+[ADR-004]: https://apalache-mc.org/docs/adr/004adr-annotations.html
 
 [TlaToJson]: https://github.com/informalsystems/apalache/blob/main/tla-io/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala#L54
 [TlaEx]: https://github.com/informalsystems/apalache/blob/main/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaEx.scala#L10

docs/src/adr/011adr-smt-arrays.md

@@ -308,14 +308,14 @@ The following changes will be made to implement the new encoding of functions:
 The use of SMT arrays will be restricted to TLA+ sets and functions for the moment. The encoding of
 additional features using SMT arrays, or potentially ADTs, will be left for the future.
 
-[KerA+]: https://apalache.informal.systems/docs/apalache/kera.html
+[KerA+]: https://apalache-mc.org/docs/apalache/kera.html
 [core theory]: http://smtlib.cs.uiowa.edu/theories-Core.shtml
 [arrays with extensionality]: http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml
 [Z3]: https://github.com/Z3Prover/z3
 [SMT-LIB Standard]: http://smtlib.cs.uiowa.edu/index.shtml
 [Version 2.6]: https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
 [TLA+ Model Checking Made Symbolic]: https://dl.acm.org/doi/10.1145/3360549
 [Symbolic Model Checking for TLA+ Made Faster]: https://doi.org/10.1007/978-3-031-30823-9_7
-[model checking parameters]: https://apalache.informal.systems/docs/apalache/running.html#model-checker-command-line-parameters
+[model checking parameters]: https://apalache-mc.org/docs/apalache/running.html#model-checker-command-line-parameters
 [represented internally in Z3]: https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-arrays
 [PR 2027]: https://github.com/informalsystems/apalache/pull/2027

docs/src/adr/014adr-precise-records.md

@@ -15,7 +15,7 @@
 ## 1. Summary
 
 This ADR extends
-[ADR-002](https://apalache.informal.systems/docs/adr/002adr-types.html) on
+[ADR-002](https://apalache-mc.org/docs/adr/002adr-types.html) on
 types and type annotations.
 
 Virtually every user of Snowcat has faced the issue of record type checking
@@ -665,7 +665,7 @@ default untyped implementation for the operators.
 
 
 
-[ADR002]: https://apalache.informal.systems/docs/adr/002adr-types.html
+[ADR002]: https://apalache-mc.org/docs/adr/002adr-types.html
 [#401]: https://github.com/informalsystems/apalache/issues/401
 [#789]: https://github.com/informalsystems/apalache/discussions/789
 [Raft]: https://github.com/ongardie/raft.tla/blob/master/raft.tla

docs/src/adr/015adr-trace.md

@@ -467,8 +467,8 @@ write a parser of custom ITF traces. Hence, we have decided to keep only the obj
 as the more general of the two representations. 
 
 
-[ADR005]: https://apalache.informal.systems/docs/adr/005adr-json.html
-[ADR002]: https://apalache.informal.systems/docs/adr/002adr-types.html
+[ADR005]: https://apalache-mc.org/docs/adr/005adr-json.html
+[ADR002]: https://apalache-mc.org/docs/adr/002adr-types.html
 [MissionariesAndCannibalsTyped]: https://github.com/informalsystems/apalache/blob/main/test/tla/MissionariesAndCannibalsTyped.tla
 [JSON]: https://en.wikipedia.org/wiki/JSON
 [RFC7159]: https://datatracker.ietf.org/doc/html/rfc7159.html

docs/src/adr/023adr-trace-evaluation.md

@@ -137,7 +137,7 @@ and trace `testTrace.json` (length 5, `x=1 -> ... -> x=5`).
 {
   "name": "ApalacheIR",
   "version": "1.0",
-  "description": "https://apalache.informal.systems/docs/adr/005adr-json.html",
+  "description": "https://apalache-mc.org/docs/adr/005adr-json.html",
   "modules": [
     {
       "kind": "TlaModule",