工作模型

工作模型 是做什麼的？

你撰寫一個小型的 *.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 會將分數儲存到頁面中。

工作流程

1. 選擇能展示令人驚訝部分的最小模型。 一個機制，一個場景，2 到 4 個滑桿。問：聰明的讀者可能會在哪裡搞錯？建立一個場景，讓那一刻發生在螢幕上（爆量清空桶子、重試同時發生、掃描刷新快取）。
2. 建立基本框架或複製範例。 從 working-model new <name> 開始，或從 examples/ 中最接近的檔案開始（權杖桶、帶抖動的退避、LRU 快取、TCP AIMD、斷路器、SIR 流行病、複利、負載平衡、布隆過濾器、Raft 領導者選舉、庫存再訂購點）。
3. 撰寫參數、狀態和規則。 離散時間：每個滴答執行 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)）。
4. 撰寫 3 到 8 個能捕捉關鍵洞察而非瑣碎細節的宣稱。 一個只是複讀規則的宣稱（例如「權杖永遠不會超過容量」，而規則正是 min(capacity, ...)）不可能失敗，也教不了任何東西；有趣的宣稱會說出讀者猜不到的事：「比快取大一個鍵的迴圈完全沒有命中」、「抖動降低了峰值重試負載」。使用正確的種類（at、always、never、eventually、whenever、sweep、compare；請參閱 references/claims.md）。
   • 至少一個宣稱必須在預設值下成立，並且在移動某個滑桿時失敗，這樣讀者才能看到解釋在哪裡不再成立。check 會列出哪些滑桿位置會破壞哪些宣稱。
   • 每個宣稱都必須是關於真實機制的真實陳述，而不僅僅是你的模型。將關鍵事實的來源放在 sources 中，並在 summary 中說明模型假設。只有在宣稱僅對這個種子成立時，才寫「在此次執行中」。
   • 讓句子精確表達表達式檢查的內容。check 證明的是表達式，而不是句子；步驟 7 測試宣稱是否可能失敗。
   • 確保 duration 夠長，足以應對最慢的滑桿設定，否則 eventually 宣稱可能僅僅因為執行結束而失敗。
5. 在文字中綁定數值。 說明文字和宣稱文字使用 {expression} 佔位符：寫 {capacity}，永遠不要使用當滑桿移動時會過時的文字 10。check 會對文字數值發出警告（W_LITERAL_NUMBER）並建議綁定。說明文字必須引用其所依賴的宣稱（cites）；引用失敗的宣稱是錯誤。
6. 執行 check 直到它顯示 N/N claims pass 且沒有錯誤。 同時修復警告。
7. 然後執行 check --mutate：測試宣稱。 它會故意破壞規則，每次突變一個小的變更（< 改為 <=、pop 改為 shift、刪除一行、事件延遲一個滴答），針對每個突變體重新檢查每個宣稱，並報告哪些宣稱捕捉到了哪些錯誤。
   • 每個宣稱必須殺死至少一個突變體。 被列在「從未失敗的宣稱」下的宣稱無法失敗：它只是在複述規則、空洞地成立，或者場景從未讓它經歷考驗。加強它（讓表達式包含句子的全部語義）或變更場景，讓宣稱受到考驗（交錯到達而非一次爆發、一個無法容納的迴圈）。references/claims.md 有一個實例。
   • 對於每個存活的突變體，要嘛添加或加強一個宣稱，要嘛在你的回覆中解釋為什麼這個變更無法被觀察到（例如，它只是重新命名了鍵）。只有真正無害的突變體才能被放入規格中的 mutate.ignore，並附上原因。永遠不要為了提高分數而削弱一個宣稱或斷言。
   • 被標記為等效或僅影響視覺的突變體不會改變任何宣稱能看到的東西；它們不計入分數。僅影響視覺的突變體會改變頁面的繪製內容，因此在螢幕截圖中檢查這些數字。
8. 永遠不要為了讓宣稱通過而削弱或刪除它。 當一個宣稱失敗時，判斷哪一個是錯的：
   • 模型錯了（規則錯誤、預設值錯誤、缺少機制）：修正模型；
   • 宣稱錯了（真實機制並非如此行為，或僅在特定條件下成立）：修正宣稱並說明錯在哪裡。 用一兩句話告訴使用者是哪個以及為什麼。不允許放寬容差直到通過，或用一個更簡單的宣稱來替換。
9. 建置，然後執行 layout。 修復所有 E_ 問題（零件重疊、文字溢出、文字碰撞、頁面在 390 px 寬度下橫向滾動）。通常：給予零件更多網格單元、縮短標籤、或移動零件。也要修復 W_LINK_CROSSES（一個箭頭繪製在另一個零件上）：移動零件或添加 via 點。查看它產生的螢幕截圖，並檢查顯示的每個數字是否都是你預期的：零件綁定不受任何宣稱測試。對於讀者可能會依賴的計數器或量表，添加一個 expect（一個獨立計算相同數字的方法，例如 "expect": "len(queue)"），如果兩者差異，check 將會失敗。
10. 交接： 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/ 中的合成示範時使用。軌跡從不是必須的。

1. 首先說明軌跡可能包含私有資料（請求 ID、使用者 ID、IP、權杖）並在本機上處理它。導入僅保留映射讀取的屬性：working-model trace import trace.jsonl --mapping trace-map.json --out trace.normalized.json。僅在使用者確認檢測記錄了所有映射種類的每個事件時才傳遞 --complete；否則完整性保持為 unknown。
2. 在你撰寫的內容中區分四件事： 模型假設、來自來源的機制事實、模型內的宣稱，以及觀察到的斷言。將假設放在規格的 reality.assumptions 中。
3. 根據軌跡實際包含的內容撰寫映射。 永遠不要發明軌跡未記錄的關聯 ID 或事件；沒有雙方主體關聯的輸出是無關聯的，其斷言是無法確定的。每個模型事件要嘛被重播，要嘛被列在 internalEvents 中。
4. 執行 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 表示檔案遺失或達到限制。
5. 當軌跡不一致時，在實質上修正假設，通常在第二個模型中，並保留反例。永遠不要為了通過而放寬 minPrecision、minRecall 或 withinMs。
6. 對於要查看的頁面，執行 working-model build spec.model.json --trace trace.normalized.json --mapping trace-map.json -o page.html：一般的解釋器加上一個模型對比觀察到的時間線、第一個不匹配和每個斷言。它包含標準化的軌跡，因此保持本地。
7. 僅在使用者要求發布時，先執行 working-model bundle spec.model.json --public ... --preview，向他們顯示金鑰列表，然後在沒有 --preview 的情況下執行它。真實的軌跡需要他們的明確 --acknowledge-privacy；永遠不要代他們傳遞。
8. 說明證據未顯示的內容： 未觀察到的狀態、取樣軌跡、所涵蓋的時間視窗。這是一個帶有軌跡證據的可執行解釋，而不是形式化驗證。

格式、選擇器和斷言種類：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": "Token Bucket Rate Limiter",
  "summary": "A bucket holds up to {capacity} tokens and refills at {refill} per second.",
  "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": "Bucket size", "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": "Bucket", "level": "fill", "text": "{tokens:.1} of {capacity}" },
    { "id": "chart", "type": "chart", "at": [0, 5, 12, 3], "label": "Tokens", "series": [{ "expr": "tokens" }] }
  ],
  "narration": [{ "from": 1, "to": 3, "text": "The first {capacity} requests spend the stored tokens.", "cites": ["burst-passes"] }],
  "claims": [{ "id": "burst-passes", "kind": "at", "t": 1, "expr": "accepted == capacity", "text": "A full bucket lets exactly the first {capacity} requests through." }]
}

• 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