Meta-issue: support for incremental bug finding

[konnov]

TLC has the flag --continue, which tells TLC to continue state space exploration after a bug has been found. This mode can be used to produce multiple tests that violate an invariant. See TLC command line options.

We should add a similar feature in Apalache, to be able to produce tests.

This is very important for model-based testing. For MBT we need some way to exhaustively enumerate all counterexamples according to some strategy. There could be different strategies that very in terms of implementation complexity or the number of produced counterexamples, e.g.:

• according to the sequence of transitions taken, ignoring the variable values
• according to the rough partitioning of the state space for certain variables, and requiring the counterexample state to touch another state space region.

Implementing at least the first strategy should be relatively easy, and it's absolutely crucial for MBT to have the ability to enumerate all possible test scenarios for a particular test.

The following features are needed for MBT (in some order):

• [ ] Implementing a JSON server to handle model checking queries #730
• [ ] Enumerating sequences of different symbolic transitions #542
• [ ] Enumerating different SMT models

[konnov]

Another interesting scenario by Markus is to enumerate all parameter values that lead to a counterexample (set with --cinit=...).

[konnov]

moving to the next milestone

[konnov]

There seem to be many interesting scenarios. We keep this issue as a meta-issue. The concrete strategies should refer it.

[konnov]

This has been solved via --max-error and --view