验证设计租约 是做什么的？
crates/server/tla/DesignLeases.tla 是一个 TLA+ 模型，模拟两个共享同一个存储的 Finite 服务器，以及一个在这两个服务器之间转移的设计。TLC（TLA+ 模型检查器）会在小范围内尝试所有可能的步骤顺序，并检查两条规则：
- StoredEditsStay（ fencing 防护层）：一旦存储接受了编辑，任何其他服务器上的陈旧副本都无法覆盖它。如果这条规则被违反，一个停滞的服务器唤醒后会抹掉新所有者保存的编辑。
- AckedEditsStay：一个 MCP 工具报告为已完成的编辑，要么在存储中，要么在仍然可以保存它的副本中，除非在其服务器崩溃或其租约在编辑保存前已过期。如果这条规则被违反，代理被告知其编辑成功，但随后编辑丢失了。查看者会看到它消失，而且没有任何东西通知代理。
当前代码通过了第一条规则，但以四种已知方式违反了第二条规则。它们列在下面的“已知发现”中。
你的变更涉及这些吗？
是的，如果它改变了此表中的任何函数。每个模型步骤都代表它所对应的代码，审阅者可以同时打开两者进行比对。
| 模型步骤 | 代码 |
|---|---|
CallStarts, CallFindsHandle, CallLoads, CallEdits, CallReads | mcp/mod.rs design, edit_checked; api.rs open; hub/mod.rs Hub::open, handle_for; hub/design.rs DesignHandle::load, edit |
SaveTakes, SaveWrites, SaveFenced, SaveFails, SaveReleases, SaveDrops | hub/mod.rs persist; hub/design.rs take_save, save_failed |
Unload | hub/mod.rs Hub::sweep; hub/design.rs unload_if_idle, is_idle |
TickRenews … TickDiscovers | hub/mod.rs Hub::tick, let_go, remove, drop_copy, discover, summaries; hub/design.rs retire, end, lease |
Owns, LeaseLapses, HeartbeatExpires | cluster.rs Members::now, lapsed, renewed, Cluster::owns, owner |
CanClaim, Claimed, store writes | postgres/mod.rs claim, save, append, release, held; store.rs trait Store (内存共享存储必须匹配) |
Start, Crash | hub/mod.rs Hub::shared |
路径均位于 crates/server/src/ 下。
同步提交：6606714。 这是模型最后一次针对此代码进行检查的提交。要查看此后所覆盖代码中发生了什么变化，请运行：
git diff 6606714 -- crates/server/src/hub crates/server/src/mcp/mod.rs crates/server/src/api.rs crates/server/src/cluster.rs crates/server/src/postgres/mod.rs crates/server/src/store.rs
如果 diff 涉及表中的函数，在您确信变更可以通过测试之前，请重新阅读其旁边的模型步骤。仅当您已确认每个更改后的步骤仍与新提交的代码匹配时，才在此文件中向前移动同步提交指针。
运行
crates/server/tla/check.sh # 日常检查，约 2 分钟
crates/server/tla/check.sh --full # 增加 Finding4.cfg 和 AllFixes.cfg，再额外约 3 分钟
该脚本首次运行时会将 TLC（tla2tools.jar v1.7.4，已校验 SHA-256）下载到 ~/.cache/finite。你需要 Java 11 或更高版本。每个配置在给出与当前代码一致的结果时打印 ok，否则打印 FAIL。当规则被违反时，TLC 的输出（包含达到违规的最短路径）会保存为 crates/server/tla/<config>.out。这些文件已被 Git 忽略。
| 配置 | 已启用的修复 | 边界 | 当前结果 |
|---|---|---|---|
Fencing.cfg | 无 | 1 次编辑，1 次读取，2 个句柄，所有行为最多 18 步 | 通过，约 280 万状态，2 分钟 |
DesignLeases.cfg | 无 | 1 次编辑，2 个句柄 | 发现 1，数秒 |
Finding2.cfg | FixRetire | 1 次编辑，2 个句柄 | 发现 2 |
Finding3.cfg | FixRetire, FixOrphan | 2 次编辑，2 个句柄 | 发现 3 |
Finding4.cfg | + FixStaleDrop | 2 次编辑，2 个句柄 | 发现 4，约 1 分钟 |
AllFixes.cfg | 全部四个 | 2 次编辑，2 个句柄 | 通过，约 1600 万状态，2 分钟 |
每个配置都将存储的纪元（epoch）限制为 3，并且不包含崩溃或失败的写入。读取是指加载设计但不进行编辑的调用，例如 MCP 读取工具或查看器的 socket。Fencing 需要一个读取，因为只有当两个调用都加载了设计时，才可能存在陈旧副本。包含该读取的完整状态空间在 30 分钟内未能完成，因此 check.sh 使用 TLC 的迭代加深（-dfid 18）运行：所有最多 18 步的行为。最短的陈旧覆盖需要 17 步。发现配置会探索其边界内的所有可能性。TLC 会在违反第一条规则时停止，因此在运行下一个发现配置时，会启用针对之前发现的提议修复。Fix* 常量是假设性开关。当它们都为 FALSE 时，模型代表当前的代码。
解读结果
请搭配 /statechart 技能阅读每个结果。它可以将 TLC 找到的到达规则违反的最短路径转换成一个带编号的步骤列表，使用通俗的语言；当一个配置通过时，它会画出一张图表来说明设计如何在不同服务器之间转移。
当一个配置打印 FAIL 时，请判断 bug 是在代码中还是在模型中：
- 真正的 bug 会在代码中产生一条可以复现的路径。逐一执行每个步骤，打开表中对应的函数，检查代码是否允许以该顺序执行该步骤。然后像下面“已知发现”那样，用代码的语言报告该路径。在检查通过之前，不要放宽规则或边界，除非被要求，否则不要更改产品代码。
- 模型错误 会产生一个代码无法执行的步骤。例如：在模型中拆分了两个本应在同一个锁（状态互斥锁、持久化互斥锁）下执行的代码步骤；模型步骤缺少代码中存在的守卫条件；或者心跳续约后立即过期。修正模型以匹配代码，并说明你修正了什么。
- 如果
Fencing.cfg失效，那是因为深度限制的运行路径没有命名其步骤。要获取命名的最短路径，请使用广度优先运行同一个配置：cd crates/server/tla && java -cp ~/.cache/finite/tla2tools-1.7.4.jar tlc2.TLC -workers auto -config Fencing.cfg DesignLeases.tla。它会在第一个违规处停止，对于“当你故意修改所覆盖的代码时”下的违规，这大约需要 6 秒。 error意味着 TLC 未能完成：解析错误，或者某个动作未给变量赋值。请阅读.out文件。
如果代码之前违反规则而现在通过了，FAIL 反而是好消息。下面的“已知发现”表格展示了如何记录它。
当你故意修改所覆盖的代码时
- 在与代码相同的提交中更改模型步骤，并保留命名该函数的注释。
- 如果你的更改修复了一个发现，请将修复作为代码（而非开关）放入模型中：删除
Fix*常量，使步骤的行为与新代码一致，并从所有配置中移除该开关。下一个发现的配置将成为默认配置，check.sh会获得新的预期结果。 - 在确信测试通过之前，先故意破坏临时副本中的代码，在模型中镜像这个破坏，并检查配置是否能捕获它。例如，如果你从
PgStore::save中删除AND epoch = $3，并从SaveWrites中删除x.ptok = store.epoch，那么Fencing.cfg会违反 StoredEditsStay。一个你从未见过失败的检查不能证明任何事情。 - 运行
check.sh --full，然后向前移动同步提交指针。
已知发现
每一个都是代码在提交 6606714 时的竞态条件。在每种情况下，代理的工具调用返回成功，但编辑却丢失了。
- 编辑落在一个正在保存其最后一个快照的副本上。 服务器 A 已加载该设计，并且一个 MCP 调用已经通过了
Hub::open。服务器 B 加入并赢得了设计（A 上的租约过期也会导致同样结果）。A 的 tick 调用let_go，因此retire将副本标记为Retiring。保存任务的take_save获取最后一个快照。然后，该调用的DesignHandle::edit获取锁并提交到正在退役的副本上，因为edit从不检查life。保存任务保存了不包含该编辑的快照，释放了租约，并且drop_copy清除了pending。B 加载的设计不包含该编辑。要在实际应用中触发此问题，当 tick 运行时，编辑必须已经在等待设计的锁，例如多个运行大型write_html调用的代理。撤销、重做、导入和评论更新走的是相同的路径。 - 编辑落在一个已被 hub 从列表中移除的句柄上。 调用的
handle_for返回一个未加载的句柄。B 加入，A 的let_go发现没有加载任何内容，因此它调用remove。该调用的load声明了租约并在那个句柄上加载了一个副本。下一次 tick 的loaded列表来自 hub 的列表，而该列表不再有这个句柄。因此，tick 释放了租约，并且该副本的下一次保存以Fenced失败。这不需要停滞，只需要一个服务器加入。 - tick 丢弃了一个在 tick 读取它之后又被加载的副本。 同一服务器，没有成员变更。tick 读取
lease()（令牌 1）。然后设计卸载，一个调用再次加载了它（令牌 2）并提交了一个编辑。tick 读取held()（令牌 2），发现 2 ≠ 1，并调用drop_copy。drop_copy结束了新副本，包括待处理的编辑。这个窗口只有两次读取之间那么短，因此很窄，但它每次 tick 都会运行。 - 刚刚续约了其租约的服务器提供了其陈旧副本。 B 停滞超过其租约期，A 接管了设计并保存了一个编辑。B 唤醒。它的 tick 续约了心跳，从那一刻起
Members::now将 B 视为存活状态并再次将其作为拥有者。但是let_go循环还没有运行。B 上的一个调用加载了仍然为Live的陈旧副本并提交了一个编辑，该编辑稍后以Fenced失败。它首先需要一次停滞。
AllFixes.cfg 针对每个发现检查了一个提议的修复：edit 拒绝一个不是 Live（1）或句柄未被列出（2）的副本。tick 仅在其令牌是它读取的那个时才丢弃一个副本（3）。一个在滞后后又续约的服务器会将自己排除在外，直到它调用了 let_go（4）。有了所有四个修复，AckedEditsStay 在这些边界内成立。
未涵盖的内容
- 一个设计，两个服务器，MCP 编辑。撤销、重做、导入、评论和重命名走的是相同的锁和提交路径，但没有被单独建模。
Hub::delete也未建模。 - 文件存储和
FINITE_NODES交接（hand_off_one，adopt），以及路由器。 - 关闭时的
Hub::flush、日志压缩阈值（COMPACT_AFTER，COMPACT_BYTES）和Recent（查看器恢复背后的缓冲区）。 - 时序。TLC 会尝试所有步骤顺序，因此模型表明存在竞态，但不显示其发生频率。它假设服务器自身的租约定时器（
Members::lapsed）不会晚于数据库将其心跳视为过期的时间。这前提是两个时钟以相同的速率运行。 - 更大的边界。更多编辑、读取、句柄或纪元、崩溃和失败的写入不在日常配置中。
AllFixes.cfg也通过了 1 次编辑、1 次崩溃和 1 次失败写入（340 万状态）的测试。超过 18 步的 Fencing 尚未完成：在 1 次编辑和 1 次读取的情况下，它通过了 5000 万个不同的状态并且仍在继续。不要相信没有读取的旧 Fencing 通过结果：仅一次编辑只会加载一个副本，因此没有任何东西会变陈旧。