I am guessing that the vscode dumptrace option support tlc and the tla2tools support tla. If I used the TLC option below:
-coverage 1 -dumpTrace tlc trace.tlc -dump dot,colorize,actionlabels ${modelName}.dot -cleanup -teSpecOutDir states
It does not produce default *.tlc in my working directory but I still got the trace.tlc in binary format.
And if I use the one here:
-coverage 1 -dumpTrace tla trace.tlc -dump dot,colorize,actionlabels ${modelName}.dot -cleanup -teSpecOutDir states
I will get both the *.tlc default file and trace.tlc and the later in valid TLA format.
I am not sure which is the expected behavior.
Thanks,
Chris
On Wednesday, February 25, 2026 at 2:54:53 PM UTC-8 Chris Ortiz wrote:
Hello,
How can I avoid having the default *.tlc dump into my working directory?
My TLC option is:
-coverage 1 -dumpTrace json trace.json -dump dot,colorize,actionlabels ${modelName}.dot -cleanup -teSpecOutDir states
I already have an explicit -dumpTrace but it still dump the default *.tlc file which just keep on accumulating on my working directory.
Thanks,
Chris (zitro)