New VSCode debugger setup, unsure what's missing

[Brian Curtin]

Hey all,

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.

Thanks,

Brian Curtin

[Markus Kuppe]

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.

[Brian Curtin]

Ah, easy enough. I guess I glossed over the command palette piece...this is now working well. Thanks!

--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/55CD5345-2E65-479C-B476-60B8E6878CD8%40lemmster.de.