TLA+的本质和速成法

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

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

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>> >>，其中<< >> 表示数组。