Thomas Pani
Thomas Pani
## Description Running `apalache-mc simulate` on `MC_LamportMutexTyped.tla` results in an uncaught exception `internal error: SMT 0: Declaring cell 5, while cell 21799 has been already declared. Damaged arena?` on the...
`CounterexampleWriter` is used by `DumpFilesModelCheckerListener` to write all sorts of traces (not just counterexamples). It should be adapted for this purpose by appropriate renaming, adapting the Scaladoc, etc. Also, its...
Currently, the `search.simulation` parameters are wired in via tuning options: https://github.com/informalsystems/apalache/blob/59f3c1de4ab21b8865d040fc839cbb9e7b1c8eb4/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/SimulateCmd.scala#L16-L21 We should either refactor these into pass options, or rename "tuning options".
Unused fields in `ModelCheckerParams` that need cleanup: https://github.com/informalsystems/apalache/blob/9bde0363e2a0c98a5c97290c91d8f7e86f12369f/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/ModelCheckerParams.scala#L66-L87
`SeqModelChecker` receives two reference to the `CheckerInput` instance; once directly as its `checkerInput` constructor parameter and once via the `ModelCheckerParams.checkerInput` field. This can be confusing when referencing the `CheckerInput` instance...
There is some tech debt / open refactoring tasks that lead to unnecessary complexity around `SeqModelChecker`. My hope with this issue is to collect a (somewhat) exhaustive list of items...
We are currently parsing CLI arguments using [backuity/clist](https://github.com/backuity/clist). We recently had some problems with how the `version` command is handled, see #1497, #1505, and #1611: * We cannot access CLI...
The following LTL property spec results in a parsing exception in the LTL Automizer [web interface](https://monteverdi.informatik.uni-freiburg.de/tomcat/Website/?ui=int&tool=ltl_automizer), but works fine with the [binary version](https://monteverdi.informatik.uni-freiburg.de/tomcat/Website/?ui=tool&tool=ltl_automizer) `LTLAutomizer_Linux64_r13621.zip`. ```c //@ ltl invariant positive: (([]AP(env...
When running @nano-o's [spec](https://github.com/nano-o/Distributed-termination-detection/blob/5f4c0df03e0be5fa2483f652d309629d8f832ec8/Termination.tla) for 6 processes, I noticed considerable fluctuations (up to 4x slowdown) in Apalache runtime. Command: ``` apalache-mc check --run-dir=out --debug --init=Correctness_ --inv=Correctness --length=1 ~/src/Distributed-termination-detection/Termination.tla ``` Spec...
As requested in https://github.com/informalsystems/apalache/pull/2148#discussion_r966689680, we should perform validation on parameters passed as tuning options. Maybe requires some rethinking of tuning options in general, currently the just get parsed into a...