开发 Event-B 模型
Event-B 模型是一个离散过渡系统。CONTEXT 保存固定集合、常量和公理；MACHINE 保存变量、不变式和守卫事件。本技能使用 ProB 检查可达行为，并使用良好定义性门。它不处理交互式 Rodin 证明。
1. 检查所需工具
需要 rossi 0.1.8+ 和 eventb-animate 6.4+。检查它们；永远不要自行安装或升级。如果任一缺失或版本更旧，请停止并让用户自行处理。
command -v rossi eventb-animate
rossi --version
eventb-animate --version
2. 建模前先明确范围
在模型的 README.md 中编写简短的需求说明：
- 系统边界和明确排除项；
- 可观察的事件及其执行者；
- 状态类型以及必须始终成立的安全性属性；
- 一个可达的成功场景，一个重要的禁止场景，以及终止状态是否为有意为之。
对于规模较大的模型或任何多层精化，请为每个层级添加一行需求到精化记录表： 需求/标准子句、新增或替换的状态、受影响的事件、不变式/粘合关系以及验证问题。如果某一层包含不相关的关注点，则将其拆分。
默认使用一个机器；将固定数据拆分为多个小型上下文，每个上下文处理其独立关注点。仅当某个精化层级隔离了独立的需求或替换了数据表示时才添加它；先编写该原因和粘合不变式。精化是一种工具，不是必需的仪式。
将每个模型放在自己的项目目录中。每个组件一个文件，文件名与组件名一致。不要在 .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 |
仅当涉及见证者或数据精化时从 examples/counter/ 开始；对于事件拆分/收敛使用 examples/cars_on_bridge/；对于终止算法使用 examples/array_maximum/。不要仅仅为了开始一个小的单机模型而阅读示例。
4. 编写最小有用的模型
- 将载体集和固定策略/配置放在一个上下文中。
- 使用第一个不变式对每个变量进行类型化，然后陈述实际的安全规则。
- 当传感或控制跨越系统边界时，保持物理状态、上报状态和命令状态相互独立，并说明它们之间允许的延迟/不确定性。
- 使
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； - 每个良好定义性义务都已解除。
退出码为零并不能证明完备性。如果有限模型报告为 incomplete，请检查原因以及相关的 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，“模型检查不是证明”。