statechart | 從 TLA+ 模型解讀狀態與反例
本頁以 pstack-claude 0.9.126 為基準。本次只介紹流程，不執行模型檢查或安裝工具。
定位與適用情境
此技能以 TLA+ 規格與設定為輸入，透過 TLC 模型檢查器 (model checker) 檢查規則，再輸出 Mermaid 狀態圖 (statechart) 與反例路徑。它不是把任意文字自動轉成經證實的真實系統模型。
情境是付款流程包含待付款、處理中、成功與失敗。團隊要檢查「未確認付款成功前不得出貨」。先由程式與產品承諾建立模型，明確表示付款結果與出貨狀態，再用此技能讓讀者看懂哪條事件路徑違反規則。
準備
- 準備 TLA+ 規格、設定檔、常數上界及規則文字。每個模型動作若描述程式，都要能對照原始碼。
- 使用儲存庫外的暫存資料夾。確認安裝版技能帶有 statechart 腳本，且有可執行 TypeScript 的執行環境。
- 原文指出首次執行會透過 mise 安裝 TLC 與 Java，並需要網路。未取得安裝或連網權限時先停下，不把這些工具當成既有能力。
Claude Code 使用 /pstack:statechart。Codex 插件選單插入 $pstack:statechart，skills-only 使用 $statechart。其他平台先核對能否執行附帶腳本，不能因技能能載入就宣稱工具可用。
操作步驟
- 把承諾寫成規則。 將讀者同意的規則寫為
INVARIANT，缺少付款或出貨變數就補入模型。Next應列出各動作的析取，保留可辨認的事件名稱。合法終態若沒有後續動作會被當成死鎖 (deadlock)，須用只在終態成立的無變更動作表達正常結束，不弱化業務規則。 - 建立讀者視圖。 視圖模組的
state(vars)可回傳字串、階層陣列或平行區域物件，step(action, from, to)則產生箭頭標籤。用「付款處理中」「付款遭拒」等可觀察用語，不直接把內部變數名稱當標籤。函式結果只能依賴傳入參數。 - 檢查有界模型。 依安裝版技能確認實際路徑，呼叫
<skill dir>/scripts/statechart SPEC.tla --config FILE --view FILE --out DIR。這是原文的指令形狀，範例中的路徑須換成實際檔案。常數或CONSTRAINT應限制模型規模，避免持續探索無界狀態。 - 逐規則閱讀報告。 將每個違反規則的最短路徑用付款事件重述，核對
breaks、mayBreak與Rules not checked。圖應盡量控制在約 20 條箭頭，不能合併掉不同規則的違反位置。若隱藏轉移，保留可達性並交代隱藏了什麼。 - 交付圖與重跑方式。 有
chart.mmd時以 Mermaid 程式碼區塊呈現，附上規則、路徑編號、模型省略事項及使用新輸出資料夾的重跑指令。描述真實程式的反例須逐步重現。重現不了時，先調查模型是否錯誤。
可直接使用的提示詞
用 pstack:statechart 檢查我提供的付款 TLA+ 模型與設定。
先核對模型與付款、出貨程式的對應，不從需求文字猜出真實行為。
規則是未確認付款成功前不得出貨，不要為了通過而弱化規則。
在儲存庫外的暫存目錄操作，先列出上界、假設及必要工具。
若需要首次安裝或連網，先回報，不要自行安裝。
用讀者看得懂的付款事件標示狀態和箭頭。
交付 Mermaid 文字、每個反例最短路徑、未檢查規則及模型省略事項。
若反例描述真實程式，提供隔離重現步驟，不接觸正式付款服務。預期結果與驗收
- 圖與報告應引用同一份模型與視圖，每項違反規則都有規則文字和報告路徑編號。
breaks表示圖中該狀態違規，mayBreak表示合併的模型狀態只有部分違規。 Rules not checked不是通過。原文流程發現違規後移除該規則再跑，其後各輪有 100,000 個不同狀態的上限，遇上限或錯誤要揭露尚未檢查的規則。- 完整圖有 500 個狀態的預算。超過時只畫違規路徑，若沒有違規則可能沒有
chart.mmd，不能據此認定模型無法檢查。
限制與權限
模型檢查不保證真實系統全面正確。VIEW、SYMMETRY 與約束會影響探索及呈現，約束外的狀態可能檢查規則卻不繼續探索或檢查死鎖。圖不是所有執行路徑的無條件保證。
此技能的圖片渲染另依上游 references/render.md，原文指定 Pele。本頁未查核該渲染文件，不提供未驗證的圖片指令。基本交付使用 Mermaid 文字，不宣稱本機已具備渲染器。執行模型、安裝依賴、連網及真實系統重現各需相應授權，不能延伸為付款或部署權限。