|
参考文档：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...
| 
转播
