Daniel T

Feature: ensure correct JDK used when running Apalache

1

Apalache should be run using the right JDK in order to get it to work on `arm64`.

Approximate [location](https://github.com/informalsystems/modelator-py/blob/d989ea4533020aef9ff852dbadf3af2884d9d2d3/modelator/tlc/raw.py#L19-L70), for commit d989ea4, of relevant code to be changed. Relevant [TLC issue](https://github.com/tlaplus/tlaplus/issues/640#issuecomment-1042484320) about new format dump feature.

_Issue created at [d989ea4](https://github.com/informalsystems/modelator-py/commit/d989ea4533020aef9ff852dbadf3af2884d9d2d3)_ Suggested location of code that would have to be updated to implement for TLC: [here](https://github.com/informalsystems/modelator-py/blob/d989ea4533020aef9ff852dbadf3af2884d9d2d3/modelator/tlc/raw.py#L19-L70)

[Context](https://github.com/informalsystems/mbt/pull/95) There is an extremely basic unoptimized version here https://github.com/informalsystems/modelator-py/blob/bc71f46f0e0cfe85843c63d46c590fce51cbd0fb/modelator/scratch_subset_selection.py , which could be replaced by a more optimized version using some efficient array encoding, by for example using numpy....

Feature: quickly get JSON format for a spec

1

Given a TLA+ spec there should be a quick way to learn the structure/format of the JSON that traces of the spec will be given in.

The tool currently writes output in json to stdout but various internal procedures should be designed so that they can be queried for their progress.

Users would like to generate multiple traces violating a single invariant using TLC. It is possible to do this using TLC's '-continue' parameter. It just allows model checking to continue,...

Sometimes fails randomly https://github.com/dymensionxyz/dymint/blob/70d946045d94bac9cff5e31d68e3dae14c1f82c1/p2p/client_test.go#L45-L63

comparison: fraud proof changes

1

I made the PR simply to see the diff # PR Standards ## Opening a pull request should be able to meet the following requirements --- For Author: - [...

feat(fraud-proofs)

1

# PR Standards ## Opening a pull request should be able to meet the following requirements --- Close #XXX For Author: - [ ] Targeted PR against correct branch -...