报告 001 · 动作恢复的受限状态枚举

文档索引 · 当前设计 · 研究问题

日期：2026-09-19。证据层次：受限状态模型。结论状态：发现反例，支持在特定条件下保留动作不确定性；未验证真实执行系统。

1. 问题与模型

问题：本地已持久化一个动作意图，是否能够仅凭本地完成标记，在崩溃后同时保证动作不遗漏且不重复？

模型包含一个动作和至多一次进程崩溃。初始持久状态为 queued，依次进行登记尝试、提供者执行、收到回执、保存完成。崩溃丢失所有易失状态，但保留本地持久记录和外部已经发生的效果。

枚举程序用广度优先搜索遍历各策略的可达状态，将相同状态合并，并保留一条最短到达路径。没有随机采样；状态数描述这个小模型，不代表测试覆盖率或发生概率。

明确假设：

• 本地持久写入与远端动作各自原子，不模拟磁盘损坏。
• 不模拟已经发出但仍在网络中、可能于恢复后才执行的请求。
• 没有并发调用、参数变化或其他操作者修改外部状态。
• 若策略允许继续执行，恢复后的请求最终得到回执。
• 提供者去重分支假定稳定业务键、永久有效的去重记录，以及去重记录和副作用共同原子持久化。

这些假设刻意简化现实。简单模型中出现的反例足以否定过强保证；没有发现反例不能证明真实系统正确。

2. 对照与实际输出

终止状态包含等待外部核对的 unknown，因此“不明时暂停”没有证明最终完成。去重分支的结果依赖提供者的理想化契约，不能推广到只有本地幂等键的调用。

程序同时断言：重试策略出现重复反例；提前确认策略出现虚假完成；保守策略的 unknown 同时可能对应 0 次或 1 次外部效果；去重分支在此次枚举的所有终止状态中效果次数均为 1。此次执行这些断言全部成立。

3. 两个反例

重复执行的路径：

登记 attempted
→ 提供者产生效果
→ 崩溃，尚未保存回执
→ 恢复后按相同操作身份重试
→ 提供者再次产生效果

使用相同本地操作标识不够；提供者必须实际理解并保证该标识的去重语义。

漏执行的路径：

发送前保存 confirmed
→ 崩溃，尚未调用提供者
→ 恢复后按已完成处理

4. 无法由本地记录区分的历史

枚举得到两条恢复时本地状态完全相同的路径：

在这个模型中，本地记录没有足够信息判断属于哪条历史。恢复需要新的外部证据、提供者去重保证或明确保留未知；仅调整本地队列字段无法消除该信息缺口。

5. 对设计的影响

支持保留以下要求：操作意图和实际效果分别记录；无法确认时允许 unknown；重试策略根据真实提供者的去重与查询契约制定。实验没有决定必须使用哪些表、字段名或状态机实现。

不能从本实验推出：SQLite 已满足持久化要求、MRPC 已提供业务幂等、多心智提交策略正确、认知分段有效，或整个系统可以恢复。这些仍需独立实验。

下一次扩展可加入延迟到达的旧请求、去重记录过期、参数与提供者切换、取消与执行竞态，尝试推翻当前理想化去重分支的保证。

依赖仅为 Python 标准库；本实验使用 Python 3.14.7，无网络、无模型调用、无真实外部动作。

从仓库根目录执行：

脚本 SHA-256：d14015c0778115d63aea8120b55e48bc1c3b9cc024ac464a844c8c8d30d29173。

这是独立研究脚本，未连接产品运行时。修改模型后应重新生成结果并更新报告，保留假设变化与反例，不能把旧结论套用到新模型。

数据可用性

本报告公开实验条件、汇总统计和失败分析。原始输入、脚本及逐次运行记录未随报告发布，因此不能仅凭本文独立复现实验。