PlusCal-Examples:兰波特 TLA+ 的算法语言 PlusCal 中的算法示例

概述 这些是用 PlusCal 编写的算法示例，PlusCal 是 Leslie Lamport 的 TLA+ 算法规范系统的算法语言。 这些文件是在 TLA+ 工具箱中创建的，因此大多数文件都是在工具箱中运行和使用 TLC 算法验证检查器的支持文件。 用于审核的重要（非自动生成）文件是以.tla结尾的.tla ，例如Euclid/Euclid.tla和HourClock/HourClock.tla 。 我已经写了\* BEGIN TRANSLATION行上方的部分，PlusCal 代码位于(*和*)注释标记之间，从--algorithm XXX指示器开始。