Skip to content

ocadaruma/tlaplus-intellij-plugin

BranchesTags

Repository files navigation

Intellij plugin for TLA+

badge 17965 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

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+)

PlusCal translation

Evaluate expression

Evaluate expression

Debug with TLC Debugger

Debugger

About

Intellij plugin for TLA+ formal specification language.

Resources

Readme

License

Apache-2.0 license
Activity

Stars

61 stars

Watchers

3 watching

Forks

2 forks
Report repository

Releases 35

0.10.2 Latest
Mar 27, 2025
+ 34 releases

Packages

 
 
 

Contributors

Languages