Jupyter kernel for TLA⁺ and Pluscal specification languages.
tlaplus_jupyter is a python package installable with
pip. Python 2 and 3 are supported. To install run:
pip install tlaplus_jupyter python -m tlaplus_jupyter.install
The last step will register
tlaplus_jupyter as a Jupyter kernel in your system and will download
tla2tools.jar. After that Jupyter can be started as usual:
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.
Basic usage is explained in an intro notebook.
tlaplus_jupyter supports several types of cells with different behavior on execution:
full module definition. Upon execution kernel will perform syntax check (with tla2sany.SANY) and report errors if any. If the module contains Pluscal program kernel will also translate it to TLA.
Cell starting with
ModuleName is the name of one of the modules previously executed. In this case, the cell is treated as a config file for the TLC model checker. For example to check spec
Spec and invariant
TypeOk of model
DieHardTLA execute following:
%tlc:DieHardTLA SPECIFICATION Spec INVARIANT TypeOK
Init and next state formula can be set after keywords
NEXT correspondingly. Constant definitions should follow
CONSTANTS keyword separated by newline or commas. Description of possible config statements and syntax is given in chapter 14 of Specifying systems book.
Custom TLC flags may be specified after the module name:
%tlc:DieHardTLA -deadlock SPECIFICATION Spec
TLC evaluation happens in the context of all defined modules. So if model refers to another model that other model should be at some cell too.
Cells containing neither
%-magic nor module definition are treated as a constant expression and will print its results on execution. As with
!tlc evaluation happens in the context of all defined modules, so the expression can refer to anything defined in evaluated modules.
%log on /
%log off correspondingly shows kernel log / enables logging / disables logging for currently open notebook.
vscode-tlaplus Cool plugin for VSCode editor with syntax highlight and custom widgets for displaying traces.