好文收藏夹

14.1 介绍 TLC TLC 是检查 TLA+ 错误的程序，它能够处理 Spec == Init /\ [][Next]_<<vars>> /\ Temporal 形式的大部分规范，这通过在配置文件中使用关键字 SPECIFICATION Spec 指定。如果规范不包含时序逻辑，也可以使用 INIT Init 和 NEXT Next 指定。TLC 中要检查的规范叫做模型。 TLC 不能处理 \EE 运算符，用户应当单独检查 \EE 涉及的子规范。这可以通过 5.8 节介绍的，为要使用 \EE 隐藏的变量在实例化时显式指定映射来绕过。 TLC 可以检查如下种类的情况： 无意义的表达式（6.2 节） 死锁，即 Next 步的前提不能被满足。但有的系统允许死锁表示系统按预期终止 使用 PROPERTY 关键字检查某公式是否为真。TLC 实际上并不是检查 Spec => Prop ，而是对于 SPECIFICATION 和 PROPERTY 分拆安全性和活跃性部分，分别检查 SPECIFICATION 的安全性蕴含 PROPERTY 安全性 SPECIFICATION 蕴含 PROPERTY 的活跃性 由于 PROPERTY 的安全性和活跃性分别检查，因此 TLC 不能处理两者相互影响的情况，也即不能处理非状态机闭包 如果想要表达公式一直为真，可以使用 [] 或者 INVARIANT 关键字描述。如果使用 INVARIANT 关键字，要检查的必须是一个单状态公式 TLC 在开始检查前需要指定规范中常数参数的取值。 TLC 有两种工作模式，检查 所有 可到达的状态，即模型检查模式；或者随机生成状态作为系统行为，即模拟模式。本节我们先讨论前者。 对于状态过多、或者无穷状态的规范，我们可以指定约束限制一些不必要状态，这可以使用 CONSTRAINT 关键字指定约束公式。 TLC 对于不同类型公式的检查速度不同，建议按照类型不变量、检查安全性、检查活跃性的顺序进行检查。完成检查后，我们还可以编写一个“事后规范”，检查规范是否能蕴含这个“事后规范”。 14.2 TLC 能处理什么 TLA+ 的描述性太强，不存在能检查 TLA+ 所有规范的工具。TLC 能处理 ...

13.1 介绍 TLATeX 使用 LaTeX 作为排版引擎由 tla 文件输出 PDF 等更易读的文件。TLATeX 提供了显示行号、传递 LaTeX 命令等功能，详见文档。 13.2 注释阴影化 TLATeX 可以控制注释区域的阴影深度，或者结合其他工具调整阴影。 13.3 对规范进行排版 规范的排版不会破坏跨行对齐。符号之间不使用空格与使用一个空格的排版相同。排版会将模块前后的文字一同处理，这种特性也可以被屏蔽。排版会检查部分词法错误。 13.4 对注释进行排版 TLATeX 会区分单行注释与多行注释。多行注释有如下三种写法： (**************) \************* (* This (* This is *) \* This is is a (* a comment. *) \* a comment. comment. *) (**************) \************* 其中前两种需要注意对齐。 多行注释的排版会自动检测段落、表格等多种情况进行折行，但不会进行跨行对齐。 注释的一些语法： `这部分注释应用规范的样式（包括规范中的字符串样式）' `^这部分注释应用注释的样式，交给 LaTeX 进行排版^' `.这部分注释不进行排版，以 ASCII 形式输出.' ``本行首末是左右引号'' `~这部分注释不会显示~' 13.5 调整输出格式 TLATeX 可以调整字号、文字高度宽度、偏移量。 13.6 输出文件 TLATeX 可以配置输出文件的文件名、ASCII 版本的输出、LaTeX 样式。 13.7 故障诊断 TLATeX 会依次产生一些中间文件，并最终输出 PDF 等阅读文件。命令行输出和中间文件日志有助于定位问题。 13.8 使用 LaTeX 命令 通过 `^这部分注释应用注释的样式，交给 LaTeX 进行排版^' 这种方式使用 LaTeX 进行排版。由于 LaTeX 代码的可读性差，因此推荐使用如下方式同时维护一份 ASCII 可读的注释 \***************************...