Markus Alexander Kuppe

The biggest concern about the lack of a model editor is the missing separation between the spec and models, which causes users to write specs that are tailored to TLC...

The Twitter thread ending with https://twitter.com/miguelraz_/status/1336892757885865985 shows how the lack of a model editor is a usability impediment (especially for learners).

FWIW: The model-checking results web-view doesn't work (not shared) when [live-sharing with VSCode](https://code.visualstudio.com/learn/collaboration/live-share).

https://code.visualstudio.com/blogs/2021/10/11/webview-ui-toolkit

@johnyf FYI, since multiple definitions on the same line in a LET/IN recently came up in a different context.

If yes, not exhaustively because the second `GraphNodePos` is still black.

Hack that adds the command `tlaplus.debugger.smoke` mentioned above: ```diff diff --git a/package.json b/package.json index 23a6451..e3d1135 100644 --- a/package.json +++ b/package.json @@ -192,6 +192,13 @@ "icon": "$(debug-alt)", "category": "TLA+" }, +...

Prerequisite: Install [vscode-tlaplus nightly build](https://marketplace.visualstudio.com/items?itemName=alygin.vscode-tlaplus-nightly)! Let `Spec.tla` be the spec one is working on. To activate "smoke testing", one has to create `SmokeSpec.tla` and `SmokeSpec.cfg` with the following content: ```tla...

[This nonsense](https://sonarcloud.io/project/security_hotspots?id=alygin_vscode-tlaplus&hotspots=AXx3eCGxYl8gH2ijuiCB) is blocking this now. @alygin I suggest we turn SonarCloud off. Taken care of in https://github.com/alygin/vscode-tlaplus/commit/e8de86c48870cc17bf82f7ef8af0d5dfd7041e8b

@peterzeller Thanks for volunteering! :-) Agreed! Ideally, this is implemented as a lookup into SANY's AST similar to how it is done in `TLAHyperlinkDetector.java`. That way, the Eclipse and VSCode...