Spectacle Integration

[lemmy]

Overview Spectacle is a browser-based TLA+ interpreter implemented in JavaScript. It enables interactive exploration of TLA+ behaviors and provides visualization and animation of state transitions.

Objective Integrate Spectacle into the VS Code TLA+ extension to allow users to visualize and explore TLA+ specifications directly within the editor environment.

Proposed Implementation

• Bundling: Package Spectacle as part of the VS Code extension distribution.
• Command Integration: Add a command (e.g., TLA+: Open in Spectacle) that opens the currently active TLA+ file in the Spectacle interface.
• Runtime Environment: Launch a lightweight HTTP server within the VS Code process to host the Spectacle application.
• Interaction Model: When invoked, the command should serve the active specification file to the Spectacle instance and open it in the user’s default browser or a VS Code webview. (Spectacles spec editor could be hidden in favor of VSCode's editor)

Benefits

• Enables interactive, visual debugging and behavior exploration.
• Provides a smoother workflow for users.

/cc @will62794

[lemmy]

At present, the Spectacle repository is too large (tree-sitter-tlaplus is 5mb) to be directly bundled within the VS Code extension. As an initial step, we will need to produce a minimal, standalone distribution of Spectacle suitable for packaging.