Skip to content

Latest commit

 

History

History
9 lines (6 loc) · 346 Bytes

README.md

File metadata and controls

9 lines (6 loc) · 346 Bytes

TLA-Practice

Chap 1-4.

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