⚡

TLA+规范技能Skill tla-specification

这个技能用于使用TLA+形式化规范语言设计和验证分布式系统和并发算法，支持精确设计、早期错误检测、模型检查和文档生成。关键词：TLA+、形式化验证、分布式系统、并发算法、模型检查、系统设计、安全属性、活性属性。

架构设计 0 次安装 0 次浏览 更新于 3/11/2026

名称: tla-规范 描述: TLA+ 分布式系统和并发算法的形式化规范语言 允许工具: 读取, 全局, 搜索, 写入, 编辑, mcp__perplexity__搜索

TLA+ 规范技能

何时使用此技能

使用此技能时：

  • TLA 规范任务 - 处理 TLA+ 分布式系统和并发算法的形式化规范语言
  • 规划或设计 - 需要 TLA 规范方法的指导
  • 最佳实践 - 希望遵循既定模式和标准

概述

TLA+ 形式化规范语言用于设计和验证分布式系统和并发算法。

强制要求：文档优先方法

在编写 TLA+ 规范之前：

  1. 调用 docs-management 技能 获取形式化方法模式
  2. 通过 MCP 服务器验证 TLA+ 语法（使用 perplexity 获取最新实践）
  3. 所有指导基于 Leslie Lamport 的 TLA+ 文档

为什么使用 TLA+？

TLA+ 支持：

  1. 精确设计：系统设计中的数学精度
  2. 早期错误检测：在编码前发现并发错误
  3. 模型检查：使用 TLC 进行详尽验证
  4. 文档：可执行的规范文档化意图
  5. 行业应用：被 Amazon（AWS）、Microsoft、MongoDB 等使用

TLA+ 结构

基本模块模板

--------------------------- MODULE OrderWorkflow ---------------------------
\* 订单工作流规范
\* 从创建到完成的订单生命周期模型

EXTENDS Integers, Sequences, FiniteSets, TLC

CONSTANTS
    MaxOrders,      \* 最大并发订单数
    MaxItems,       \* 每个订单的最大商品数
    Customers,      \* 客户 ID 集合
    Products        \* 商品 ID 集合

VARIABLES
    orders,         \* 从 OrderId 到订单状态的函数
    inventory,      \* 从 ProductId 到数量的函数
    payments,       \* 已处理支付记录集合
    notifications   \* 已发送通知序列

vars == <<orders, inventory, payments, notifications>>

-----------------------------------------------------------------------------
\* 类型定义
-----------------------------------------------------------------------------

OrderStatus == {"Draft", "Submitted", "Paid", "Shipped", "Delivered", "Cancelled"}

Order == [
    id: Nat,
    customerId: Customers,
    items: SUBSET (Products \X Nat),  \* (商品, 数量) 对的集合
    status: OrderStatus,
    total: Nat
]

TypeInvariant ==
    /\ orders \in [SUBSET Nat -> Order \cup {NULL}]
    /\ inventory \in [Products -> Nat]
    /\ payments \in SUBSET [orderId: Nat, amount: Nat, timestamp: Nat]
    /\ notifications \in Seq([type: STRING, orderId: Nat])

-----------------------------------------------------------------------------
\* 初始状态
-----------------------------------------------------------------------------

Init ==
    /\ orders = [o \in {} |-> NULL]
    /\ inventory = [p \in Products |-> 100]  \* 每个商品初始为 100
    /\ payments = {}
    /\ notifications = <<>>

-----------------------------------------------------------------------------
\* 动作
-----------------------------------------------------------------------------

\* 创建新草稿订单
CreateOrder(customerId, orderId) ==
    /\ orderId 
otin DOMAIN orders
    /\ Cardinality(DOMAIN orders) < MaxOrders
    /\ orders' = orders @@ (orderId :> [
           id |-> orderId,
           customerId |-> customerId,
           items |-> {},
           status |-> "Draft",
           total |-> 0
       ])
    /\ UNCHANGED <<inventory, payments, notifications>>

\* 向草稿订单添加商品
AddItem(orderId, productId, quantity) ==
    /\ orderId \in DOMAIN orders
    /\ orders[orderId].status = "Draft"
    /\ quantity > 0
    /\ quantity <= inventory[productId]
    /\ Cardinality(orders[orderId].items) < MaxItems
    /\ orders' = [orders EXCEPT
           ![orderId].items = @ \cup {<<productId, quantity>>},
           ![orderId].total = @ + (quantity * 10)]  \* 简化定价
    /\ UNCHANGED <<inventory, payments, notifications>>

\* 提交订单进行处理
SubmitOrder(orderId) ==
    /\ orderId \in DOMAIN orders
    /\ orders[orderId].status = "Draft"
    /\ orders[orderId].items /= {}
    \* 保留库存
    /\ \A <<p, q>> \in orders[orderId].items : inventory[p] >= q
    /\ orders' = [orders EXCEPT ![orderId].status = "Submitted"]
    /\ inventory' = [p \in Products |->
           inventory[p] - Sum({q : <<prod, q>> \in orders[orderId].items, prod = p})]
    /\ notifications' = Append(notifications,
           [type |-> "OrderSubmitted", orderId |-> orderId])
    /\ UNCHANGED <<payments>>

\* 处理支付
ProcessPayment(orderId, amount) ==
    /\ orderId \in DOMAIN orders
    /\ orders[orderId].status = "Submitted"
    /\ amount = orders[orderId].total
    /\ payments' = payments \cup {[orderId |-> orderId, amount |-> amount, timestamp |-> 0]}
    /\ orders' = [orders EXCEPT ![orderId].status = "Paid"]
    /\ notifications' = Append(notifications,
           [type |-> "PaymentReceived", orderId |-> orderId])
    /\ UNCHANGED <<inventory>>

\* 发货订单
ShipOrder(orderId) ==
    /\ orderId \in DOMAIN orders
    /\ orders[orderId].status = "Paid"
    /\ orders' = [orders EXCEPT ![orderId].status = "Shipped"]
    /\ notifications' = Append(notifications,
           [type |-> "OrderShipped", orderId |-> orderId])
    /\ UNCHANGED <<inventory, payments>>

\* 交付订单
DeliverOrder(orderId) ==
    /\ orderId \in DOMAIN orders
    /\ orders[orderId].status = "Shipped"
    /\ orders' = [orders EXCEPT ![orderId].status = "Delivered"]
    /\ notifications' = Append(notifications,
           [type |-> "OrderDelivered", orderId |-> orderId])
    /\ UNCHANGED <<inventory, payments>>

\* 取消订单（仅草稿或已提交）
CancelOrder(orderId) ==
    /\ orderId \in DOMAIN orders
    /\ orders[orderId].status \in {"Draft", "Submitted"}
    /\ orders' = [orders EXCEPT ![orderId].status = "Cancelled"]
    \* 如果已提交则返回库存
    /\ inventory' = IF orders[orderId].status = "Submitted"
                    THEN [p \in Products |->
                          inventory[p] + Sum({q : <<prod, q>> \in orders[orderId].items, prod = p})]
                    ELSE inventory
    /\ notifications' = Append(notifications,
           [type |-> "OrderCancelled", orderId |-> orderId])
    /\ UNCHANGED <<payments>>

-----------------------------------------------------------------------------
\* 下一状态关系
-----------------------------------------------------------------------------

Next ==
    \/ \E c \in Customers, o \in 1..MaxOrders : CreateOrder(c, o)
    \/ \E o \in DOMAIN orders, p \in Products, q \in 1..5 : AddItem(o, p, q)
    \/ \E o \in DOMAIN orders : SubmitOrder(o)
    \/ \E o \in DOMAIN orders : ProcessPayment(o, orders[o].total)
    \/ \E o \in DOMAIN orders : ShipOrder(o)
    \/ \E o \in DOMAIN orders : DeliverOrder(o)
    \/ \E o \in DOMAIN orders : CancelOrder(o)

Spec == Init /\ [][Next]_vars

-----------------------------------------------------------------------------
\* 安全性属性
-----------------------------------------------------------------------------

\* 库存非负
InventoryNonNegative ==
    \A p \in Products : inventory[p] >= 0

\* 订单状态转换有效
ValidStatusTransitions ==
    \A o \in DOMAIN orders :
        LET status == orders[o].status
        IN status \in OrderStatus

\* 支付仅用于已提交订单
PaymentOnlyForSubmitted ==
    \A p \in payments :
        p.orderId \in DOMAIN orders

\* 无重复支付
NoDoublePayment ==
    \A p1, p2 \in payments :
        p1.orderId = p2.orderId => p1 = p2

-----------------------------------------------------------------------------
\* 活性属性
-----------------------------------------------------------------------------

\* 每个已提交订单最终完成（交付或取消）
EventualCompletion ==
    \A o \in DOMAIN orders :
        orders[o].status = "Submitted" ~>
            orders[o].status \in {"Delivered", "Cancelled"}

\* 如果支付成功，订单最终发货
PaymentLeadsToShipment ==
    \A o \in DOMAIN orders :
        orders[o].status = "Paid" ~> orders[o].status = "Shipped"

-----------------------------------------------------------------------------
\* 辅助函数
-----------------------------------------------------------------------------

Sum(S) ==
    IF S = {} THEN 0
    ELSE LET x == CHOOSE x \in S : TRUE
         IN x + Sum(S \ {x})

NULL == CHOOSE n : n 
otin Order

=============================================================================

PlusCal

PlusCal 是一种编译到 TLA+ 的算法语言：

PlusCal 示例

--------------------------- MODULE DistributedLock ---------------------------
EXTENDS Integers, Sequences, TLC

CONSTANTS Nodes, NULL

(*--algorithm distributed_lock

variables
    lock = NULL,                    \* 当前锁持有者
    requests = [n \in Nodes |-> 0], \* 请求时间戳
    grants = [n \in Nodes |-> FALSE];

define
    \* 安全性：最多一个节点持有锁
    MutualExclusion ==
        \A n1, n2 \in Nodes :
            grants[n1] /\ grants[n2] => n1 = n2

    \* 活性：每个请求最终被授予
    EventuallyGranted ==
        \A n \in Nodes :
            requests[n] > 0 ~> grants[n]
end define;

fair process Node \in Nodes
variables
    myTimestamp = 0;
begin
    Request:
        myTimestamp := myTimestamp + 1;
        requests[self] := myTimestamp;

    WaitForLock:
        await lock = NULL \/ lock = self;
        lock := self;

    EnterCriticalSection:
        grants[self] := TRUE;
        \* 临界区工作在此

    ExitCriticalSection:
        grants[self] := FALSE;
        lock := NULL;
        goto Request;
end process;

end algorithm; *)

\* BEGIN TRANSLATION - 由 TLA+ 自动生成
\* ... TLA+ 翻译出现在这里 ...
\* END TRANSLATION

=============================================================================

PlusCal 构造

variables         - 全局变量声明
define            - 定义运算符/不变量
process           - 进程定义 (fair = 公平调度)
procedure         - 可重用过程
begin/end         - 进程体
await             - 等待条件
either/or         - 非确定性选择
while             - 循环
if/then/else      - 条件语句
goto              - 跳转到标签
call              - 过程调用
return            - 从过程返回
with              - 原子性与非确定性选择

常见模式

共识算法

--------------------------- MODULE SimpleConsensus ---------------------------
EXTENDS Integers, FiniteSets

CONSTANTS
    Nodes,      \* 参与者节点集合
    Values,     \* 可达成一致的可能值
    Quorum      \* 仲裁所需的最小节点数

VARIABLES
    proposed,   \* proposed[n] = 节点 n 提议的值
    accepted,   \* accepted[n] = 节点 n 接受的值
    decided     \* decided[n] = 最终决定值（或 NULL）

vars == <<proposed, accepted, decided>>

TypeOK ==
    /\ proposed \in [Nodes -> Values \cup {NULL}]
    /\ accepted \in [Nodes -> Values \cup {NULL}]
    /\ decided \in [Nodes -> Values \cup {NULL}]

Init ==
    /\ proposed = [n \in Nodes |-> NULL]
    /\ accepted = [n \in Nodes |-> NULL]
    /\ decided = [n \in Nodes |-> NULL]

\* 节点提议一个值
Propose(n, v) ==
    /\ proposed[n] = NULL
    /\ proposed' = [proposed EXCEPT ![n] = v]
    /\ UNCHANGED <<accepted, decided>>

\* 节点接受一个提议值
Accept(n, v) ==
    /\ \E m \in Nodes : proposed[m] = v
    /\ accepted[n] = NULL
    /\ accepted' = [accepted EXCEPT ![n] = v]
    /\ UNCHANGED <<proposed, decided>>

\* 如果达到仲裁，节点决定
Decide(n) ==
    /\ decided[n] = NULL
    /\ \E v \in Values :
        /\ Cardinality({m \in Nodes : accepted[m] = v}) >= Quorum
        /\ decided' = [decided EXCEPT ![n] = v]
    /\ UNCHANGED <<proposed, accepted>>

Next ==
    \/ \E n \in Nodes, v \in Values : Propose(n, v)
    \/ \E n \in Nodes, v \in Values : Accept(n, v)
    \/ \E n \in Nodes : Decide(n)

Spec == Init /\ [][Next]_vars

\* 安全性：协议 - 所有决定值相同
Agreement ==
    \A n1, n2 \in Nodes :
        decided[n1] /= NULL /\ decided[n2] /= NULL =>
            decided[n1] = decided[n2]

\* 安全性：有效性 - 决定值曾被提议
Validity ==
    \A n \in Nodes :
        decided[n] /= NULL =>
            \E m \in Nodes : proposed[m] = decided[n]

=============================================================================

两阶段提交

--------------------------- MODULE TwoPhaseCommit ---------------------------
EXTENDS Integers, FiniteSets

CONSTANTS
    Coordinators,
    Participants

VARIABLES
    coordState,     \* 协调者状态
    partState,      \* 参与者状态
    prepared,       \* 已准备参与者集合
    decision        \* 最终决定

vars == <<coordState, partState, prepared, decision>>

CoordStates == {"init", "waiting", "committed", "aborted"}
PartStates == {"working", "prepared", "committed", "aborted"}

TypeOK ==
    /\ coordState \in CoordStates
    /\ partState \in [Participants -> PartStates]
    /\ prepared \in SUBSET Participants
    /\ decision \in {"pending", "commit", "abort"}

Init ==
    /\ coordState = "init"
    /\ partState = [p \in Participants |-> "working"]
    /\ prepared = {}
    /\ decision = "pending"

\* 协调者发送准备请求
SendPrepare ==
    /\ coordState = "init"
    /\ coordState' = "waiting"
    /\ UNCHANGED <<partState, prepared, decision>>

\* 参与者准备（投票是）
Prepare(p) ==
    /\ partState[p] = "working"
    /\ partState' = [partState EXCEPT ![p] = "prepared"]
    /\ prepared' = prepared \cup {p}
    /\ UNCHANGED <<coordState, decision>>

\* 参与者中止（投票否）
Abort(p) ==
    /\ partState[p] = "working"
    /\ partState' = [partState EXCEPT ![p] = "aborted"]
    /\ UNCHANGED <<coordState, prepared, decision>>

\* 协调者决定提交（所有已准备）
DecideCommit ==
    /\ coordState = "waiting"
    /\ prepared = Participants
    /\ coordState' = "committed"
    /\ decision' = "commit"
    /\ partState' = [p \in Participants |-> "committed"]
    /\ UNCHANGED <<prepared>>

\* 协调者决定中止（任何中止）
DecideAbort ==
    /\ coordState = "waiting"
    /\ \E p \in Participants : partState[p] = "aborted"
    /\ coordState' = "aborted"
    /\ decision' = "abort"
    /\ partState' = [p \in Participants |->
           IF partState[p] = "prepared" THEN "aborted" ELSE partState[p]]
    /\ UNCHANGED <<prepared>>

Next ==
    \/ SendPrepare
    \/ \E p \in Participants : Prepare(p)
    \/ \E p \in Participants : Abort(p)
    \/ DecideCommit
    \/ DecideAbort

Spec == Init /\ [][Next]_vars

\* 安全性：原子性 - 所有参与者达成相同决定
Atomicity ==
    decision /= "pending" =>
        \A p \in Participants :
            (decision = "commit" => partState[p] = "committed") /\
            (decision = "abort" => partState[p] \in {"aborted", "working"})

=============================================================================

TLC 模型检查

配置文件 (.cfg)

SPECIFICATION Spec

\* 常量
CONSTANTS
    Nodes = {n1, n2, n3}
    Values = {v1, v2}
    Quorum = 2
    NULL = NULL

\* 要检查的不变量
INVARIANT TypeOK
INVARIANT Agreement
INVARIANT Validity

\* 活性属性
PROPERTY EventuallyDecided

\* 有界模型检查的约束
CONSTRAINT StateConstraint

\* 对称性优化
SYMMETRY Symmetry

运行 TLC

# 命令行 TLC
java -jar tla2tools.jar -config Spec.cfg Spec.tla

# 使用工作器并行
java -jar tla2tools.jar -workers 4 -config Spec.cfg Spec.tla

# 错误时生成跟踪
java -jar tla2tools.jar -dump dot,colorize states.dot Spec.tla

时态运算符

[]P          - 总是 P（不变量）
<>P          - 最终 P
P ~> Q       - P 导致 Q（如果 P 则最终 Q）
[]<>P        - 无限经常 P
<>[]P        - 最终总是 P
P /\ Q       - P 且 Q
P \/ Q       - P 或 Q
~P           - 非 P
P => Q       - P 蕴含 Q
ENABLED A    - 动作 A 已启用
[A]_v        - A 或 v 未改变
<<A>>_v      - A 且 v 改变
WF_v(A)      - 弱公平性
SF_v(A)      - 强公平性

与 C# 集成

// 规范驱动设计：实现以匹配 TLA+ 规范

public enum OrderStatus
{
    Draft,
    Submitted,
    Paid,
    Shipped,
    Delivered,
    Cancelled
}

// 匹配 TLA+ 转换的状态机
public sealed class Order
{
    private static readonly Dictionary<(OrderStatus From, string Action), OrderStatus> _transitions = new()
    {
        // 匹配 TLA+ SubmitOrder 动作
        { (OrderStatus.Draft, "Submit"), OrderStatus.Submitted },
        // 匹配 TLA+ ProcessPayment 动作
        { (OrderStatus.Submitted, "Pay"), OrderStatus.Paid },
        // 匹配 TLA+ ShipOrder 动作
        { (OrderStatus.Paid, "Ship"), OrderStatus.Shipped },
        // 匹配 TLA+ DeliverOrder 动作
        { (OrderStatus.Shipped, "Deliver"), OrderStatus.Delivered },
        // 匹配 TLA+ CancelOrder 动作
        { (OrderStatus.Draft, "Cancel"), OrderStatus.Cancelled },
        { (OrderStatus.Submitted, "Cancel"), OrderStatus.Cancelled },
    };

    public OrderStatus Status { get; private set; } = OrderStatus.Draft;

    public Result Transition(string action)
    {
        if (!_transitions.TryGetValue((Status, action), out var newStatus))
            return Result.Failure($"无效转换: {Status} -> {action}");

        Status = newStatus;
        return Result.Success();
    }
}

// 测试中的不变量检查（匹配 TLA+ 安全性属性）
public class OrderInvariantTests
{
    [Fact]
    public void InventoryNonNegative_IsAlwaysTrue()
    {
        // 模拟 TLA+ 模型检查 InventoryNonNegative
        var inventory = new Dictionary<string, int>();
        // ... 运行状态空间
        Assert.All(inventory.Values, qty => Assert.True(qty >= 0));
    }
}

工作流

创建 TLA+ 规范时：

  1. 识别状态：什么变量定义系统状态？
  2. 定义类型：每个变量的有效值是什么？
  3. 指定初始：初始状态是什么？
  4. 定义动作：可能的状态转换是什么？
  5. 编写不变量：什么必须总是为真（安全性）？
  6. 编写活性：什么必须最终发生？
  7. 模型检查：运行 TLC 验证属性
  8. 细化：添加细节或修复发现的错误

最佳实践

  1. 从简单开始：从最小规范开始，逐步增加复杂性
  2. 先检查类型：TypeOK 应在复杂属性前通过
  3. 使用常量：参数化以便轻松调整模型大小
  4. 添加约束：限制状态空间以便可检查
  5. 对称性：利用对称性减少状态空间
  6. 跟踪错误：使用 TLC 跟踪理解失败
  7. 文档化意图：注释解释为什么，而不是什么

参考文献

详细指导：

最后更新： 2025-12-26