Ah, easy enough. I guess I glossed over the command palette piece...this is now working well. Thanks!
The missing piece is to use "TLA+: Check and debug model with TLC" rather than "Check model with TLC”.
From the Command Palette (Ctrl/Cmd+Shift+P), run:
> TLA+: Check and debug model with TLC
You don’t need to create a launch.json or add a TLA+ entry to the standard Run and Debug configuration dropdown. The debugger is launched through the TLA+ extension command instead.
So the distinction is:
• "Check model with TLC" — runs the model checker normally.
• "TLA+: Check and debug model with TLC" — runs TLC under the VS Code debugger.
M.
> On Aug 12, 2026, at 7:19 AM, Brian Curtin <brian.curtin@xxxxxxxxx> wrote:
>
> It's been a while since I've setup a new dev env, and the VSCode work that's been done in the last while looks fantastic. I'm really interested in the interactive state space and breakpoints from the screencasts like [0] .
>
> The env is very up to date, as follows:
> * Java version: java 25.0.4 2026-07-21 LTS
> * VSCode version: 1.133.0 [2026-08-11T22:14:08Z (16 hrs ago)]
> * tlaplus.vscode-ide version: 2026.8.22255 (2 days ago)
>
> Something I can't really figure out is the Run and Debug pane of VSCode to initiate a debugger to hit breakpoints and step in/out/over, either invoked by the green button, or hitting F5 when on a module. In the screencast there is some debugger config setup, in that case for an EWD998App which I've seen Markus talk about.
>
> I can right click on a .tla file and choose "Check model with TLC" which works, but doesn't invoke it in the debugger. The "Add configuration..." debugger dropdown doesn't seem to know about TLA+/TLC; it just has Python, Node, and some default web stuff. I can choose to install an extension from there, but this is already installed. I've also looked at a launch.json, which I recall doing in the past for other things, but that seems to require host/port settings for attaching to a remote debugger, best I can tell.
>
> Does anyone have any configuration details that can bridge the gap to where I am? Happy to update the docs along the way.
--
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/55CD5345-2E65-479C-B476-60B8E6878CD8%40lemmster.de.