Add the option to specify a number of (counter)examples to generate

[shonfeder]

Discussed in #1138

^{Originally posted by ivan-gavran September 1, 2023}
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).

[shonfeder]

@ivan-gavran mentioned this would save time and help with audits. It is possible to do this with just scripting, but this is an obviously valuable feature for MBT.

As an extension of this, we should include a feature to generate N traces that produce a property, so take care of negating invariants.

This is not currently blocking any work as far as we know but would be a clear benefit.

As @p-offtermatt pointed out, one of the principle challenges with a user script is being able to identify duplicate traces.

As a separate, related concern, we should determine how easy it is to get this from apalache.

[josef-widder]

It would definitely be useful to have this feature for MBT and audits. Actually I was surprised that it is not possible at the moment. I thought that because the help of quint run tells me

  --max-samples  the maximum on the number of traces to try
                                                       [number] [default: 10000]

there should be a way for me to access these 10000 traces. I really think it is important working on this feature.

[ivan-gavran]

--max-samples the maximum on the number of traces to try [number] [default: 10000]

there should be a way for me to access these 10000 traces. I really think it is important working on this feature.

Nitpicking, but have to in order to be on the safe side: just accessing those 10000 traces would not suffice: if a property is defined, the run stops immediately once a trace that satisfies the property is found (thus, all prior traces are not the ones we're interested in).
With no property defined, I believe it suffices to access the 10000 traces (and this too would be a valuable feature).