Re: [tlaplus] How can I avoid dumping *.tlc files

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

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

> On Feb 25, 2026, at 2:54 PM, Chris Ortiz <zitroomega@xxxxxxxxx> 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)

-- 
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 visit https://groups.google.com/d/msgid/tlaplus/B9142495-7DB0-4284-88F5-8582A578E5F5%40lemmster.de.