Markus Alexander Kuppe

Better separate models and specs

17

We want specs to describe systems. Verification with model-checkers such as TLC is import, but ultimately a secondary concern. We do not want users to write specs that are amenable...

TLA+ CommunityModules and vscode-tlaplus

3

The popularity of the CommunityModules warrants that we bundle (or otherwise) include its jar in the vscode extension.

Error-trace shows a bag (multiset) like a sequence

5

```tla ---- MODULE Braf ---- EXTENDS Bags, Naturals VARIABLE x, y Init == /\ x = [ k \in {, } |-> 1 ] /\ y = 1 Next ==...

Support github.dev & vscode.dev web editors

2

The extension doesn't work in the github.dev web editor: "The 'TLA+' extension is not available in Visual Studio Code for the Web." > Why is an extension not installable in...

Add "creation and last modified" footer to specs

2

The Toolbox automatically adds a footer to every spec that shows the original author and creation date and all modifications by other authors. Toolbox implementation: https://github.com/tlaplus/tlaplus/blob/df144c5f0e93b996362a199afa43cf453f4c2856/toolbox/org.lamport.tla.toolbox.editor.basic/src/org/lamport/tla/toolbox/editor/basic/TLAEditor.java#L551-L640

Continuous (smoke) testing with TLC simulator upon editor save

3

 [Hi-res screencast at https://www.youtube.com/watch?v=jcsQzzeVjuI](https://www.youtube.com/watch?v=jcsQzzeVjuI) ----- # Install/Activate 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...

Run TLC in VSCode integrated terminal

2

Some TLC-specific TLA+ operators such as [`PickSuccessor`](https://github.com/tlaplus/CommunityModules/blob/11a0679c484893b98982a47a0d625ae5d70ed0c3/modules/TLCExt.tla#L30-L40) prompt users for (interactive) input (on `stdin`). This is currently unsupported because the extension just prints TLC's stdout/stderr to the output section of...

"Go to definition" for definitions in module extended

1

Let `B` be a module and `E` be an extender (EXTENDS B). Clicking `Go to definition` on a symbol in `E` that is defined in `B` doesn't work. ![Peek 2020-12-10...

Clicking on a module name on the EXTENDS line should open the module

7

If one clicks on a module name on the EXTENDS line in the toolbox, an editor for that module is opened (including standard modules).

Split parsing from PlusCal translation

1

[Automatic module parsing](https://github.com/alygin/vscode-tlaplus/wiki/Automatic-Module-Parsing) is super useful but gets in the way if a user wants to modify the generated TLA+. In these cases, it would be better to separate parsing...