tla2tools.jar output error trace

[zhi niu]

Hello, I am integrating tla2tools.jar for formal verification, but during the command line stage, I want to output all error traces in json format.

But when I use the -dumpTrace command, the trace json file can be output normally.

java -jar tla2tools.jar -config DieHard.cfg DieHard.tla -dumpTrace json ./test/test.json (trace output right)

However, once I add the -continue option to the command line, I find that the -dumpTrace option is invalid. not output trace file. What is the reason? Or is there any other good solution?

java -jar tla2tools.jar -config DieHard.cfg DieHard.tla -continue -dumpTrace json ./test/test.json (trace output error)

tlc version is 2.18.

[Markus Kuppe]

Currently, the -continue and -dumpTrace options are incompatible due to a technical limitation. We are open to considering patches that might address this issue. :-)

Additionally, it's important to note that the JSON encoding does not support multiple traces. In contrast, -dumpTrace tla is specifically designed to handle multiple traces, including counterexamples to liveness properties.

Markus

[zhi niu]

thanks,I would like to ask, when will this patch be completed? if possible?