正文
前面对 TLA+ 有了一个大概的介绍，但我相信大家可能仍然是一头雾水，我们如何使用 TLA+ 去验证系统原型设计的正确性呢？我觉得我们可以先从一些简单的例子入手，然后再逐渐理解，最后再用 TLA+ 来验证我们自己的系统。
DieHard
第一个简单的例子就是 DieHard，不过我没看过这部电影。电影里面主角需要用一个 3 加仑的水壶和一个 5 加仑的水壶得到 4 加仑的水，怎么做呢？
当然，这个问题比较简单，大家可以在脑袋里面自行分析流程，这里我们通过 TLA+ 来得到结果。
首先我们定义两个变量，big 和 small，用来表示 5 和 3 加仑的水壶。定义是
VARIABLES big, small
。在前面我们介绍过，TLA+ 其实就是一个状态机，它有一个初始状态，然后就开始不停的迭代循环到下一个状态。
首先我们来看初始状态，也就是 big 和 small 都为 0，如下：
Init ==
/\ big = 0
/\ small = 0
然后我们再看 Next 状态，我们可以做如下事情：
-
给 3 加仑水壶灌满水
-
给 5 加仑水壶灌满水
-
清空 3 加仑水壶
-
清空 5 加仑水壶
-
将 3 加仑水壶的水倒到 5 加仑水壶
-
将 5 加仑水壶的水倒到 3 加仑水壶
对应的 TLA+ 为：
Next ==
\/ FillSmall
\/ FillBig
\/ EmptySmall
\/ EmptyBig
\/ SmallToBig
\/ BigToSmall
我们首先来看
FillSmall
，我们可以写
FillSmall == small' = 3
，但这样其实是不对的。因为这里我们并没有处理 big 的情况，在之前的文章里面我们说过，Next 表示的其实就是在当前状态下变量的值以及在下一个状态下这些变量的可能的值之间的关系，所以上面的语句我们只处理了 small，但 big 可能就是任意值了，实际上 big 的值是不变的，所以真正的
FillSmall
为：
FillSmall ==
/\ small' = 3
/\ big' = big
注意，这里在说明一下，TLA+ 里面会用
'
来表示下一个状态。
自然的
EmptySmall
为：
EmptySmall ==
/\ small' = 0
/\ big' = big
然后我们再来看看
SmallToBig
，它有几种情况：
-
small + big <= 5，那么我们就能将 small 的水全部倒到 big 里面
-
small + big > 5，我们只能从 small 这边倒 5 - big 的水
上面两种情况，其实都可以写成
Min(big + small, 5) - big
，首先我们定义
Min
：
Min(m, n) == IF m < n THEN m ELSE n
如果公式 m 小于 n 为 TRUE，那么就使用公式 m，否则就使用公式 n。
然后我们实现
SmallToBig
：
SmallToBig ==
LET poured == Min(big + small, 5) - big
IN
/\ big' = big + poured
/\ small' = small - poured
当然，我们可以很容易的写出其他的公式，详细可以参考
DieHard.tla
。
实现了
Init
和
Next
之后，下一步就是如何去验证了。我们要得到 4 加仑的水，所以如果我们发现，在某一个状态的时候，big 里面有 4 加仑的水，那么直接报错，TLA+ 会输出迭代到 4 加仑水这个状态时候所有的步骤，我们自然就能知道如何得到 4 加仑水了。所以我们先定义
NotSolved == big /= 4
，并加入到 TLC model 的 Invariants 里面，然后执行 model，会发现 TLC 会报错了。关于 TLA+ toolbox 的使用，大家可以自行下载尝试，后面有机会我也会在说明一下。
Transaction Commit
上面的 DieHard 只是一个比较简单的例子，我们下面来说说事务。说到事务，就不得不用结婚的例子来说明了。一个婚礼的大概流程如下：
-
神父对新郎说：『你准备好了吗？』
-
新郎回复：『准备好了。』
-
神父对新娘说：『你准备好了吗？』
-
新娘回复：『准备好了。』
-
神父对新郎新娘说：『恭喜你们。』
上面假设 2 和 4 的时候任意一方说『不愿意』，那么神父就会取消婚礼。所以对于一次婚礼来说，要不就是新郎新娘结为夫妇，要不就是散伙，绝对不会出现新郎认为结婚了，但新娘认为没结婚这样的状态，反之亦然。
对应到事务上面，新郎新娘就是 Resource Manager（RM），而神父就是 Transaction Manager（TM）。对于所有 RM，它们最终只可能是 committed，或者 aborted 状态，不可能一些是 committed，一些是 aborted。最开始 RM 是 working 状态，然后会变成 prepared 状态，当一个 RM 是 prepared 了，它就可能变成 committed 或者 aborted，RM 也可以直接从 working 变成 aborted。
这里，我们首先用 TLA+ 来描述下事务提交的规格，这里，我们只会关注 RM，而不会关注 TM，因为 TM 是用来执行事务的，也就是 How 的过程，而并不是 What。后面我们会实际的用 2 PC 再来讲解 How。
首先我们先定义常亮 RM，使用
CONSTANTS RM
，RM 是一个集合，在 TLC model 里面我们会给它赋值，譬如叫
{"r1", "r2", "r3"}
这种的。然后我们定义变量
VARIABLES rmState
用来表示 RM 的状态。
初始我们会将所有的 rmState 设置为 working，也就是
TCInit == rmState = [r \in RM |-> "working"]
。
对于任意一个 RM，它的 Next 可能是准备事务，也可能是觉得是否提交或者终止事务。所以 Next 定义为
TCNext == \E rm \in RM : Prepare(rm) \/ Decide(rm)
，这里我们注意下
\E rm \in RM : Prepare(rm) \/ Decide(rm)
，假设 RM 是
{"r1", "r2"}
，那么它就等价于
Prepare("r1") \/ Decide("r1") /\ Prepare("r2") \/ Decide("r2")
。
