modelator-py

modelator-py copied to clipboard

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.

danwt

_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)

danwt

[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....

danwt

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.

danwt

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.

danwt

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,...

danwt