[tlaplus] tla2tools.jar output error trace

[zhi niu <zhiniu28@xxxxxxxxx>]

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.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/78bd1c2b-fe15-4e8f-ae4d-8facb143742an%40googlegroups.com.