前言

TLA+ in practice 学习笔记

前段时间看到一篇文章，是讲AMS使用TLV+来测试其开发的系统，文章中讲TLA+是一种容易学习和掌握的形式化语言。为此，我从网上找到了一本Practical TLA的书，阅读之后，还是有一些心得。

这本书，是一本使用TLS进行设计验证的入门书，TLA是很晦涩的，为了便于使用，作者又开发了一门基于TLS的DSL语言–PlusCal。PlusCal是一门具有函数式编程风格的描述语言，虽然对于C语言程序员而言仍然不容易掌握，但是相对于TLA来说已经是好了很多的了。

那么，这本书，按照作者的说法，希望对读者有两方面的帮助：

• 首先就是对模型进行检查。模型是对现实世界事物的一种理想化的抽象，在建模的过程中，会强迫设计者识别哪些是重要的概念，哪些是不重要的概念。在这本书中，时时刻刻体现了模型的概念。
• 其次，是