[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] tla2tools.jar output error trace

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.