旧Worker为什么还会写入？

I15 旧Worker为什么还会写入？

关联章节：M07 · 交互类型：lease-race · 状态：提供纯逻辑参考函数，UI待实现

教学目标

lease到期与资源拒绝旧拥有者是两个机制。

初始状态

{
  "current_token": 1,
  "lease_until": 10,
  "now": 0,
  "workers": {
    "A": 1,
    "B": null
  }
}

操作控件

• 推进时钟

• B接管并递增token

• A尝试写

• B尝试写

• 关闭资源端token检查（危险对照）

状态变化规则

• A在t0持有token1，lease至10。

• t10后B接管得到token2；资源写入要求token相同且now<lease_until。

• 危险对照只演示如果不检查会产生的错误，不改变正确答案。

黄金案例与反馈

old-owner

输入：

{
  "token": 1,
  "current": 2,
  "now": 11,
  "lease_until": 20
}

期望：

{
  "allowed": false
}

lease过期不会物理停止A，资源必须拒绝旧token。

new-owner

输入：

{
  "token": 2,
  "current": 2,
  "now": 11,
  "lease_until": 20
}

期望：

{
  "allowed": true
}

当前拥有者在有效lease内。

boundary

输入：

{
  "token": 2,
  "current": 2,
  "now": 20,
  "lease_until": 20
}

期望：

{
  "allowed": false
}

到期边界不可写。

完成条件

• 构造A/B竞争并拒绝A

• 说明外部工具也需相应边界

反馈层次

• 提交预测后显示结果；允许跳过预测但记录跳过，不阻止阅读

• 结果同时显示状态变化、原因与被拒绝动作；不是只给红绿灯

• 第一次错误给边界提示，第二次提供最小反例；参考推导始终可主动打开

• 重置恢复固定初始状态并保留历史尝试供用户手动清除

无障碍与静态替代

• 全部操作有原生button/input/select替代，不依赖拖拽

• 图与动画提供同步文字状态表；支持prefers-reduced-motion

• 状态改变用aria-live=polite摘要，不逐字朗读长日志

• 焦点不跳走；错误提示关联输入；颜色不是唯一编码

无JavaScript时直接展示初始输入、规则和黄金案例表，读者仍能完成纸面推演。状态动画仅作解释，不能成为获取答案的唯一途径。

持久化与重置

使用版本化键agent-course:1:I15，仅保存本地学习状态。支持单卡重置和全站清除；存储失败时以内存模式继续，不阻断阅读。

必须避免的误导

fencing不等于自动取消旧线程，且不能保护未验证token的远程资源。

执行边界

纯本地教学状态机；不执行任意代码，不连接真实资金/模型/宿主Shell。

逻辑参考

web/reference/engines.mjs中的canWrite；对应测试在web/reference/engines.test.mjs。UI可复用或等价移植，但不得改变黄金结果。