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
