TLA⁺ Nightly for Visual Studio Code

ATTENTION: This is the preview version of the TLA⁺ for Visual Studio Code extension, used for early feedback and testing.

ATTENTION: Both the stable and nightly versions cannot be used at the same time. You must disable or uninstall one of them.

TLA⁺ Nightly:

• Is released more frequently.
• Includes features and bug fixes that may not have been tested yed.
• May include nightly builds of the TLA⁺ tools.

This extension adds support for the TLA⁺ formal specification language to VS Code. It also supports running the TLC model checker on TLA⁺ specifications.

Features

• TLA⁺ and PlusCal syntax highlighting and code snippets.
• Running the PlusCal-to-TLA⁺ translator and module parser.
• Running TLC model checker on TLA⁺ specifications.
• Model checking process and result visualization.
• Evaluating constant expressions.
• Converting TLA⁺ specifications to LaTeX and PDF documents.
• Code completion.
• Code on-type formatting.
• Powered by the official TLA⁺ tools.

Documentation

The project's Wiki provides information on how to install, configure and use the extension.

• How to Install
• Getting Started
• Settings
• Commands
• Setting up Environment
• Caveats
• Troubleshooting

Contributing

All forms of contribution are highly welcome! Feel free to file bugs, propose improvements, ask questions, send other feedback.

If you decide to pitch in and write some code, this document will provide you with useful information: CONTRIBUTING.md.

TLA⁺ Resources

If you're not familiar with TLA⁺, but want to get a grasp on it, the following list of resources is a good starting point:

• TLA⁺ Home Page on Leslie Lamport's website.
• Introduction to TLA⁺ and PlusCal by Hillel Wayne.
• TLA⁺ in Practice and Theory by Ron Pressler.
• A collection of TLA⁺ specification examples in the TLA⁺ repository.

License

MIT