软件建模E03：TLA+有限模型检查，找到重复承诺的执行次序
两个请求先后检查同一台设备，都看到可用，然后分别提交预留。每个请求单独运行都没有问题；交错运行时，却可能同时得到承诺。测试某一条执行顺序，只能说明那次运行的结果，不能代替对模型所允许次序的检查。
本篇使用真实 TLC 检查器执行一个 TLA+ 有限模型。未保护版本产生五个状态的重复承诺反例，增加提交时的原子检查后，检查器遍历完指定范围，没有发现违反不变量的状态。两个结果都保留原始输出与进程退出码。
先固定工具和观察范围
实验冻结官方 TLA+ tools 发布标签 v1.7.4，下载其中的 tla2tools.jar。运行横幅显示的是组件版本 TLC2 Version 2.19、修订 5a47802；发布包版本与组件横幅不是同一编号。这里使用一个固定历史版本，不以“最新版本”作为可复现条件。官方1.7.4发布页
下载文件先与发布页的 SHA1 对照，再把实际 SHA256 写入工具锁。读者入口从固定官方 URL 下载缺失文件，运行前总会核对 SHA256；jar 放在外部缓存，不进入示例源码。实际运行使用 Corretto Java 21.0.11，命令行和 Java 版本另存为证据。
TLC 是显式状态模型检查器，可以检查一部分常用 TLA+ 规格，尤其是有限系统。本题关心先检查、后提交的交错行为，因此选择 TLA+ 与 TLC；本篇没有运行 Alloy，也不比较两种工具在所有问题上的优劣。TLC项目文档
模型只有两个请求 R1、R2，竞争一台设备的同一个冲突时间段。时间区间已经被抽象成“互相冲突”，没有分钟、时区或跨日计算。每个请求检查一次、提交一次，不取消、不重试、不崩溃。这些限制决定了后面通过结论的范围。
状态记录了什么
stage 保存每个请求处于未检查、已检查或已完成；sawFree 保存该请求上一次检查时看到的空闲结果；committed 保存已经获得承诺的请求集合。初态中集合为空，两个请求都尚未检查，缓存结果为假。
检查动作读取当前承诺集合，若为空，就把自己的观察记成真，然后进入已检查阶段。它不会占用设备，也不会阻止另一个请求执行同样的检查。这个设计使“读到空闲”与“取得承诺”成为两个独立动作。
提交动作将请求推进到已完成。未保护版本只相信先前的 sawFree；只要该值为真，就把自己加入承诺集合。即使另一项请求已经在两次动作之间提交成功，这个旧观察仍不会自动变化。
sequenceDiagram
participant A as 请求R1
participant S as 承诺集合
participant B as 请求R2
A->>S: Check：集合为空
S-->>A: sawFree为真
B->>S: Check：集合仍为空
S-->>B: sawFree为真
A->>S: Commit：加入R1
B->>S: Commit：仍相信旧观察，加入R2
Note over S: 集合含R1、R2，违反至多一个承诺第一张图对应工具实际找到的轨迹，而非预先固定给检查器的脚本。Next 每一步可以选择任意尚有动作可执行的请求，因此既包含顺序处理，也包含图中的交错处理。工具通过扩展后继状态发现导致失败的选择。
不变量必须写成可检查的性质
NoDoubleCommitment 要求承诺集合的基数至多为一。另一个 TypeOK 检查阶段函数、布尔观察和承诺集合属于声明的取值范围。仅有类型正确还不够：含 R1、R2 的集合类型完全合法，却违反资源承诺政策。
规格通过配置文件给出两个模型值，并分别把 Protected 设置为假与真。两次运行使用同一份动作定义和同一个不变量，改变的只有保护开关。这样，结果差异能追溯到提交条件，而不是换了性质或缩小了请求集合。
原始未保护输出显示，两个请求先各自完成检查，然后 R1 提交，最后 R2 提交。在第五个状态，集合变为 {R1, R2}，TLC 报出具名不变量违反，进程退出码为 12。入口同时检查错误名称、双承诺集合和两个真观察，避免把解析失败当成发现反例。
本次搜索在反例处停止，输出还有三个状态留在队列。它已经给出推翻该不变量的合法轨迹，不需要再走完剩余状态才能确认这项错误。报告中的“找到反例”与后面“完成整个有限搜索”因此对应不同证据。
保护条件放在哪一步
保护版本仍允许两个请求都读到空闲，但提交动作在加入集合之前再次要求当前集合为空。检查与加入写在同一个模型动作内。R1 已经提交后，R2 的旧观察虽然仍为真，当前集合检查却失败，因而只结束请求，不新增承诺。
flowchart TB
C["已检查，保存旧观察"] --> P["提交动作：旧观察为真？"]
P -->|否| D["完成，不新增承诺"]
P -->|是| LIVE["当前承诺集合为空？"]
LIVE -->|否| D
LIVE -->|是| ADD["在同一个原子动作内加入自己"]
ADD --> END["完成，承诺集合至多一项"]第二张图强调模型动作的原子边界。如果实现把“重新读集合”和“写入承诺”再次拆成两个不受保护的步骤，相同竞态仍可能出现。模型没有自动选择数据库事务隔离级别、锁、版本比较或唯一约束；这些实现机制需要另行证明符合这个原子动作。
保护版本实际生成 19 个状态，发现 14 个不同状态，结束时队列为零，退出码为 0。输出中的“未发现错误”只针对这份配置的可达状态及所检查性质，不是对任意请求数量、故障模式或生产程序的证明。
完成请求不等于保证获得设备
保护版本会让竞争失败的请求进入已完成阶段，但没有给它承诺。当前性质允许这种结果，因为目标只是防止重复承诺。如果需求还规定请求必须收到明确的成功或拒绝回执，就要把结果状态加入模型，不能从集合中没有它推断回执已经发送。
全部请求完成后，规格允许保持状态不变的动作。这样，终止状态不会仅因没有后续业务动作而被报告为死锁。实验没有检查公平性，也没有声明每个请求最终都会获批；安全性条件与进展要求需要分别表达。
模型还把提交写入当成持久结果，没有宕机恢复、网络丢包或消息重放。若实际系统可能在写入后、回执前失败，就需要增加中间状态和重试语义。直接拿本例的绿色结果回答“重试会不会重复确认”，超出了检查对象。
模型检查与实现之间还缺一条对应关系
既有租赁应用中的预留编号、设备编号、时间段和事务边界，比三个模型变量更丰富。应用的一次操作可能映射为模型的一步，也可能跨越多步。需要明确哪些程序状态对应 committed，以及哪些不可见内部步骤不会改变观察到的承诺事实。
小模型可以揭示一种确实可能的设计错误，但没有建立程序到模型的精化关系，就不能把模型检查通过转写为代码已被形式化验证。这里没有读取或验证累计 Java 实现，也没有执行数据库并发压力测试。
有限范围仍然有用：两个竞争者已经足以暴露这次先检查后提交的缺陷，反例给出了可转成应用测试的具体次序。若增加取消、延期或多个设备，需要扩大状态与性质，再重新运行；旧的 14 个状态不能覆盖新需求。
搜索参数也是证据的一部分
实验固定一个工作线程、种子和指纹多项式编号，减少并行搜索次序对反例展示的影响。原日志仍包含启动时间、进程号和临时目录，所以不要求日志逐字节一致；核对的是指定不变量、具体违反状态、完成状态和退出码。只截取一个绿色结尾，会丢掉这些复现条件。
TLC 使用状态指纹识别已访问状态，成功输出还列出指纹碰撞遗漏状态的概率估计。本例如实保留这段工具报告，没有把概率估计转写为数学证明。若业务需要更强结论，还要考虑性质证明、实现精化及工具假设；扩大请求数并不能自动填补这些缺口。
反例也要检查是否来自过度抽象。这里把两个请求视为冲突，是因为它们竞争同一设备的同一时段；若实际时间段互不重叠，至多一个承诺就会错误拒绝正常业务。将性质套到不同时间段之前，必须把区间关系重新放回模型。
复跑检查器
1 | |
运行前让 JAVA_HOME 指向可用的 Java 21，或把对应 Java 放入 PATH。MODELING_TOOL_CACHE 可指定外部缓存位置；未设置时使用系统临时目录下的专用缓存。首次运行需要访问官方 GitHub，已有缓存仍会校验摘要。
实际入口完成 7 项结果核对并退出 0，其中未保护子进程退出 12、保护子进程退出 0。unguarded-output.txt 保存完整反例，protected-output.txt 保存有限搜索统计，工具锁和调用清单记录复现条件。受限环境若禁止 TLC 的本地管理端口，应把它记为环境失败，不能冒充模型结果。
