书写并检验TPaxos的Liveness性质

[hengxin]

借鉴 Lamport 已有的 TLA+ Spec for Paxos, 书写并检验 TPaxos 的 Livensss 性质。

在此过程中，更深入理解 Safety, Liveness, Fairness。

[Starydark]

和Basic Paxos相同，TPaxos的liveness性质也需要single-leader来保证，不然也会出现两个参与者互相竞争发起提议而破坏liveness性质的情况发生。在此基础上，新加了LSpec时序公式用于检测TPaxos的活性，目前已经测试并通过了(2, 2, 3)、(2, 4, 4)这些规模的模型。