Automatic generation of test cases for counterexample traces

[p-offtermatt]

It would be very useful to have an option to automatically convert a counterexample trace into a test inside your module.

A suggestion for the workflow could be like this: You run quint run .... file.qnt and get a counterexample. You then run something like quint generate-test, which automatically generates a test according to the run that just found a violation and puts it into file.qnt

Why is this useful? I would see this being used as a way to help debug problems. You very easily get a test case that you can run, but an advantage over just rerunning with the same seed is that you can play with the test case, e.g. change input parameters or actions and check whether the invariant violation still happens.

Is this even feasible? I think a problem is probably how/where to resolve nondeterminism. If no nondeterminism is resolve, a valid counterexample trace would always just be something like init.then(step).then(step).then(step).....then(assert(invariant_that_fails)) Of course, in reality step probably looks like

any {
nondet param = oneOf(..)
nondet param2 = oneOf(..)
action1(param, param2)

nondet param = oneOf(..)
action2(param)
}

Then, optimally the test case generator would be smart enough to figure out that the trace can be made deterministic by not simply calling step over and over, but by calling the actions with the parameters that were chosen in the counterexample.

I think a tricky part would be choosing which level of nondeterminism resolution is appropriate, e.g. somewhere deep in some call, something might be nondeterministic, and resolving that could lead to extremely long tests calling tons of functions. Then one might prefer leaving this deep nondeterminism, and having that resolve via the seed. I think one could have a parameter governing how deep to resolve nondeterminism, or the crazier solution: try many ways and query an LLM to ask which way it thinks is most appropriate :)