Introducing TLA+ Intellij plugin

Motivation

Nowadays, it's getting popular to use formal methods to verify complex systems e.g. distributed storages.

TLA+ is a widely-adopted formal specification language created by Leslie Lamport.

The standard way to write and verify TLA+ specification is to use official TLA+ toolbox which is built on top of Eclipse.

Though the toolbox is a full-featured and easy-to-use basically, it was bit frustrating that I cannot use code editing environment I'm familiar with.

For VS code users, there is already a great vscode-tlaplus plugin.

But I'm a fan Intellij IDEA and there seems to be no plugin exists as of now. Then why not creating it?

That's why I developed TLA+ Intellij plugin.

github.com

Features

The plugin is heavily inspired by vscode-tlaplus and it has only subset of features of vscode plugin for now.

Please refer README for the features currently implemented.

But there are several unique points in the intellij plugin.

In this article, I gonna introduce one of them, fine-grained reference resolution.

Reference resolution (i.e. Find usages / Go to definition)

In tlaplus-intellij-plugin, TLA+ files are parsed by similar grammar definition as SANY (TLA+'s syntactic analyzer) which is written in Grammar-Kit's BNF.

tlaplus-intellij-plugin/tlaplus.bnf at v0.4.6 · ocadaruma/tlaplus-intellij-plugin · GitHub

Find usage / Go to definition are implement on top of it.

It means that the correctness of the reference resolution is almost same level as SANY (as well as Toolbox).

For example:

• Local definitions introduced by LET are visible only inside of IN block
• Definitions prefixed by LOCAL are visible only inside the module
• Modules can be instantiated with different name by Bar == INSTANCE Foo

This greatly helps to read complex TLA specs which often separated to multiple sub modules and require us to find the definition across multiple files.

Conclusion

Though still there are points of improvement in tlaplus-intellij-plugin, it will provide better editing experience for Intellij IDEA users.

Please try it out if you're interested, and give me your feedbacks!