vscode-tlaplus
vscode-tlaplus copied to clipboard
tlaplus
TLA+ language support for Visual Studio Code
With the following `User` and `Workspace` level settings User: `-cp /path/to/CommunityModules.jar` Workspace: `-XX:+UseParallelGC` The CommunityModules won't be added to Java's classpath, causing the EXTENDS to result in a parser error:...
The "Check model with TLC" command is not shown when the model-checking panel has focus. This makes it necessary to e.g. close the panel if a user wants to add...
When actions are instantiated from other modules for example ```tla s1 == INSTANCE step1 Next == \E task \in Tasks: \/ Cancel(task) \/ s1!Acquire(task) \/ s1!Release(task) \/ s1!WakeUp(task) \/ s1!Finished...
Repeatedly hitting this "parse_module" command is a bit annoying, why not automate?
Here `pc` is marked as modified between states. But inner second `pc` does not have mark `M`. Here the same for `resource_needed` variable **Extension's version**: 1.5.0 TLC2 output ``` @!@!@STARTMSG...
[Original observation](https://github.com/alygin/vscode-tlaplus/issues/207#issuecomment-845354312) from @lemmy: >I realized that the dialog could be used to support evaluating expressions in a spec that declares variables and/or constants, but lacks a model: > >```tla...
 The Toolbox colors multi-line (* *) and single-line \* comments differently. I find this useful because it makes me use the former for actual documentation while...
TLC (and the Toolbox) [recently](https://github.com/tlaplus/tlaplus/commit/7c61d1a70f03fe4e54142f59487af90745386b74) implemented functionality to detect PlusCal TLA+ divergence, which should be easy to implement for this extension too: 
https://github.com/tlaplus/tlaplus/issues/485 https://github.com/tlaplus/tlaplus/issues/393
Let `A` be a module that EXTENDS module `B` that happens to be in a library `L`. Library `L` is added to TLC's classpath in `Tlaplus > Java: Options`. Ordinary...