Thomas Pani

Z3 `Global.getParameter()` throws `NoSuchFieldError`

1

Z3's `Global.getParameter()` throws `NoSuchFieldError` in: https://github.com/informalsystems/apalache/blob/b39ce05b2f8f51858d6ae5262fe5812a59e7ebaf/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala#L45-L46 Upstream issue: https://github.com/Z3Prover/z3/issues/6311

Use assumptions in incremental Z3SolverContext

11

We currently encode transitions in SMT like this: ```smt ;; ... prefix (push) ;; translate transition to SMT (push) (assert transition-trigger-var) (check-sat) ;; check enabledness (push) ;; encode -invariant (check-sat)...

Make deadlock detection optional

2

Given that deadlock detection makes an additional call (and it's is incomplete anyways), it seems to be a good idea to me to set `--no-deadlock=true` by default. _Originally posted by...

We should add a top-level handler for `Z3Exception`, to catch unexpected exceptions like the following: ``` State 7: Checking 1 state invariants I@07:19:23.982 State 7: Checking 2 state invariants I@07:20:32.515...

## Description `Z3SolverContext` expects a `.dispose()` call at the end of its lifetime. In offline mode (`--algo=offline`), we create multiple `Z3SolverContext` objects, one for each snapshot. All but the first...

_Spin-out from #878, which contained two reports in a single issue._ Apalache throws `A set filter over PowSet[FinSet[Int]] is not implemented` ```tla ------- MODULE Foo ------- EXTENDS Integers CONSTANT \*...

[FEATURE] Add TLA expression generator with well-typed output

1

The current `IrGenerators` produces TLA+ expressions with arbitrary type annotations. This produces errors in property-based testing such as #1364. Filtering the current (sometimes ill-typed) expressions through the typechecker is probably...

While addressing https://github.com/informalsystems/quint/issues/1196, I tried to write an Apalache config file, but struggled. The best documentation I found is [this manual section](https://apalache.informal.systems/docs/apalache/config.html#file-format-and-supported-parameters). It documents the principle format, but I had...

Temporal translation broken with nested temporal subformulas and quantifiers

6

Translation of temporal properties is broken, if the property contains nested temporal subformulas and quantifiers. Take the temporal property of the MWE below; ```tla TemporalProp == [](\A i \in DOMAIN...

cache action fails to unpack files in macOS CI

3

There's some issue with the cache action in `build` CI on macOS (not on Ubuntu). It fails to unpack the received cache contents: Example run: https://github.com/informalsystems/apalache/actions/runs/5290491810/jobs/9574713460 ``` 2023-06-15T08:49:11.1466950Z ##[group]Run john-shaffer/cache@59429c0461095f341a8cf7388e5d3aef37b95edd...