核心
This is the core language material. You can think of this section as a self-contained “book” that gets you from a complete outsider to a beginning practitioner. People who are already comfortable with TLA+ may find the topics more useful. 这一部分是语言的核心资料。可以认为这一部分是新人指南。主题部分对TLA+老手更有价值。
Outline - 大纲
As a very rough guide, here’s the order we’ll learn things: 粗略来说，学习顺序如下：
How to do basic operations, like adding two numbers or concatting two sequences. 如何完成一个基本操作，例如简单对两个数求和，或拼接两个序列。
How to specify simple, deterministic, nonconcurrent algorithms, like “check if this list has any duplicates in it”, and how to check if invariants hold. 如何定义简单的、确定的、非并发的算法，例如“检查列表中是否有重复元素”，以及如何检查不变量是否成立。
Specifying nondeterministic algorithms, like ones involving randomness or a chance of failure. 定义不确定的算法，例如包含随机数或有概率失败的算法。
Specifying concurrent systems, like independent readers and writers sharing a queue. 定义并发系统，例如针对一个队列的随机共享读写。
Specifying temporal properties, or properties on the entire lifetime on the system, like “eventually all servers come online”. 定义时序属性，或系统全生命周期的属性，例如“最终所有的服务都会上线”。
Writing TLA+-first specifications. 写TLA+优先规约。
Everything up to and including “temporal properties” is necessary to fully use TLA+. Everything after that adds further power. 截止“时序属性”的所有内容都是充分使用TLA+的必要条件。其后的每一部分内容都属于是功能增强。
Notes on the Material - 注意事项
Examples - 例子
Right now the guide is pretty light on examples. More interesting examples are in the examples section. 目前这个指南的例子蛮少的。更多更有意思的例子在示例模块。
PlusCal vs TLA+
There are two languages that people write TLA+ in practice. First, you can do everything in TLA+ (“pure TLA+”). Second, you can treat it as an “assembly language” of sorts, and write most of your basic logic in TLA+ but handle all the state transitions in a DSL. There’s an official DSL for this called “PlusCal”, which is what we’ll be starting with. I prefer doing things this way for two reasons: 在实践中，开发者使用两种语言写TLA+。首先，纯TLA+可以做任何事。其次，你可以把TLA+当作某类“汇编语言”，使用TLA+写基本逻辑，然后使用一个DSL处理所有的状态转换。官方提供的DSL叫做“PlusCal”，这将是我们梦开始的地方。我推荐使用后者进行实践，这里有两个原因：
Specification is an extremely dense, interconnected topic. By teaching PlusCal first, I can teach some aspects of the topic in an isolated, useful way, and gradually introduce other on top of that. This reduces the cognitive load. By contrast, if you learn pure TLA+ first, you have to learn everything all at once to get anything done. 规约是一个极度密集的、相互联通的主题。通过上来就教PlusCal，我可以使用一种孤立的、实用的方式来讲述规约的一些方面（话题），随后在此基础上逐渐介绍其余内容。这为学习者降低了认知负担。不然的话，如果我一开始就讲TLA+，你就必须把所有的知识都学全了，才能开始投入实践。
Once you know PlusCal, it is extremely easy to learn pure TLA+. I’ll be able to cover all of the “new stuff” in a single chapter. 一旦你学会了PlusCal，再学习TLA+就非常容易了。我会在一个独立的章节中介绍“新的知识”。
That said, not everybody finds it easier to learn this way, and that’s fine. There are two TLA+-first resources available, both by the inventor of TLA+: 不过或许，并非所有人都能够适应我的教学方式，这也没问题。下面有两个起手就讲TLA+的资料，都是Lamport写的：
Specifying Systems: This is a comprehensive introduction to modeling systems in TLA+, though it’s a little lighter on how to check those specifications.
Video Course: I’ve not watched this so can’t speak to its quality, but some people I know really enjoy it.
See also Other Resources for a larger list of other learning material. 这里还有更多的学习资料。
Last updated