Re: [tlaplus] tla2tools.jar output error trace

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

> 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.