# TLA+ on OpenBSD

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
(tlaplus_env) $jupyter notebook  Now we are ready to start Jupyter notebook: (tlaplus_env)$ jupyter notebook