tla.nvim
is a Lua plugin built to provide IDE-like experience while developing
TLA+ and PlusCal specifications. Powered by official TLA tooling.
- TLA tools installation
- PlusCal to TLA+ translation
- TLC model-checking
- TLC output parsing and displaying
- state graph dump to dot-formatted file
- code snippets
- diagnostics via LSP mechanisms
- worksheets and REPL
- PDF generation
- Neovim >= v0.5.0. While
tla.nvim
will aim to always work with the latest stable version of Neovim, there is no guarantee of compatibility with older versions. - Java >= 8. If you have the
JAVA_HOME
environment variable, plugin will work from the start. Otherwise you should specify the location of Java installation. - plenary.nvim. Make sure to have this installed
- Include the plugin to your config. For example, using packer:
use({"susliko/tla.nvim", requires = { "nvim-lua/plenary.nvim" }})
- Setup the plugin in your
init.lua
:
require("tla").setup()
This is equivalent to:
require("tla").setup{
-- Path to java binary directory. $JAVA_HOME by default
java_executable = "path/to/java/bin",
-- Options passed to the jvm when running tla2tools
java_opts = { '-XX:+UseParallelGC' },
-- Only needed if you don't wont automatic tla2tools installation
tla2tools = "path/to/tla2tools.jar",
}
Command | Lua API | Description |
---|---|---|
TlaInstall |
require"tla.install".install_tla2tools() |
Downloads latest tla2tools release. Rewrites existing |
TlaTranslate |
require"tla".translate() |
Translates PlusCal code in the current buffer into TLA+ code |
TlaCheck |
require"tla".check() |
Model-checks TLA+ code in the current buffer and displays results |
TODO gifs
tree-sitter usage for syntax highlighting is encouraged; a tree-sitter grammar exists for TLA+ and PlusCal.