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

Re: [tlaplus] tla2tools.jar output error trace

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.


> On Nov 15, 2023, at 5:15 PM, zhi niu <zhiniu28@xxxxxxxxx> wrote:
> 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/26A6F82B-1B16-45F4-A9D8-84E80585A517%40lemmster.de.