- 初步了解TLA语法,编写简单的specification,理解$Spec\triangleq Init\and\Box[Next]_{vars}$ 的含义;
- 使用TLC进行模型检验,检验deadlock,invariant,termination;
- 了解PlusCal语法,PlusCal到TLA的转换;
- TODO:了解TLAPS的使用,invariance的结构化证明方法。
runze-wu / tlapractice Goto Github PK
View Code? Open in Web Editor NEWTLA+
Home Page: https://lamport.azurewebsites.net/tla/tla.html