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 能处理 TLA+ 的大多数情况。

14.2.1 TLC 值

TLC 能表达的值比 TLA+ 更有限，TLC 值的四种基本类型是布尔型、整数、字符串、作为常量符号的模型值。TLC 值是由

  • 基本类型

  • 可比较的 TLC 值构成的有限集

  • 定义域和值域全部是 TLC 值的函数

组成。两个值可比较的定义是 TLA+ 语义下两个值可以判断是否相等。字符串和数字在 TLA+ 中是不能判断相等的。包含不同个数元素的集合，即使元素分别是是字符串和数字，是可以判断不相等的。更精确的定义见 14.7.2

14.2.2 TLC 如何对表达式求值

检查规范的过程就是对表达式求值，查看结果是否为真的过程。

TLC 有短路特性，以此避免越界。

TLC 只能处理绑定变量\E x \in S: p的表达式，而且S必须是有限集。与 TLA+ 不同，TLC 不能处理未绑定变量的表达式\E x: p。

TLC 在CHOOSE无法取到合法的值时会报错。

TLC 仅在需要的时候求值，例如[n \in Nat |-> n * (n + 1)][3]中Nat不是有限集，但可以求值。

TLC 对于合法的递归表达式有时不能求值，例如 6.3 节使用record.f和record.g解决依赖多个函数的问题。TLC 会完全对record求值，再取它的成员，因此有些情况下会造成自我依赖，进入死循环。

14.2.3 赋值和替换

TLC 的赋值指的是配置文件CONSTANT部分c = v形式的语句。v必须是一个 TLC 值，或者是 TLC 值的有限集。v可以包含模型中的某个变量，即模型值，作为一个常量符号。c可以是规范中定义的符号或者常数参数，TLC 会对其进行赋值或者覆盖。覆盖常常用于使用模型值表示 TLC 不能表达的 TLA+ 表达式，为了提高可读性，一般写作symbol = symbol。

CONSTANT部分可以应用替换，表示成c <- d的形式。替换与复制的区别是替换的d需要是有定义的符号，而v需要是 TLC 值。替换可以用于，在一个简单、快速写成的规范中用更高效的实现替换部分标识符。

14.2.4 时序逻辑公式求值

TLC 可以对满足如下条件的 TLA+ 时序逻辑公式求值：表达式良定义并且其“组成部分”都可以求值。良定义指的是表达式由如下四种公式合取而成：

  • 单状态公式

  • 不变量公式[]P，其中P是单状态公式

  • [][A]_v，其中A是动作v是单状态公式

  • 由如下两种合取而成的公式

    • 单状态时序逻辑公式，既不包含'变量

    • 满足公平性、[]<><<A>>_v、<>[][A]_v的形式，其中A是动作v是单状态公式。公平性的“组成部分”是<<A>>_v和ENABLED <<A>>_v

14.2.5 覆盖模块

TLC 支持使用 Java 实现覆盖模块，标准模块Naturals，Integers，Sequences，FiniteSets，Bags已经被覆盖。

14.2.6 TLC 如何计算状态

状态就是所有变量都具有对应的值，TLC 将不带'的变量计算对应的值，然后计算Next公式。Next公式的计算与 14.2.2 节提到的计算有两点不同：

  1. 析取子式（包括\/，\E，=>）隔离计算。合取子式仍然会依次计算并提前终止。

  2. 对于第一次出现的'的变量x' = e进行赋值并对公式返回TRUE。除这种情况以外，TLC 会对'的变量的访问报错。

对于ENABLED A这种公式，TLC 把A作为Next公式进行计算，如果有至少一个可达状态，ENABLED A的值就为真。

14.3 TLC 如何检查性质

14.1 节介绍 TLC 有两种工作状态，检查所有行为或者随机模拟一些行为。首先我们介绍前者。

将 TLC 配置文件中的各段进行整理，可以得到如下几类公式。定义某类公式为空表示为真：

  • Init，由INIT指定，或者是SPECIFICATION中所有单状态公式的合取

  • Next，由NEXT指定，或者是SPECIFICATION中所有形如[][N]_v的N合取

  • Temporal，SPECIFICATION中既不是单状态公式也不是[][N]_v的公式合取，通常表达活跃性

  • Invariant，由INVARIANT指定，或者是PROPERTY中形如[][I]的I合取

  • ImpliedInit，PROPERTY中单状态公式的合取

  • ImpliedAction，PROPERTY中形如[][A]_v的[A]_v合取

  • ImpliedTemporal，PROPERTY中除Invariant以外的时序逻辑公式

  • Constraint，由CONSTRAINT指定

  • ActionConstraint，由ACTION-CONSTRAINT指定。该类公式与Constraint类似，但是Constraint排除了一些状态，ActionConstraint排除了一些状态转移。Constraint P等价于ActionConstraint P'

14.3.1 模型检查模式

该模式下 TLC 维护两个数据结构：有向图G的点集、边集分别存储可达的状态和转移，队列U存储G中尚未检查邻接点合法性的点。

TLC 维护的不变量包括：

  • G中的状态满足Constraint

  • G中的状态有自环边

  • G中的状态是由满足Init的状态可达的

  • G中的边满足Next /\ ActionConstraint

  • U中的点不重复，且都在G中

  • 对于G中不在U中的点s，如果t满足Constraint且边(s, t)满足Next /\ ActionConstraint，那么t和(s, t)也在G中

TLC 按照如下流程进行检查：

  • 检查 TLC 常数参数的指定是符合ASSUME的

  • 按照Init计算初始状态。对于每个初始状态s：

    • 检查Invariant和ImpliedInit

    • 如果s满足Constraint，将s添加到G和U中，将(s, s)添加到G中

  • 当U不为空时：

    • 队首出队，记为s

    • 计算s所有可达的状态，记为集合T

    • 如果T是空集而且 TLC 配置为不允许死锁，报告错误

    • 对于T中的每个状态t：

      • 检查t满足Invariant，(s, t)满足ImpliedAction

      • 如果t满足Constraint且(s, t)满足ActionConstraint：

        • 如果t不在G中，将其加到G中，并在U的队尾入队。(s, t)、(t, t)加到G中

如果ImpliedTemporal不为空，在G每次加边时 TLC 都会为新增加的边求出Temporal和ImpliedTemporal的值。TLC 周期性检查G中由初始状态出发形成的无限长的路径是否满足Temporal => ImpliedTemporal。

14.3.2 模拟模式

模拟模式不尝试检查所有的状态，因此可以看作U的最大长度限制为 1。在行为的状态数达到设定值的时候，TLC 进行时序逻辑相关性质的检查，并将G和U恢复到初始状态重新进行模拟。

14.3.3 视图和指征

在模型检查模式中，G中的节点实际上是视图而不是状态，这么做的原因是视图可以控制仅用部分变量区分G的点。视图在配置文件的VIEW进行指定。视图常见的应用是，用户为了调试规范增加了一些辅助变量，但是这样会增大搜索空间，所以用视图指定为原始的非调试变量。

由于视图限制了一些状态加入G，TLC 可能会因此将时序逻辑性质判断错误。

在实现中，TLC 是通过视图的哈希，即指征进行区分。这样又引入了哈希碰撞引发的错误概率。TLC 会在模型检查的结果中汇报这种概率。

在模拟模式中，没有这两个概念以及它们潜在的错误。

14.3.4 利用对称性

对称性指轮换对称性，在配置文件中通过SYMMETRY Perms指定。Perms常常通过 TLC 模块的Permutations(S)运算符表示S的元素是满足轮换对称性的。在 TLC 增长G和U时检查轮换对称性引起的重复，从而避免添加不必要的状态。如果有多个集合S1，S2……，可以表达成Permutations(S1) \union Permutations(S2) ...。

TLC 同样会因为对称性跳过状态从而将时序逻辑性质判断错误。

在误用对称性时，TLC 会报告Failed to recover the state from its fingerprint.

对称性也是仅在模型检查模式有效。

14.3.5 活跃性检查的局限

在某些情况下，TLC 需要限制搜索空间的数目即G的大小，从而可能导致规范的活跃性不满足。例如对于

EvenSpec == (x = 0) /\ [][x' = x + 2]_x /\ WF_x(x' = x + 2)

检查<>(x = 1)。TLC 不能处理无穷的状态，为了检查能终止，需要用CONSTRAINT限制G的大小（此处为x的取值）。而x的限制取值会导致G产生的无穷行为末尾出现x保持不变的无限个状态，因此弱公平性为假。按照蕴含的定义，WF_x(x' = x + 2) => <>(x = 1)为真，也就是 TLC 没有检查出错误。

为了避免这个情况，可以用一个必定为假的活跃性性质，检查 TLC 有没有正常工作。

14.4 TLC 模块

TLC 模块提供了一些辅助功能。

Print(out, val)运算符的值是val，但是 TLC 在对其进行求值时会打印out。

Assert(val, out)起到了断言的作用，如果val为假，TLC 会打印out并终止。

JavaTime会打印当前时间。

1 :> "ab" @@ 2 :> "cd"表示定义域为{1, 2}取值分别为{"ab", "cd"}的函数。

前文中提到的Permutations(S)定义如下：

Permutations(S) == {f \in [S -> S]: \A w \in S : \E v \in S : f[v] = w}

使用Permutations(S)和:>、@@运算符，我们可以表达更复杂的对称性。例如对于两个处理器p1、p2分别有相关的地址a11、a12和a21、a22，我们可以定义对称性为

Permutations({a11, a12}) \union {p1 :> p2 @@ p2 :> p1
                                  @@ a11 :> a21 @@ a21 :> a11
                                  @@ a12 :> a22 @@ a22 :> a12}

这个并集操作两边分别是交换第一个处理器相关的地址，以及交换两个处理器。可以验证所有的对称性可以通过这两个交换构造出来。

SortSeq(s, Op(_, _))运算符对序列按照全序运算符Op进行排序。

14.5 如何使用 TLC

14.5.1 运行 TLC

TLC 在运行时有诸多配置，包括：

  • -deadlock不检查死锁

  • -simulate模拟模式

  • -depth num模拟模式下行为的长度，默认为 100

  • -seed num模拟模式下随机数种子，取值在 -2^63 到 2^63 - 1 之间

  • -aril num模拟模式下影响初始化的随机数种子

  • -coverage num每隔num分钟打印赋值相关动作的执行覆盖情况

  • -recover run_id表示从run_id的存盘点继续

  • -cleanup清理临时文件，注意多个 TLC 实例运行时该选项会破坏运行中的实例

  • -difftrace num打印错误时使用在状态转移之间仅打印差异部分

  • -terse打印错误时打印精简的变量值

  • -workers num使用num个线程寻找可达状态，默认为 1

  • -config config_file表示使用config_file作为配置文件，默认与 TLA+ 文件同名

  • -nowarning不显示警告

14.5.2 调试规范

TLC 在运行时会打印很多信息，这里仅介绍几个不直观的输出：

Implied-temporal checking--relative complexity = 8.

表示估计的时序逻辑公式相对于安全性公式的复杂度，这个值越高在检查活跃性时耗时越长。

Progress(9): 2846 states generated, 984 distinct states found. 856 states left on queue.

括号中的9表示直径，即G中从初始状态延伸的路径长度的最大值。在多线程情况下，这个值可能并不准确。856即为U的长度，一般而言整个过程中该长度先上升后下降。

-- Checkpointing run states/99-05-20-15-47-55 completed

states/99-05-20-15-47-55即为run_id存盘点。

14.5.3 高效使用 TLC 的提示

先为模型的常数参数赋较小的值，再逐渐增大。模拟模式在运气好的时候也能暴露错误。

对“成功”结果表示怀疑，因为有些规范中的错误会导致搜索状态意外减少。这可以通过-coverage num选项的输出或者添加额外的检查条件来排查。

更高效利用 TLC，例如分拆不变量，使用Print打印变量的变化，将出错的状态设置为初始状态、Next公式从而快速出错。

出错后不要急着从头开始。先使用上一条中提到的“快速出错”确保错误已经被修复。另外由于存盘点只保存G和U，如果修正错误后的规范没有改变变量名，可以复用之前的存盘点。

尽量多检查各种性质。

TLC 的目的是检查错误，因此为了绕过 TLC 的限制可以使用替换等方式调整规范。比如对于Nat等无限大小的集合使用0..n代替。

使用ASSUME快速计算 TLA+ 中简单公式的值。

14.6 TLC 不能做什么

TLC 的限制还包括：Naturals和Integers模块的 Java 实现实际上只能处理 -2^63 到 2^63 - 1 之间的值。

TLC 的部分语义也与 TLA+ 不同。包括：TLC 的CHOOSE运算符只保证对句法上相同的集合选出相同的元素，因此不保证{1, 2}与{2, 1}选出相同的元素；字符串是基本数据类型而不是函数，因此取下标会报错。

14.7 更精确的表述

14.7.1 配置文件的语法

配置文件的语法可以用 BNF 表示，详见原书。除此之外，INIT、NEXT定义只能有一次，SPECIFICATION定义只能出现一次且不能与INIT、NEXT同时出现。VIEW和SYMMETRY定义同样只能出现一次。除此以外的段都能定义多次。

14.7.2 可比较的 TLC 值

满足如下规则的值是可比较的：

  • 对于基本数据类型，如果类型相同就可比较

  • 模型值总是可比较的，因为它仅与自己相等

  • 集合的可比较定义为大小不同，或者大小相同且元素两两可比较

  • 函数的可比较仅当定义域可比较，或者定义域相同且相同的x对应的值可比较