TLA+ 是什么？

TLA+ 是一种用来精确描述任意离散系统行为的数学语言，它是由 Leslie Lamport 发明的。 能够让 TLA+ 实用化的是 TLC，它是由 Yuan Yu 开发实现的。

如果想要学习 TLA+，那么我建议从下面给出的资料中，按照次序依次地阅读：

TLA+ 解决了什么问题？它有什么用？

通常我们做系统设计时，会有一份设计文档。这个设计文档通常是用文字和图表来描述的， 它的描述是模糊而不精确的，它里面是否有错误只能通过人来举出一些反例来说明（虽然也 可以通过证明的方法来找出错误，但是证明所耗的时间太多了），但是通常一个系统的状态 空间太大，人不可能想到系统的所有行为，那么也就找不出错误来了。这种系统通常只能在 实现、测试或者上线之后，才发现系统的错误，这个时候才发现设计上的错误，代价就太 大了。

TLA+ 要解决的问题就是在设计初期就能找出设计上的错误。

TLA+ 在工业界的大型分布式系统中有一些应用，从公开的资料来看，包括 MicroSoft， Amazon，Intel 都使用过 TLA+ 来描述过一些大型系统的行为，使用 TLC 来检查设计上是 否存在错误。Paxos、Raft 这样的工业级分布式容错一致性算法，也使用了 TLA+ 进行描述， 也通过TLC 来进行检查，最后还使用了 TLAPS 进行证明。

TLA+ 的原理是怎样的？

TLA+ 是建立在 TLA 之上的。TLA(Temporal Logical of Action)是“行为时序逻辑”，理 论上可以描述任意一个离散系统的行为。TLA 假定底下有一个可以依赖的普通数学基础， Lamport 发现不需要引入编程语言的结构，但是为了能够编写大型的规范，最后只引入了两 种技术：定义（definition）和模块化（module）。我们通常使用一种工具来检查规范是否 包含错误，这样的工具是 TLC。

现实世界中的系统，会有多种抽象，每种抽象又会有多种可以描述它的模型。TLA+ 选择了 一种基于状态的模型来描述一种抽象。这个模型包含了三种要素：状态（state）,步骤 （step），行为（behavior）。

state 是对所有变量的一次赋值，单从系统的角度来看，它只能观察到系统本身的变量。

step 是一个状态对（s, t），这个状态对满足了一种动作（action）。

action 是一个有真假值的公式，这个公式包含了变量的旧值和新植，将 s 代入 action 中 作为一个变量的旧值，将 t 代入 action 中作为一个变量的新植，然后就可以对 action 求值，在 TLC 中则是将旧值代入，令公式为真，然后求得新值 t。

behavior 是无限的状态序列。系统终止的行为可以表现为一个不变的状态重复无限多，系 统不停地运行则表现为状态的不断变迁。由于一个行为的状态可以有无限多，所以可以对它 做出一些断言。例如，“某个特性在行为的所有状态上求值都是真”,“某个状态在某个行 为中一定会出现”等等。由于状态是无限多的，而且系统只能观察到自身的变量的状态，而 不是系统内部行为，是不会影响到系统的状态变迁的，所以行为中需要能够出现不变的状态， 两个不变状态之间，是由不变步骤（Stuttering Step）得到的，所以 TLA+ 不允许写出没 有不变步骤的行为。

TLA+ 还允许表达“系统中某个特性在所有的行为中都是成立的”这样的断言，这种断言叫 做 safety，它的意思是某个特性（一个对行为可以求值为真假的公式）在行为的每一个状 态上都是成立的。除了 safety，TLA+ 还允许表达“系统中某个特性在满足特定的条件后一 定会出现”，这叫做 liveness，它的意思是某个特性（也是一个对行为可以求值为真假的 公式）在一个行为的一个状态出现之后，另一个状态必定出现。

使用 TLA+ 来精确地描述系统行为，就叫做系统的规范，它还支持检查一个规范是否能够实 现另外一个规范。一个低层次的规范含有更多的细节，使用“refinement mapping”来对低 层次的规范中的变量进行转换，可以使用 TLC 来检查是否满足高层次（更少细节）的规范。 从一个行为中的状态来看，“refinement mapping”主要做的事情是将低层次的状态中的变 量进行替换，使之产生一个替换后的行为，然后再看看这个行为是否满足够层次的规范。例 如，低层次规范一个行为某些状态为 a->b1->b2，需要替换为高层次规范的某些行为 a->b2， 这时需要将 b1 通过变换得到 b2，也就是状态变为 a->b2->b2，这里也从另外一面可以看 到允许不变步骤的必要性。

一开始学习时，发现“=>”（蕴涵，或者叫做推断）很难理解，我自己用这样的例子来理解 是比较容易接受的：对于公式“Spec => DeadlockFree”，它断言“满足系统的行为，也满 足 DeadlockFree 这种特性”，那么不满足系统的一个行为（公园中一只小狗在跑步），不 应该影响到 DeadlockFree 作为系统特性是否成立。

关于 TLA+ 没有得到应有重视的思考

TLA+ 的学习路径是非常陡峭的，它和一个菜鸟刚接触编程时所要经历的学习路径是相似的。 相对于程序员来说，TLA+ 是和编程语言完全不同的一门数学语言，它的思维方式和编程语 言的思维方式是不同的：TLA+ 是以状态为基础的，而编程语言是以程序执行路径为基础的。

TLA+ 要重新掌握的符号和概念都是非常多的，但是相对于编程语言来说，算是比较少的。 抛开 Weak Fairness，要掌握它所出现的符号和基本概念，还有 TLC 的使用，时间是以月 为单位的。

最重要的原因是，它在实际的工作中不是必须要求掌握的。

TLA+ 的不流行和数学的不流行有一定的关系，那么数学本身一定是有它自己的原因，才会 导致它不流行。个人觉得数学中的一些概念，不能以现实世界中的例子来理解，这本身就是 因为一些数学概念本身就是“不可理解”的，而不可理解的东西，不能在平常用到的话，会 很容易忘掉的。

TLA+ 的学习资源

作为一个备忘，将我自己学习过的资源放在这里：

TLA+ 社区：

本人 TLA+ 的学习路径

最初我是从学习 Paxos/Raft 时开始接触 TLA+。让我产生学习 TLA+ 的兴趣和动力是想读 懂 Paxos/Raft 的 TLA+ 描述和看懂它们的证明，而坚定我学习 TLA+ 是看到了 Use of Formal Methods at Amazon Web Services 这篇文章。

我从 SpecifySystem 开始学习，看到了第 4 章看不下去了，然后转向 learntla.com 进行学习。之后，将 hyperbook 除了证明相关 的章节外，都完整地看过一遍。接下来看了 SpecifySystem 中的前 7 章，加上第 8 章（Liveness）、第 11 章（Adavance Example）和 TLC 一节的原理和使用。 最后，再将 hyperbook 中的 Alternation 和 Concurrent 两章仔细地看完。 至此，我自己才敢说掌握了 TLA+/PlusCal 的使用，能够看懂一些 Spec 了。

而现在我仍然需要掌握的知识包括：

  • TLAPS 的使用
  • 对模型特性（Safety/Liveness）的证明