[Feature request] Add the option to specify a number of (counter)examples to generate

[ivan-gavran]

I would like to start a discussion on a feature that would enable specifying a number of (different) counterexamples to be generated for quint run and quint verify.

The motivation comes from the usage of Quint in testing: with a specified model, I am interested in generating a (large) number of traces satisfying a property (given as a negated invariant).
I believe the proposed feature could already be achieved for quint verify by passing the Apalache parameter --max-error. I don't see how to accomplish the same for quint run with current options.

A more general view of this feature request would be to make sampling a first-class citizen of Quint (whereas now it can be accomplished by repeatedly looking for a counterexample). This functionality was one of the features of (now not actively developed) Modelator. The question is whether such feature belongs to Quint, or rather to wrappers of Quint (such as Modelator).

[konnov]

It seems that you would like to have something similar to quint test --output=out{#}.itf.json and --max-error of apalache-mc. Is that right?

[ivan-gavran]

The way I understand it, quint test --output is producing multiple traces but for multiple tests, right? I would like to get multiple traces for a single property (but the format of quint test --output seems good for the purpose)

[konnov]

Looking at the code, I think you are right.

[konnov]

I would say that properly adding --output and --max-error to quint run requires about a week of work, marking it with w8.

[hvanz]

The run command has the parameter --max-samples but it doesn't seem to have any effect.

[konnov]

Yeah, --max-samples specifies how many runs the simulator is inspecting, not how many traces it would produce

[hvanz]

Would it be faster to generate N traces internally rather than calling quint run N times? I mean, the simulator would perform some kind of backtracking, or each trace would be generated independently of each other? If it's the second case, probably it's more cost effective just to call quint run N times in a script.

[konnov]

Technically, it would be faster to generate tests in a loop inside quint run, since quint run compiles a spec to a bunch of JavaScript objects. So it would probably benefit from JIT. However, have you tried to run quint run in a loop? Maybe it just works for you.

[hvanz]

have you tried to run quint run in a loop?

Yeah, that's what I end up doing. I'm just experimenting so I couldn't say yet if the performance is good enough.

[p-offtermatt]

I would also be interested in this feature. Specifically, running Quint in a loop makes it hard to force it to generate different traces, which is something I would be interested in.

Different for me would mean any difference in states, i.e. I wouldn't necessarily be interested in two different traces that resolve nondeterminism differently if this does not have any visible effect on the state.

How hard would such a "different" requirement be to implement? I imagine it shouldn't add too much complexity but might be missing some subtlety?

[konnov]

You know the --view option of Apalache. Now imagine you would have the same option in quint run. Would that help you?

[p-offtermatt]

Oh, yeah, thanks for recalling that - it's exactly what I'd be interested in!