How can I avoid dumping *.tlc files

[Chris Ortiz]

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)

[Markus Kuppe]

Hi Chris,

this is a new feature of the TLA+ VS Code extension, introduced in PR #484 [1]. It enables counterexamples to be replayed at any time.

By default, TLC does not generate the .tlc file required for replaying counterexamples, so this enhancement ensures that the necessary data is preserved to support that functionality.

Further discussion would be welcome on the PR itself. If you have suggestions for improvements, please feel free to comment there.

Markus

[1] https://github.com/tlaplus/vscode-tlaplus/pull/484

[Chris Ortiz]

I just tried something.

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

[Chris Ortiz]

Thanks Markus. I reviewed the link and that is actually a cool feature and I would like to try it out one day. I added my suggestion in that PR. 

Regards,

Chris (zitro)