TLA+ 语法全解

TLA+ 作为图灵奖得主、paxos 算法发明者 lamport 创造的语言，可谓掌握了“流量密码”，在它的应用领域大展身手。如果开发了一个新的分布式协议、验证一个复杂状态的算法，配上一个 TLA+ 的证明，就能大大增加算法的可信度。

可这么好的东西竟然没有一个系统的语法讲解，作为一个学习者，粗浅的使用难以满足我对其全貌的好奇。邃开发了 atlc(Another TLC)，一个 TLA+ 的解释器，借此深入其细节。