论文标题
使用TLA+ Trifecta：TLC，Apalache和TLAPS进行规范和验证
Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS
论文作者
论文摘要
使用SAFRA引起的算法作为分布式终止检测作为运行示例，我们提供了用于验证用TLA+编写规范的主要工具。研究他们的互补优势和劣势，我们提出了一个支持不同类型分析的工作流程，并且可以适应所需的信心程度。
Using an algorithm due to Safra for distributed termination detection as a running example, we present the main tools for verifying specifications written in TLA+. Examining their complementary strengths and weaknesses, we suggest a workflow that supports different types of analysis and that can be adapted to the desired degree of confidence.
