In `run` command, option `--n-traces` has no effect unless argument to `--out-itf` ends with `.itf.json`

[romac]

If I run Quint on a spec with

$ quint run (...) --n-traces 10 --out-itf traces.json

I would expect to see 10 traces being generated, but only a single one is output to traces.json, thus silently disabling the behavior of --n-traces.

I apparently have to specify a .itf.json suffix for --n-traces to have any effect, which is counterintuitive to me.

My suggestion is to let users choose any filename + extension, and specify the trace number to use in the output using the {#} placeholder (much like for the test command) instead of having Quint automatically append the trace number to files ending with .itf.json.

$ quint run (...) --n-traces 3 --out-itf trace_{#}.json

The command above would produce traces_0.json, traces_1.json, traces_2.json.

[romac]

Note that the test command has its own counterintuitive behavior, where it accepts placeholders but those only take effect when the filename ends with .itf.json, see #1137.

I would suggest we remove the restriction on the extension in the test command as well. What do you think @bugarela?

[romac]

I have opened a PR for both issues, but I am happy to discuss alternative solutions.