vscode-tlaplus
vscode-tlaplus copied to clipboard
tlaplus
Proof of concept Model Editor web view
- In the most simple of model checking cases, this works now; PoC finshed to a point to ping mku.
- Minor clean-up and a few comments before making a PR, per @lemmy
This is an experimental addition (a rough proof of concept) of introducing a Toolbox-esque Model Editor into the VS Code extension.
Kudos, SonarCloud Quality Gate passed!
0 Bugs
0 Vulnerabilities (and 
0 Security Hotspots to review)
0 Code Smells
No Coverage information
No Duplication information
![sonarqubecloud[bot] avatar](https://avatars.githubusercontent.com/in/12526?v=4 "Published by a pub.dev verified publisher"){kind=small}
@quaeler, thanks for putting your effort into adding this feature to the extension! And sorry for the late reply, things have been a bit disrupted recently.
As a PoC it looks good. But before moving further, I'd like us to come up with a vision of what features this editor should support. My main concerns are:
- VS Code is not very friendly to interactive user interfaces. It's more a text editor than an IDE, so reimplementing the UI-related Toolbox features might be quite a challenge.
- The model editor in the Toolbox mixes things from different areas: the model itself, tla2tools argument, jvm options, other (for instance, I have no idea where it puts the model description). Bringing them all to the extension will require a (presumably) great deal of preparation work.
What features do you think this editor should have when it's ready for publishing?
cc @lemmy
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 model checking. For example, an Init predicate is specified as x \in 1..3 instead of x \in Nat with the model redefining Nat to 1..3. In other words, the "spec-model" separation keeps specs pristine and prevents them from being tainted.
To encourage users to separation the model from the spec, the VSCode extension should thus support definition overrides, state & action constraints, ... somehow; either with an interactive UI or - if it better aligns with the VSCode best practices - a text-based interface.
A low-hanging fruit might be - for the vanilla extension - to generate not only a .cfg file automatically, but also a .tla file (similar to what the Toolbox does).
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).