关于教程

这本教程重点介绍以最低要求就能让你启动，运行以及改进你的模型。虽然这种方法将略过一些TLA+的内容，以便使我们更容易学习各个简单的模块，但这并不意味着其他部分无聊，困难或没什么用。远非如此，只是它们超出了本教程的内容范围。

假设你具有以下背景：

• 你是一位经验丰富的程序员。这本教程不是教授如何去编程，并且TLA+也不是一个用户友好的工具。
• 你熟悉测试。如果你之前没有使用过单元测试，那么对你来说学习测试比学习TLA+更有用。
• 你知道一些数学。 TLA+大量借鉴数学结构和语法。假如你听说过德·摩根定理，知道什么是集合，并且能够理解什么(P => Q) => (~Q => ~P)是什么意思就更好了。否则，虽然你仍然可以学习TLA+，但可能不太直观。

你需要下载TLA+ Toolbox，并且确保你还能获取以下资源:

• PlusCal手册：PlusCal是TLA+的算法接口。虽然我们将在本指南中介绍它的所有内容，但是有一个完整的语法参考还是很好的。
• TLA + Cheat Sheet：这里包括本教程范围之外的TLA+语法。
• Specifying Systems：Specifying Systems是由TLA+的发明者Leslie Lamport编写的，目前仍然是关于TLA+的最全面的一本书。