This PR closes issue #490. The paths defined in the environment variable `TLA_PATH` are joined with the paths defined in the Java system variable `TLA-Library`. The latter is having priority...
This is probably a rare use case. It has a simple workaround. I am submitting this issue, as it probably could be fixed at the code level. If we run...
We are now using `OpDefOrDeclNode.getComment` to parse annotations in TLA+ declarations, see [this PR](https://github.com/informalsystems/apalache/pull/503). While it works well, we have noticed a few inconsistencies in the placement of comments. For...
This is a meta-issue on implementing a new SMT encoding that efficiently uses arrays. All issues in this feature are labeled with FARR.
As we have found in #1725, the mode specified with `search.invariant.mode` dramatically changes the running times, depending on whether we are checking an inductive invariant or running bounded model checking....
Closes #1756. This is a work-in-progress specification of the basic model checking mode. While this specification may be checked with Apalache, it is not entirely faithful in representing the interaction...
In this tutorial, we reproduce a known scenario of ERC20 tokens with property-based testing, Apalache, and TLC under five configurations. - Stateful testing with Hypothesis. This is pretty much random...
Since we have introduced the idiom for uninterpreted types/model values in [the manual](https://apalache.informal.systems/docs/HOWTOs/uninterpretedTypes.html), the syntax for uninterpreted values should become more visible. Currently, it is implemented in https://github.com/informalsystems/apalache/blob/unstable/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/ModelValueHandler.scala. With #1977,...
Following #1946, a type annotation disappears in this MWE: ```tla ---- MODULE A ---- EXTENDS Naturals, FiniteSets, Apalache \* @type: (Set(a), Set(b)) => Set(a -> b); FSets(D, R) == LET...
Following the bug report in #1946, type annotations in multiple-line LET-IN definitions do not work: ```tla ---- MODULE Apalache_M0 ---- EXTENDS Naturals, FiniteSets \* @type: (Set(a), Set(b)) => Set(a ->...