TLA+的本质和速成法

TLA+在系统架构高可用性验证中，由于其轻量级带来的高性价比被越来越多架构师接受，为了让大家尽快上手，本文尝试总结下TLA+建模的方法。

了解事物

了解任何一件新事物，都要从两个方面着手：

– 规律，即它同其他事物相似点

– 本质，即它同其他事物不同点

这两点都可以最大限度利用大脑中已有相关知识。掌握规律，就可以最大限度嫁接到已有知识，从而抬高了学习的起点；掌握了本质，就容易跟已有知识做对比，人脑最喜欢最对比，有了对比就很容易记住。从而就很容易了解这个新事物。

TLA+的本质是啥呢？站在系统视角看，就是用状态的变化表现行为

视角

视角非常重要，用户视角，即是代入用户角色看待和系统的交互。系统视角，站在系统上，观察系统状态。

状态

状态是一个动态概念（大前提是我们建模是基于离散模型的）， 是指系统属性的离散化、符号化表达。

系统初始态或运行时，假设拿来一个时间停止器，按一下停止开关，系统凝固住（不是停止，停止时系统属性会reset），这时看到系统属性集合就是系统所有随时间变化的状态空间中的一种。

行为

行为指外部一个动作作用到系统上，并且系统能够感知到。所谓感知到就是指系统状态发生了变化。

如果行为作用到系统上，系统状态没有发生变化，我们认为这个行为对系统来说不存在。

站在系统内视角看，状态发生了变化，即意味着系统接受到了外部行为的激励。

有了这个认识，TLA+建模就变得极其简单了，先找到业务行为，再看看这些业务行为用什么样的数据结构值的变化来表达，模型就建完了。

比如某个系统中有个用户注册的行为，这个所谓注册行为，其实就是已注册用户数据结构（registeredUsers）中增加一个新注册用户的ID，可以推导出registeredUsers为集合（无序、消重）。如果考虑用户注册先后顺序，也可以使用列表（有序，可重复），注意消重。

例如原来registeredUsers值{u1，u2}，用户u3注册行为结束后registeredUsers值变成{u1,u2,u3}。

上述思路为了方便大家实践，总结了“4看”建模法，供大家参考。

看边界

只要是模型，一定要考虑层次和边界，只有保持在同一层次上讨论问题，模型才能足够的清晰，才不会一下子陷入细节之中，也不容易引起混乱；另外也很容易控制住模型复杂度，请记住对于复杂问题，分而治之常常是搞定它的不二法门，一定要做到左右模块、上下分层。所以建模第一步就是分层分模块。

我们一般通过通信机制来作为分层分模块的起点，理清系统通信两个问题：

1、通信结构：master-slave、p2p或者两者结合。

2、通信方式：同步、异步、pubsub

比如我们对一个资源管理系统建模，客户端和服务器采用主从方式通信；客户端和服务端通信可以是同步或异步，但是同步会导致两者之间耦合过于紧密，加之资源申请和资源分配耦合到一起了，并且有性能瓶颈，我们这里考虑采用异步方式。

我们可以按通讯机制把系统分成了两层，内层就是服务端，外层是客户端，两者之间是消息通道。

我们的系统边界应该从内层服务端入手，完成服务端模型后再叠加客户端模型和通信机从而制形成完整系统模型。

如果建模一上来包含了客户端和服务端，无疑还要考虑两者之间的通讯机制（可能是消息队列、消息重复、消息丢失、消息乱序等），就比较复杂。

TLA+提供instance关键字提供模型组合能力，可以由服务端出发，演进式叠加消息通道、客户端组形成整个系统模型。

看行为

确定好模型层次以后，接下来就是根据主要业务功能找出业务行为，还以资源管理为例，确定只考虑服务端后，就可以转换下视角，从服务端的角度来看（站在服务端上看服务端边界上的行为）行为，主要业务行为应该为：

– 资源申请（request）

– 资源分配（allocate）

– 资源释放（return）

等业务功能，注意要保持业务行为在同一层次上。比如资源分配中获取空余资源这个行为就属于细粒度层次，它和资源申请就不在同一个层次上。

服务端是个异步系统，它的业务行为是随机产生。如下图

看状态

行为就是状态变化。这一步很关键，有了行为，就可以找到行为会引起哪些状态的变化。比如request对对应一个叫做未满足资源的状态unsat( unsatisfiedRes)的变化，unsat数据结构可以考虑采用map，key是客户id，值是未分配资源的集合；同理allocate对应同样的数据结构alloc。所有资源行为结果都是对这两个map组成的状态进行操作。见图（注意行为导致的状态变化，另外，某个行为也不一定导致状态中所有值变化，至少一个变化即可。）

服务端收到了客户端c1申请资源集合{r1}请求，就是把未满足unsat里面增加一个c1申请的资源集合{r1};

服务端给客户端c1分配了资源{r1}，就是把已分配alloc中增加一个c1申请的资源集合{r1};

服务端收到了客户端c1释放已分配资源{r1}的请求，就是把已分配alloc中c1的资源中减去{r1}。

看状态

针对上一步骤“看状态”，状态中的数据结构就非常重要，好的数据结构可以起到事半功倍的效果。比如这个资源申请，使用map中套set的数据结构就比较合理，因为业务行为中，最多的就是根据客户id调整资源。

比如汉诺塔的例子中，主要对三个塔的不同的砖进行转移，这样采用数组套数组的数据结构比较容易根据下标操作砖的移动。

汉诺塔移动之前，数据结构值应该是<< <<1,2,3>>,<<>>,<<>> >>，

汉诺塔移动完成后，数据结构的值应该是<< <<>>,<<>>,<<1,2,3>> >>，其中<< >> 表示数组

同理，TLA+模型验证的invariant和properties也可以通过状态表达出来。

综上，TLA+建模关键是用状态变化表示行为-》找到行为-》找到状态-》仔细考量状态的数据结构，建模大功告成。