TLA+ on OpenBSD
Couple years ago I decide to know more about TLA+. TLA+ is a tool for formal verification of models. Unfortunately TLA+ is not supported by OpenBSD. I have found an installation guide for Linux users and tried to run TLA+ on OpenBSD and failed on step with building Toolbox. But when I’m going through these steps on OpenBSD I have found that there is no Toolbox binaries for OpenBSD, I submitted issue and developers said there are no plans to build binaries for OpenBSD. TLA Toolbox requires Eclipse and port for it was outdated for a long time.
Well, we can run TLA+ in a headless mode without GUI. It is required to
download
tla2tools.jar
and install Java package. Running TLA+ in command line:
java -Xmx30G -cp ../tla2tools.jar tlc2.TLC MC -deadlock -workers 12
. The
setting -Xmx30G
denotes the amount of memory to allocate to the model checker
and -workers 12
the number of worker threads (should be equal to the number
of cores on machine). The setting -deadlock
ensures that TLC explores the
full reachable state space, not searching for deadlocks.
Using TLA+ in console is inconvenient a bit. We will use it with tlaplus_jupyter. It is a plugin for Jupyter, popular system for interactive computations. By default it supports only Python kernel, but it is possible to extend it with kernels that add support for other programming languages.
Create Python virtual environment and install tlaplus-jupyter
package in it:
$ python -m venv tlaplus
$ . tlaplus/bin/activate
(tlaplus_env) $ pip install tlaplus_jupyter
(tlaplus_env) $ python -m tlaplus_jupyter.install
Installing Jupyter kernel spec
Downloading tla2tools.jar to /home/sergeyb/Downloads/tlaplus_env/lib/python3.7/site-packages/tlaplus_jupyter/vendor/tla2tools.jar
(tlaplus_env) $ jupyter notebook
Now we are ready to start Jupyter notebook:
(tlaplus_env) $ jupyter notebook
To create a new TLA+ notebook click on the New button and select TLA+ in a dropdown menu. It is also handy to enable line numbering inside cells (View -> Toggle Line Numbers) since syntax checker refers to problems by their line numbers.
Learn more about TLA+
- Learning TLA+ on website of Leslie Lamport
- TLA+ in Practice and Theory
- Learn TLA+