vscode-tlaplus
vscode-tlaplus copied to clipboard
tlaplus
TLA+ language support for Visual Studio Code
```tla ---- MODULE Braf ---- EXTENDS Bags, Naturals VARIABLE x, y Init == /\ x = [ k \in {, } |-> 1 ] /\ y = 1 Next ==...
Is it possible to have `vscode-tlaplus` run tlapm to check the proofs and even to decompose the proofs?
This is extremely minor, but maybe worth noting in a wiki page. PlusCal syntax highlighting won't work if the algorithm is written as: ``` (* --algorithm WriteStealing { { skip;...
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...
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
 [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...
I'm not sure how to set or override constant values. I've figured out how to set model values in the .cfg file, for example: ``` CONSTANT APPROVED = APPROVED ```...
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...
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...
If one clicks on a module name on the EXTENDS line in the toolbox, an editor for that module is opened (including standard modules).