開發 Event-B 模型
Event-B 模型是一種離散轉換系統。CONTEXT 包含固定的集合、常數與公理；MACHINE 包含變數、不變量與守護事件。本技能使用 ProB 檢查可達行為並驗證 well-definedness。它不編寫互動式 Rodin 證明。
1. 檢查必要工具
需要 rossi 0.1.8+ 與 eventb-animate 6.4+。檢查它們；切勿自行安裝或升級。如果任一工具缺失或版本過舊，請停止並要求使用者處理。
command -v rossi eventb-animate
rossi --version
eventb-animate --version
2. 建模前先界定範圍
在模型的 README.md 中撰寫簡短的需求文件：
- 系統邊界與明確的排除事項；
- 可觀測的事件及其執行者；
- 狀態類型與必須始終成立的安全屬性；
- 一個可達的成功情境、一個重要的禁止情境，以及終止狀態是否為刻意設計。
對於大型模型或多層次細化，請為每個層級新增一個需求到細化的對照表，每個層級一行：需求/標準條款、新增或取代的狀態、受影響的事件、不變量/黏合關係，以及驗證問題。若某層級的行中包含無關的關注點，請進行拆分。
預設使用一個 machine；將固定資料根據其獨立關注點拆分為多個小型 context。僅在隔離不同的需求或取代資料表示時才新增細化層級；請先寫下該理由與黏合不變量。細化是工具，而非必備儀式。
將每個模型放在自己的專案目錄中。每個元件使用一個檔案，檔案以元件命名。不要在 .eventb 檔案中加入散文式註解；將解釋保留在 README.md 中。
3. 僅閱讀相關的參考資料
| 需求 | 閱讀 |
|---|---|
精確的 .eventb 文法與動作形式 | references/syntax.md |
| 運算子或其優先順序 | references/math-toolkit.md |
| 協助選擇狀態、不變量或事件 | references/modelling.md |
| 真正的細化步驟，或規劃細化鏈 | references/refinement.md |
| 核心的反應式系統模式 | references/patterns.md 中對應的標題 |
| 離散時間、截止時間、模式或感測器/致動器 | references/patterns-control.md |
| 多參與者：拓撲、回合、共識、通道、長時間運作 | references/patterns-distributed.md |
| 存取控制、授權策略或保留 | references/patterns-security.md |
| 從後條件推導迴圈，或直譯器/ISA | references/patterns-algorithms.md |
| CLI 故障排除或條件式進階命令 | references/tooling.md |
| 最終設計審查 | references/best-practices.md |
僅在涉及 witness 或資料細化時，才從 examples/counter/ 開始；使用 examples/cars_on_bridge/ 學習事件拆分/收斂，使用 examples/array_maximum/ 學習終止演算法。不要為了開始一個小型單一 machine 模型而閱讀範例。
4. 撰寫最小可用模型
- 將載體集合與固定的策略/設定放在 context 中。
- 用第一個不變量為每個變數賦予型別，然後陳述實際的安全規則。
- 當感測或控制跨越系統邊界時，保持物理狀態、回報狀態與命令狀態的區別，並明確說明它們之間允許的延遲/不確定性。
- 讓
INITIALISATION滿足所有不變量。 - 為每個事件提供功能性需求、僅轉換需求以及不變量保持所需的所有守護；動作同時執行，未指派的變數保持不變。
- 當後續狀態目標必須觀察某個重要結果時，請在狀態中表示該結果。不要單純為了獲得覆蓋率而新增無操作事件；啟用的無操作會改變死鎖與活性行為。
- 保持有限檢查情境的小型化。寬鬆的非確定性參數會倍增操作啟用次數，可能使原本有限的檢查變得不完整或緩慢。
5. 執行核心閘門
從模型的專案目錄執行，而不是從包含不相關模型的上層目錄。建構一個 .zip 檔案；它包含動畫器所需的已檢查檔案。
rossi fmt -i .
rossi validate .
rossi fmt --check .
rossi build . -o /tmp/model.zip
eventb-animate --json /tmp/model-report.json /tmp/model.zip
eventb-animate wd /tmp/model.zip
僅在以下情況下接受結果：
- 驗證與建構沒有錯誤；即使命令以零退出，也將
missing or ill-typed witness與event is inaccurate視為失敗； - 報告中的
status: "ok"且無不變量違反； - 沒有非預期的死鎖；對於刻意設計的終止狀態，請記錄終止謂詞並使用
--no-deadlock重新執行，而非宣稱無死鎖； - 人類可讀的
Covered operations區塊包含預期的事件（報告 v3 不儲存操作覆蓋率，因此若需要稽核，請捕捉命令輸出）； - 對於有限的驗收情境，
completion.classification為complete； - 每個 well-definedness 義務都已履行。
退出碼為零並不代表完整性。如果有限模型被報告為不完整，請檢查原因與相關的 ProB 上限：
eventb-animate info --prefs /tmp/model.zip \
| rg 'MAX_(INITIALISATIONS|OPERATIONS)|DEFAULT_SETSIZE'
僅提升 MAX_INITIALISATIONS 或 MAX_OPERATIONS 至足以列舉已知的有限選擇，然後重新執行並要求 completion.classification: "complete"。對於刻意通用/無界限的模型，誠實報告有界限的結果，並在窮舉閘門重要時另外新增一個小型有限情境。
如果有細化鏈，請對每個層級使用 -m <machine> 重複模型檢查與 wd。
6. 在問題需要答案時，使用有針對性的證據
當問題是狀態謂詞是否可達時，使用目標追蹤：
eventb-animate -m M --goal '<predicate>' --no-invariant --no-deadlock \
--save /tmp/scenario.json /tmp/model.zip
eventb-animate replay -m M -t /tmp/scenario.json /tmp/model.zip
達到的目標會刻意退出碼為 1；要求 PERFECT 重播。在不變量或死鎖失敗時，請在修改模型前先儲存並重播其反例。
狀態目標無法證明無動作或僅有守護的事件已觸發：它可能在達到啟用狀態時立即停止。透過完整檢查的 Covered operations 區塊確認特定的轉換，或使用測試生成來鎖定：
eventb-animate testgen -m M --operations EVENT_NAME \
--out /tmp/scenario-traces /tmp/model.zip
僅在這些功能有特定用途時使用：
testgen：見證特定轉換或產生可重播的操作測試案例；它不是比窮舉檢查更強的閘門，且「未覆蓋」的結果不具結論性。--symbolic ic3|kinduction：無界限的不變量安全檢查；它不檢查死鎖、不報告事件覆蓋率，也不提供追蹤。po：檢查已包含.bpo/.bps證明的現有 Rodin 專案。import/export：Rodin 交換格式，非一般編寫流程。
有關這些條件式工作流程，請參閱 references/tooling.md。預設的 ProB 後端是正常的編寫路徑。
7. 以可讀的產出作為結束
交付 .eventb 檔案以及簡短的 README.md，其中包含範圍、模型形狀、以白話文說明的安全不變量、任何細化帳本、精確的檢查命令、完整性、事件覆蓋率、WD 結果，以及任何刻意進行的抽象化。乾淨的有界限執行意味著「在界限內未發現錯誤。」完整的有限執行僅證明被檢查的可達行為：它仍可能接受過強、非歸納的不變量，因為違反狀態是不可達的。它不滿足 Event-B 不變量/細化證明義務；僅適用的證明閘門才能支援該主張。請參閱 references/refinement.md，「模型檢查不是證明。」