Kukovec

Make it possible to evaluate expressions over (ITF) traces

6

Often, it is difficult for humans to _evaluate_ or _inspect_ a counterexample and mine it for information. This is mainly due to the fact that invariants, for which counterexamples are...

Relax compiler warnings for imports used in scaladoc

5

If a scaladoc references e.g. `[[object]]` while using a top-level `import a.b.c.object`, instead of `[[a.b.c.object]]`, this triggers a compiler warning ("unused import") if `object` is not used in the code....

- [x] Tests added for any new code - [x] Ran `make fmt-fix` (or had formatting run automatically on all files edited) - [ ] ~Documentation added for any new...

File references in the manual get silently invalidated by file changes

4

Often, manual sections will link to hard-coded segments in source `.tla` files. For example, https://github.com/informalsystems/apalache/blob/a7b670cb700683554e933aef81a189a9843ae059/docs/src/apalache/principles/recursive.md?plain=1#L15-L19 used to point to the definitions of `FoldSeq` and `FoldSet`, but as `Apalache.tla` has changed...

`ExprOptimizer` optimizes `r \in { [f_1 |-> x_1, ..., f_k |-> x_k]: x_1 \in S_1, ..., x_k \in S_k }` into `DOMAIN r = { "f_1", ..., "f_k" } /\...

`BuilderTest` offers testing templates, which accept a sequence constructor for a sequence of ill-typed expressions (`mkIllTyped`), then check that attempting to build any of them causes a `TBuilderTypeException`. The templates...

See discussion in #1916.

Where available, the JSON encoding should include information about all of the known annotations (not just types).

[BUG] Skolem operator wrapping a non-existential triggers unrelated exceptions

1

## Input specification ``` ---------- MODULE test ---------- EXTENDS Apalache Init == TRUE Next == TRUE Inv == Skolem(TRUE) ==================== ``` ## The command line parameters used to run the...

## Input specification ``` ---------- MODULE test ---------- EXTENDS Apalache Init == TRUE Next == TRUE Inv == Expand({}) = {} ==================== ``` ## The command line parameters used to...