Interactive State-Space Navigation with Successor Selection and Backtracking #475
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Contributor
There was a problem hiding this comment.
Pull request overview
This PR implements an interactive state-space navigation feature for the TLA+ debugger, allowing users to navigate between states using a "Go to State" command. This is the frontend implementation corresponding to backend changes in tlaplus/tlaplus#1270.
Key Changes
- Added a debug adapter tracker to detect the
supportsGotoStatecapability from the backend debugger - Implemented a
gotoStatecommand that sends custom DAP requests to navigate to specific states - Added UI integration through context menu and keyboard shortcut (ctrl+g/cmd+g) in the variables view
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 5 comments.
| File | Description |
|---|---|
| src/main.ts | Registers the new TLADebugAdapterTrackerFactory and gotoState command with VS Code extension context |
| src/debugger/debugging.ts | Implements the tracker factory to detect backend capabilities and the gotoState function to handle state navigation |
| package.json | Defines the command, adds it to the debug variables context menu, and configures the keyboard shortcut |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
lemmy
force-pushed
the
mku-DAPStateSpaceExploration
branch
2 times, most recently
from
e28b6b4 to
2ad8a60
Compare
- Introduced a new command `tlaplus.debugger.gotoState` to navigate to a specific state in the TLA+ debugger. - Registered the command in the command palette and added a keyboard shortcut (Ctrl+G / Cmd+G). - Updated context menu for debug variables to include the new command. [Feature] Signed-off-by: Markus Alexander Kuppe <[email protected]>
- Added TLADebugAdapterTrackerFactory to monitor debug adapter protocol messages. - Tracks supportsGotoState capability from the debugger backend's initialize response. - Updated package.json when clauses to conditionally show command in context menu and keybindings. - Command now only appears when the debugger explicitly declares support for the feature. [Feature] Signed-off-by: Markus Alexander Kuppe <[email protected]>
- Updated debug/variables/context menu when clause to check debugProtocolVariableMenuContext == 'state'. - The TLA+ debugger backend sets __vscodeVariableMenuContext property on state variables. - Command now only appears for actual state variables, preventing invocation on non-state variables. - Improves UX by hiding the command when it is not applicable. [Feature] Signed-off-by: Markus Alexander Kuppe <[email protected]>
lemmy
force-pushed
the
mku-DAPStateSpaceExploration
branch
from
2ad8a60 to
f317aa4
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Frontend of tlaplus/tlaplus#1270
Limitations
The “Go to State” context menu appears even when it’s not relevant to the current tree item.