Skip to content

Commit

Permalink
Merge branch 'main' into update/sbt-scoverage-2.1.1
Browse files Browse the repository at this point in the history
  • Loading branch information
konnov authored Sep 2, 2024
2 parents 693607a + c69c355 commit d4bb391
Show file tree
Hide file tree
Showing 58 changed files with 224 additions and 120 deletions.
4 changes: 2 additions & 2 deletions .github/FUNDING.yml
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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']
1 change: 1 addition & 0 deletions .unreleased/bug-fixes/2962-fix-trunc-smt-log
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Fix truncation of SMT logs, see #2962
1 change: 1 addition & 0 deletions .unreleased/bug-fixes/2969-powset-expansion
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Better error reporting for hitting the limits of `SUBSET` expansion, see #2969
1 change: 1 addition & 0 deletions .unreleased/features/rewrite.md
Original file line number Diff line number Diff line change
@@ -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
4 changes: 2 additions & 2 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion CONTRIBUTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
9 changes: 8 additions & 1 deletion FUNDING.md
Original file line number Diff line number Diff line change
@@ -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
Expand Down
105 changes: 56 additions & 49 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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
Expand Down Expand Up @@ -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,
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Binary file added assets/reloading-apalache.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
2 changes: 1 addition & 1 deletion docs/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
4 changes: 2 additions & 2 deletions docs/src/adr/002adr-types.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion docs/src/adr/003adr-trex.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion docs/src/adr/004adr-annotations.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions docs/src/adr/005adr-json.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions docs/src/adr/011adr-smt-arrays.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions docs/src/adr/014adr-precise-records.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions docs/src/adr/015adr-trace.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion docs/src/adr/023adr-trace-evaluation.md
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
Loading

0 comments on commit d4bb391

Please sign in to comment.