工作模型是做什么的？

你编写一个小的 *.model.json 规范：参数（滑块）、状态、用微小安全规则语言编写的规则、事件场景、绑定到状态的视觉部件、说明文字和断言。CLI 在 Node 中模拟它，检查每条断言，检查文本，并构建一个离线 HTML 页面，该页面运行相同的引擎，并在读者拖动滑块时实时重新检查断言。

关键点：一个经过测试的解释。一个模型无法支持的断言，在用户看到之前就会失败。

命令

所有命令在 Node 20 或更新版本上运行，无需 npm install。保留引号：路径可能包含空格。

node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" new token-bucket --dir ./explainers         # 一个已经通过的规范
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" check ./explainers/token-bucket.model.json  # 模式检查、模拟、断言、文本检查
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" check ./explainers/token-bucket.model.json --mutate   # 断言能否捕获被破坏的规则？
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" build ./explainers/token-bucket.model.json -o ./explainers/token-bucket.html
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" layout ./explainers/token-bucket.model.json --out ./explainers/shots   # 需要本地 Chrome 或 Edge
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" snap ./explainers/token-bucket.model.json --at 2 -o shot.png           # 可选的截图
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" fuzz ./explainers/token-bucket.model.json --cases 300 --seed 7          # 基于种子的反例搜索
node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" check ./explainers/token-bucket.model.json --trace t.normalized.json --mapping trace-map.json   # 模型与观测轨迹对比

下面，working-model 是 node "${CLAUDE_SKILL_DIR}/scripts/working-model.mjs" 的简写。在不替换 ${CLAUDE_SKILL_DIR} 的代理中，请使用此文件所在的文件夹。check 退出码：0 表示所有断言通过，1 表示断言或文本检查失败，2 表示规范无效。添加 --json 以获得机器可读的输出，添加 --set name=value 以尝试其他滑块位置。--mutate 在断言不失败时退出 0；添加 --mutate-strict（和 --min-score 80）以在断言从未失败或分数较低时退出 1。build --mutate 将分数存储在页面中。

工作流程

选择能展示最令人惊讶部分的最小模型。 一个机制，一个场景，2 到 4 个滑块。问：一个聪明的读者会在哪里出错？构建场景，使那个时刻在屏幕上发生（耗尽桶的突发流量，同时发生的重试，刷新缓存的扫描）。
搭建框架或复制一个例子。 从 working-model new <name> 开始，或从 examples/ 中最接近的文件开始（令牌桶、带抖动的退避、LRU 缓存、TCP AIMD、断路器、SIR 流行病模型、复利、负载均衡、布隆过滤器、Raft 领导者选举、库存再订购点）。
编写参数、状态和规则。 离散时间：每个滴答运行 rules.tick，然后该滴答的事件触发其 rules.on.<event> 处理程序。保持单位一致（timeUnit，滑块 unit）。使用 emit('name', payload) 来触发链接动画或断言应关注的事物。
- 时间是浮点数。 t 是 tick × dt，因此存储为 t + lead 的时间永远不会完全等于稍后的 t。对于截止日期和倒计时，存储滴答数（due = tick + round(lead / dt)，然后 tick >= due）。references/spec.md 在“编写行为正确的规则”中有更多此类陷阱。
- 列表是值: a = b 复制。通过索引更改嵌套列表（push(queues[i], job)）。
编写 3 到 8 条捕获关键见解的断言，而不是琐事。 一条重述规则的断言（“令牌永远不会超过容量”，当规则是 min(capacity, ...) 时）无法失败，也学不到任何东西；有趣的是读者猜不到的断言：“一个比缓存大一个键的循环完全没有命中”，“抖动降低了峰值重试负载”。使用正确的类型（at, always, never, eventually, whenever, sweep, compare；参见 references/claims.md）。
- 至少有一条断言必须在默认值下成立并且在移动滑块时失败，以便读者看到解释在何处不再成立。check 列出哪些滑块位置破坏了哪些断言。
- 每条断言必须对真实机制为真，而不仅仅对您的模型为真。将关键事实的来源放在 sources 中，并在 summary 中说明模型假设。当断言仅在此种子下成立时，写“在此次运行中”。
- 让句子准确表达表达式检查的内容。check 证明的是表达式，而不是句子；第 7 步测试断言是否可能失败。
- 使 duration 足够长以应对最慢的滑块设置，否则 eventually 断言可能仅因为运行结束而失败。
在文本中绑定数字。 说明文字和断言文本采用 {expression} 占位符：写 {capacity}，永远不要写一个当滑块移动时会过时的字面量 10。check 会警告字面数字（W_LITERAL_NUMBER）并建议绑定。一条说明文字必须引用其依赖的断言（cites）；引用一条失败的断言是一个错误。
运行 check 直到它显示 N/N claims pass 且没有错误。 同时修复警告。
然后运行 check --mutate：测试断言。 它故意破坏规则，每个突变一个小的更改（< 改为 <=，pop 改为 shift，删除一行，事件延迟一个滴答），针对每个突变重新检查每条断言，并报告哪些断言捕获了哪些错误。
- 每条断言必须杀死至少一个突变。 列在“从未失败的断言”下的断言无法失败：它重述了一条规则，空洞地通过，或者场景从未执行它。加强它（让表达式说明其句子的全部内容）或更改场景，以便断言受到考验（交错到达而不是单次突发，一个放不下的循环）。references/claims.md 中有一个实际例子。
- 对于每个幸存的突变，要么添加或加强断言，要么在回复中解释为什么该更改不可见（例如，它只重命名了键）。只有真正无害的更改才进入规范中的 mutate.ignore，并附带理由。永远不要为了提高分数而削弱断言或断言。
- 标记为等价或仅视觉更改的突变不会改变断言能看到的任何内容；它们不计入分数。仅视觉更改的突变会改变页面的绘制内容，因此在截图中检查这些数字。
永远不要为了通过测试而削弱或删除断言。 当断言失败时，决定哪一个错了：
- 模型错了（规则错误、错误的默认值、缺失的机制）：修复模型；
- 断言错了（真实机制并非那样运行，或者仅在特定条件下才如此）：纠正断言并说明错误之处。用一两句话告诉用户是哪一个以及为什么。不允许放宽容差直到通过，或用一个更简单的断言替换它。
构建，然后运行 layout。 修复所有 E_ 问题（部件重叠、文本溢出、文本碰撞、页面在 390 像素宽度下水平滚动）。通常：给部件更多的网格单元，缩短标签，或移动部件。也修复 W_LINK_CROSSES（一条箭头穿过另一个部件）：移动部件或添加 via 点。查看它生成的截图，并检查显示的每个数字是否是你所期望的：部件绑定不受任何断言测试。对于读者会依赖的计数器或仪表，添加一个 expect（一种独立计算相同数字的方法，例如 "expect": "len(queue)"），如果两者有差异，check 会失败。
移交： HTML 路径、断言摘要行（6/6 claims pass）和突变分数，每条断言一行，以及哪个滑块破坏了哪条断言。提及读者应了解的任何模型假设。

寻找反例

在 check 和 check --mutate 通过后，working-model fuzz spec.model.json --cases 300 --seed 7 在邻近的种子案例上运行相同的断言：滑块值、模型种子以及 fuzz 块标记为可模糊测试的事件（移位、重复或删除）。然后 working-model minimize spec.model.json --case .working-model/fuzz/first-failure.json 缩小第一个失败，同时保持相同的断言失败。用通俗的语言报告最小化案例（“在分散的失败和断路器跳闸之间删除成功”）。在非默认设置下的失败是解释在何处不再成立的发现：基于实质性理由纠正断言或模型，保留反例，永远不要为了压制它而削弱断言。“未发现失败”不是证明。详情：docs/FUZZ.md。

与观测轨迹对比

仅在用户拥有真实系统的轨迹（JSONL 或 OTLP JSON 子集）或询问 examples/reality-bridge/ 中的合成演示时使用。轨迹不是必需的。

首先说明轨迹可能包含私有数据（请求 ID、用户 ID、IP、令牌），并在本地处理它。导入只保留映射读取的属性：working-model trace import trace.jsonl --mapping trace-map.json --out trace.normalized.json。仅当用户确认检测记录了映射种类的所有事件时，才传递 --complete；否则 completeness 保持 unknown。
在您写的内容中区分四件事： 模型假设、来自来源的机制事实、模型内的断言以及观测到的断言。将假设放在规范的 reality.assumptions 中。
根据轨迹实际包含的内容编写映射。 永远不要发明轨迹未记录的关联 ID 或事件；没有双方主体上的输出是不相关的，其断言也是不确定的。每个模型事件要么被重放，要么列在 internalEvents 中。
运行 working-model check spec.model.json --trace trace.normalized.json --mapping trace-map.json。 分别报告模型线和观测线（Model: 4/4 claims pass | Observed: 1 pass, 2 fail, 0 inconclusive），第一个不匹配及其事件 ID，以及每个不确定原因的原样。退出码 1 表示断言或观测到的断言失败；2 表示无效的轨迹或映射；3 表示缺少文件或超出限制。
当轨迹不一致时，基于实质性理由修复假设，通常是在第二个模型中，并保留反例。永远不要仅仅为了通过而放宽 minPrecision、minRecall 或 withinMs。
对于要查看的页面，运行 working-model build spec.model.json --trace trace.normalized.json --mapping trace-map.json -o page.html：普通的解释器加上模型与观测的时间线、第一个不匹配和每条断言。它包含标准化的轨迹，因此保持本地性。
仅当用户要求发布时，首先运行 working-model bundle spec.model.json --public ... --preview，向他们显示密钥列表，然后在不加 --preview 的情况下运行。真实轨迹需要他们明确的 --acknowledge-privacy；永远不要代表他们传递。
说明证据未显示的内容： 未观测到的状态、采样轨迹、时间窗口覆盖范围。这是一个带有轨迹证据的可执行解释，而非形式化验证。

格式、选择器和断言类型：docs/REALITY-BRIDGE.md。威胁模型：docs/TRACE-SECURITY.md。证据的限制：docs/CONFORMANCE-LIMITS.md。

在 CI 中保持诚实

当用户希望每次拉取请求时都检查解释时，添加 .working-model-ci.json（模型，以及要运行的断言、突变、模糊测试、现实和一致性检查，附有明确阈值）并复制 .github/workflows/working-model-ci.example.yml。working-model ci --config .working-model-ci.json --format markdown 打印审阅者阅读的摘要。永远不要为了通过 CI 而降低阈值。详情：docs/CI.md。

规范概览

{
  "title": "令牌桶速率限制器",
  "summary": "一个桶最多容纳 {capacity} 个令牌，并以每秒 {refill} 个的速率补充。",
  "sources": [{ "title": "RFC 2697", "url": "https://www.rfc-editor.org/rfc/rfc2697" }],
  "timeUnit": "s", "dt": 0.1, "duration": 16, "seed": 7,
  "params": [{ "id": "capacity", "label": "桶大小", "min": 1, "max": 30, "step": 1, "default": 10, "unit": "tokens" }],
  "events": [{ "name": "request", "at": 1, "count": 15 }],
  "state": { "tokens": "capacity", "accepted": 0, "rejected": 0 },
  "derived": { "fill": "tokens / capacity" },
  "rules": {
    "tick": "tokens = min(capacity, tokens + 2 * dt)",
    "on": { "request": ["if tokens >= 1 {", "  tokens -= 1; accepted += 1; emit('accept')", "} else {", "  rejected += 1; emit('reject')", "}"] }
  },
  "layout": { "cols": 12, "rows": 8 },
  "parts": [
    { "id": "bucket", "type": "tank", "at": [4, 0, 4, 4], "label": "桶", "level": "fill", "text": "{tokens:.1} / {capacity}" },
    { "id": "chart", "type": "chart", "at": [0, 5, 12, 3], "label": "令牌", "series": [{ "expr": "tokens" }] }
  ],
  "narration": [{ "from": 1, "to": 3, "text": "前 {capacity} 个请求消耗了存储的令牌。", "cites": ["burst-passes"] }],
  "claims": [{ "id": "burst-passes", "kind": "at", "t": 1, "expr": "accepted == capacity", "text": "一个满的桶正好让前 {capacity} 个请求通过。" }]
}

state 中的字符串是表达式（"capacity"）；文本值需要内部引号（"'closed'"）。
规则语言：数字、字符串、列表、true/false、+ - * / % **、比较、and or not、c ? a : b、let、if / else if / else、while、for x in list、break、continue、赋值操作符以及诸如 min max abs clamp round sqrt exp log rand randint chance pick len push pop shift unshift remove contains indexOf slice sum range fill emit 的函数。没有成员访问、没有用户函数、没有 eval。完整参考：references/spec.md。
部件：box tank queue stack grid counter gauge lamp node link chart label group，使用 at: [col, row, width, height] 放置在网格上。绑定和选项：references/parts.md。
断言以及如何编写好的断言：references/claims.md

工作模型

工作模型是什么？

在你喜欢的 AI 中提问

文档

工作模型是做什么的？

命令

工作流程

寻找反例

与观测轨迹对比

在 CI 中保持诚实

规范概览

相关技能

steipete/video-frames

steipete/summarize

openclaw/openclaw

obra/superpowers

affaan-m/ECC

affaan-m/everything-claude-code

在你喜欢的 AI 中提问

文档

工作模型 是做什么的？

命令

工作流程

寻找反例

与观测轨迹对比

在 CI 中保持诚实

规范概览

相关技能

steipete/video-frames

steipete/summarize

openclaw/openclaw

obra/superpowers

affaan-m/ECC

affaan-m/everything-claude-code

工作模型是做什么的？