主要观点：

• 介绍了系统中的活性（liveness）和安全性（safety）问题，以电梯系统为例进行说明。
• 通过 TLA+ 语言构建电梯系统模型，包括变量定义、动作规范等。
• 探讨了如何避免电梯 stuck 状态（活性条件），提出使用弱公平性（weak fairness）和强公平性（strong fairness）来确保电梯系统的活性。
• 强调在添加活性属性时要将安全性和活性性分开，避免无意添加新的安全性约束。

关键信息：

• 活性属性是断言某好事最终会发生，如电梯灯从红变绿；安全性属性是断言某坏事永不发生，如南北和东西交通灯不同时为绿。
• TLA+ 模型中电梯系统有变量 i（表示电梯位置）和 dir（表示电梯移动方向），定义了四种动作（UpFlr、UpBetween、DnFlr、DnBetween）。
• 避免电梯 stuck 需添加约束，直接添加不随意的时态属性可能会添加新的安全性约束，应使用公平性属性来确保活性。
• 弱公平性指若动作 A 永远可用，则最终会有 A 步；强公平性类似弱公平性，但适用于系统进出某状态的情况。
• 要保证电梯最终访问每一层，需分别为每个楼层添加强公平性条件，仅对 UpFlr 和 DnFlr 动作添加强公平性不能保证。

重要细节：

• 以 3 层楼为例说明 i 与楼层的对应关系，奇数时电梯在楼层，偶数时在两楼层之间。
• 在 TLC 模型检查中，可通过指定属性来检查电梯系统的各种性质，如 DoesntGetsStuckBetweenFloors 表示电梯不会永远 stuck 在两楼层之间。
• 给出了不同情况下的反例，如电梯 stuck 在两楼层之间、在 1 和 2 楼层间循环、到达顶楼后停留等，通过添加不同的公平性条件来修正。
• 推荐 Hillel Wayne 的博客和 Leslie Lamport 的书以获取更多 TLA+ 相关知识，还可参考 Andrew Helwer 的 MultiCarElevator 示例了解更真实的电梯模型。