TLA-Practice

Chap 1-4.

• 初步了解TLA语法，编写简单的specification，理解$Spec\triangleq Init\and\Box[Next]_{vars}$ 的含义；
• 使用TLC进行模型检验，检验deadlock，invariant，termination；
• 了解PlusCal语法，PlusCal到TLA的转换；
• TODO：了解TLAPS的使用，invariance的结构化证明方法。