This is an old revision of the document!
Debugger
TLA+ tools come with a debugger that allow you to debug your specifications. See it in action:
Graphical and time-traveling debugging
You will need the SVG extension: https://marketplace.visualstudio.com/items?itemName=jock.svg.
fponzi