用于TLA的Jupyter内核
tlaplus-jupyter的Python项目详细描述
特拉普卢斯朱庇特
用于TLA+和Pluscal规范语言的Jupyter内核。在
- 基于官方lexer的语法高亮显示。在
- 表达式的REPL功能。在
- 可以用活页夹在线执行。Try it now!
- 不需要安装TLA工具箱：Java和Python就足够了。在
在
安装
tlaplus_jupyter是一个可以与pip一起安装的python包。支持Python2和3。要安装运行：
pip install tlaplus_jupyter
python -m tlaplus_jupyter.install
最后一步将在系统中注册tlaplus_jupyter作为Jupyter内核，并下载tla2tools.jar。之后，Jupyter可以像往常一样启动：
要创建一个新的TLA+笔记本，请单击New按钮，并在下拉菜单中选择TLA＋。在单元格内启用行号也很方便（查看>切换行号），因为语法检查器通过行号来指出问题。在
使用
基本用法在intro notebook中解释。在
tlaplus_jupyter支持执行时具有不同行为的多种类型的单元：
- 在
具有
在full module definition的单元格。执行时，内核将执行语法检查（使用tla2三一三一)并报告错误。如果模块包含Pluscal程序内核也会将其转换为TLA。在 - 在
以
%tlc:ModuleName开头的单元格，其中ModuleName是先前执行的模块之一的名称。在本例中，单元被视为TLC模型检查器的配置文件。例如，要检查模型Spec的规范Spec和不变量TypeOk，请执行以下操作：%tlc:DieHardTLA SPECIFICATION Spec INVARIANT TypeOKInit和next state公式可以设置在关键字
INIT和NEXT之后。常量定义应该跟在CONSTANTS关键字后面，用换行符或逗号分隔。可能的配置语句和语法的描述在Specifying systems书的第14章中给出。在可以在TLC名称后指定模块名称：
%tlc:DieHardTLA -deadlock SPECIFICATION SpecTLC评估在所有已定义模块的上下文中进行。所以，如果模型引用另一个模型，那么另一个模型也应该在某个单元格中。在
在 - 在
不包含
在%-magic或模块定义的单元格被视为常量表达式，并将在执行时打印其结果。与^{一样，求值发生在所有已定义模块的上下文中，因此表达式可以引用已计算模块中定义的任何内容。在 - 在
命令
在%log/%log on/%log off对应显示当前打开的笔记本的内核日志/启用日志记录/禁用日志记录。在
与Binder共享可执行模型
通过将Dockerfile复制到存储库根目录，可以很容易地使Github上共享的TLA+模型可运行。之后，可以在Binder使用指向此类回购的URL来启动一个动态TLA+环境。在
相关项目
vscode-tlaplus用于VSCode编辑器的酷插件，具有语法突出显示和用于显示跟踪的自定义小部件。在
许可证
- 项目
标签：
欢迎加入QQ群-->： 979659372
