参考文档：C:\ProgramFiles\TLAToolbox-1.6.0-win32.win32.x86_64\plugins\org.lamport.tla.toolbox.doc_1.7.0.202004251858\pdfs\summary-standalone.pdf

模块级结构 -- Module-Level Constructs
常数运算符 -- The constant Operators
其他构造 -- Miscellaneous Constructs
动作运算符 -- Action Operators
时态运算符 -- Temporal Operators
用户可定义的运算符符号 -- User-Definable Operator Symbols
运算符的优先范围 -- Precedence Ranges of Operators
标准模块中定义的运算符 -- Operators Defined in Standard Modules
排版图形符号的ASCII表示 --ASCII Representation of Typeset Symbols

 

TLA+ Toolbox使用向导

Step-1. 添加新规约：

File -> Open Spec  -> Add New Spec 

注意：

a. pecification name 规约名必须与顶级模块名相同

        e.g.    规约文件名 Transfer.tla  文件中，必须和顶级模块名 ---- MODULE Transfer ---- 一致。

Step-2. 解析规约：

File -> Parse Spec 

Step-3. 添加模型

TLC Model Checker  -> New Model...