方法与工具 / INTERACTIVE EDITION · ETCD 3.6.6

历史检查台

这些已完成操作能否放进一次合法的寄存器执行？

原理模型检查 — 不是集群实测

单整数寄存器，初值 0。读返回当前值，写替换它。所有操作均已完成，每客户端顺序调用，区间处于可比的同一时钟。不支持未完成/超时调用、事务、因果消息或租约。

选择历史

已完成操作（JSON；value 为写入值或读结果）

id/client 为非空字符串；type 为 read/write；value 为安全整数；start/end 为有限数且 start < end；同客户端区间不得重叠。输入只在浏览器处理，不存储，不发送分析数据。

模型
搜索状态数（1–100,000）

通过给出一个合法顺序；失败表示在该模型中穷尽全部合法顺序；未判定表示达到 12 操作上限或搜索预算，绝不算通过；输入无效表示格式或范围不支持。有限历史通过不等于实现被证明正确。

搜索枚举前置关系的拓扑顺序和寄存器状态，按已选集合/当前值记忆。真实时间边使用 end ≤ 下一次 start；顺序一致模式只保留同客户端的边。解释见第 2–3 章；独立全排列基准测试在下载源码中。