okue/tlaplus-intellij-plugin

Intellij plugin for TLA+

Intellij plugin for TLA+ formal specification language.

This plugin is heavily inspired by TLA+ for Visual Studio Code.

Features

Syntax highlighting

• Supports syntax highlighting for TLA+, PlusCal, TLC cfg file

Run TLC model checker

Current limitations:

• You have to write TLC config file (.cfg) directly instead of GUI like toolbox

• TLC’s command line args are not configurable

• Error trace exploration is not supported

Find usages (Go to declaration)

• References are searched across different modules including standard modules

Code completion

• Support basic keyword completion and variable/constant/operator name completion

PlusCal (Translate into TLA+)

Evaluate expression