eventb-rossi/rossi
GitHub: eventb-rossi/rossi
一个 Rust 实现的 Event-B 形式化建模语言工具链，提供解析、静态检查、Rodin 双向转换及多编辑器 LSP 支持。
Stars: 3 | Forks: 2
# Rossi
面向 Event-B 形式化建模语言的 Rust 工具链：解析器、静态检查器、命令行工具以及 Language Server Protocol 实现。
## 概述
Event-B 是一种用于系统级建模和分析的形式化方法。
Rossi 覆盖了从编写到 Rodin 的完整路径：
- **`rossi`** — 基于 pest 的解析器和带有漂亮打印器（pretty-printer）的带类型 AST，支持在 `.eventb` 文本与原生 Rodin 的 `.buc` / `.bum` / `.zip` XML 格式之间进行双向转换。
- **`rossi-build`** — 静态检查器，在 AST 上层叠类型推断和良构性检查，并生成 Rodin 兼容的 `.bcc` / `.bcm` 已检查 XML，从而使得以文本编写的模型可以通过 Rodin 工具链进行往返处理。
- **`rossi-cli`** — 封装了解析器、检查器和语言服务器的 `rossi` 命令行工具。
- **`eventb-lsp`** — Language Server Protocol 实现，为 VS Code、Neovim、Emacs、Sublime Text 和 Zed 的编辑器扩展提供支持。
## 功能
**解析与双向转换**
- 完整的 Event-B 语法：上下文（contexts）、机器（machines）、事件（events）、细化（refinement）、见证（witnesses）
- 文本 ↔ 原生 Rodin XML (`.buc` / `.bum` / `.zip`)
- Unicode 和 ASCII 运算符约定（Rodin 键盘映射）
- 具有可配置缩进的漂亮打印器；解析 → 转换 → 打印
- 可选的 serde 支持，用于 AST 的 JSON 序列化
**静态检查与类型推断**
- 基于合一（unification）的类型推断（整数、布尔值、给定集合、幂集、笛卡尔积）
- 对守卫（guards）、动作（actions）、不变式（invariants）和公理（axioms）的良构性检查
- 跨 SEES / EXTENDS / REFINES 的交叉引用解析，并带有循环依赖检测
- `EB0xx` 诊断以及建议性 lint（死代码或未修改的变量、不完整的 INITIALISATION 等）
- 兼容 Rodin 的 `.bcc` / `.bcm` 已检查输出
**命令行工作流**
- `validate`、`import`、`export`、`fmt` 和 `build` 子命令
- 用于 CI 和 IDE 集成的文本、JSON 和 SARIF 2.1.0 诊断输出
**编辑器集成 (LSP)**
- 诊断、补全、悬停提示、转到定义、查找引用、重命名
- 格式化、语义高亮、代码操作、代码折叠和签名帮助
- 支持 VS Code、Neovim、Emacs、Sublime Text 和 Zed 的扩展
## 安装
从源码构建 `rossi` 命令行工具：
```
git clone https://github.com/eventb-rossi/rossi
cd rossi
cargo build --release -p rossi-cli
```
构建完成后，二进制程序将位于 `target/release/rossi`。独立语言服务器 (`eventb-language-server`) 的构建方式相同，只需指定 `-p eventb-lsp`。
要将 Rossi 作为库使用，请添加对 `rossi` crate 的依赖——它包含解析器、带类型的 AST、漂亮打印器以及 Rodin XML/ZIP 转换功能。运行 `cargo doc -p rossi --open` 查看 API 文档。
## CLI 工具
本项目提供了一个 `rossi` 命令行工具，它封装了解析器、`rossi-build` 静态检查器和语言服务器：
| 子命令 | 用途 |
|------------|---------|
| `validate` | 校验 `.eventb` 文件、Rodin `.zip` 归档或解压后的 Rodin 项目目录。 |
| `import` | 将 Rodin `.zip`/`.buc`/`.bum`/目录 导入为 `.eventb` 文本。 |
| `export` | 将 `.eventb`/`.txt`/目录 导出为 Rodin `.zip` 归档。 |
| `fmt` | 就地重新格式化 Event-B（运算符约定、缩进）。 |
| `build` | 对 Rodin 项目进行静态检查并生成 `.bcc` / `.bcm` 已检查 XML。 |
| `lsp` | 通过 stdio 运行 Rossi 语言服务器（等同于 `eventb-language-server` 二进制程序）。 |
### 校验 (Validate)
```
# 验证单个文件
rossi validate crates/rossi/examples/counter.eventb
# 验证多个文件
rossi validate crates/rossi/examples/*.eventb
# 用于工具集成的 JSON 输出
rossi validate --format json crates/rossi/examples/counter.eventb
# 面向 IDE 和代码扫描工具的 SARIF 输出
rossi validate --format sarif crates/rossi/examples/base-model.zip
# 安静模式（仅显示错误）
rossi validate --quiet crates/rossi/examples/*.eventb
# 遇到失败时继续
rossi validate --continue-on-error crates/rossi/examples/*.eventb
# 跳过 .zip 输入的语义检查，或跳过建议性 lint
rossi validate --no-semantic crates/rossi/examples/base-model.zip
rossi validate --no-lints crates/rossi/examples/base-model.zip
```
**文本输出：**
```
✓ crates/rossi/examples/counter.eventb - Valid Context 'counter_ctx'
✓ crates/rossi/examples/counter_machine.eventb - Valid Machine 'counter'
==================================================
Summary:
Total: 2
Passed: 2 ✓
Failed: 0 ✗
==================================================
```
**JSON 输出：**
```
[
{
"file": "crates/rossi/examples/counter.eventb",
"success": true,
"component_type": "Context",
"component_name": "counter_ctx"
}
]
```
对于 `.eventb` 文件，`validate` 会解析文本并报告组件结果。
对于 `.zip` 归档，除非设置了 `--no-semantic`，否则它还会运行 rossi-build 语义检查和建议性 lint；`--no-lints` 会保留语义检查，但会丢弃建议性的 lint 行。目录输入会被视为解压后的 Rodin 项目并需要进行语义检查，因此对于此类输入会拒绝 `--no-semantic`。
### 导入 (Rodin → Event-B 文本)
```
# 将 Rodin .zip 归档文件转换为 .eventb 文本文件（每个组件一个）
rossi import project.zip --output ./project
# 在生成的文本中使用 ASCII 操作符（以及自定义缩进）
rossi import project.zip --output ./project --ascii --indent=" "
# 合并所有组件到单个文件中，可选择指定顺序
rossi import project.zip --output project.eventb --merge=M0,C0
```
### 导出 (Event-B 文本 → Rodin 项目)
```
# 将 .eventb 文件目录打包成 Rodin .zip 归档文件
rossi export ./project --output project.zip
# 或者生成一个松散的 Rodin 项目目录
rossi export ./project --output ./rodin-project
```
`export` 会写入一个完整的 Rodin 项目：一个 `.project` 描述符（以输出路径命名）以及每个组件的原生 XML。使用 `.zip` 输出路径可生成可导入的归档，或使用目录输出路径生成松散的项目文件。归档始终使用 Unicode 运算符，这正是 Rodin 所期望的，因此 `export` 没有运算符约定选项——请使用 `rossi fmt` 来更改文本文件的约定。
### 格式化 (`fmt`)
`fmt` 会在*不*跨越 Rodin↔文本边界的情况下重新格式化 Event-B：它会对运算符约定（`--ascii`/`--unicode`，默认为 Unicode）和缩进（`--indent`）进行标准化。
```
# 将 ASCII 操作符文本转换为 Unicode（默认），打印到 stdout
rossi fmt model.eventb
# 就地重新格式化文件；明确选择操作符约定
rossi fmt -i ./project --ascii
rossi fmt -i model.eventb --indent=" "
# CI 检查门禁：如果存在任何未格式化的内容则以非零状态退出
rossi fmt --check ./project
# 将 Rodin 归档文件规范化为规范的 Unicode XML（保留其他条目）
rossi fmt project.zip -o normalized.zip
```
使用语言服务器的编辑器会使用相同的引擎在保存时进行格式化；`rossi fmt` 是其命令行和 CI 的对应工具。（Rodin 归档必须保持为 Unicode，因此对于 `.zip`/`.buc`/`.bum` 输入会拒绝 `--ascii`。）
### 构建 (静态检查 + Rodin 已检查 XML)
```
# 静态检查并将 .bcc / .bcm 生成到已检查的 Rodin .zip 中
rossi build project.zip --output project-checked.zip
# 或者将松散文件生成到目录中
rossi build project.zip --output ./out
```
### LSP
```
# 通过 stdio 启动语言服务器
rossi lsp
```
这与运行独立的 `eventb-language-server` 二进制文件完全相同；编辑器扩展可以调用任一形式。
### 退出代码
- `0` - 所有文件校验成功
- `1` - 一个或多个文件校验失败或未找到文件
## 示例
请查看 `crates/rossi/examples/` 目录以获取 Event-B 模型文件：
- `counter.eventb` / `counter_machine.eventb` - 简单计数器
- `library_ctx.eventb` / `library_machine.eventb` - 图书馆管理
- `traffic_light_ctx.eventb` / `traffic_light_machine.eventb` - 交通信号灯控制器
- `scheduler_ctx.eventb` / `scheduler_machine.eventb` - 进程调度器
- `refinement_abstract.eventb` / `refinement_concrete.eventb` - 细化示例
- `lambda_example_ctx.eventb` - Lambda 表达式和集合推导式
## 架构
本项目组织为一个包含四个公开 crate 的 Cargo 工作空间：
```
rossi/
├── crates/
│ ├── rossi/ # Core parser, AST, pretty-printer, Rodin XML
│ ├── rossi-build/ # Static checker / Rodin .bcc / .bcm builder
│ ├── rossi-cli/ # `rossi` command-line interface
│ └── eventb-lsp/ # Language Server Protocol implementation
└── editors/
├── vscode/ # VS Code extension
├── neovim/ # Neovim plugin
├── sublime/ # Sublime Text syntax (also used by bat, delta)
├── emacs/ # Emacs major mode
└── zed/ # Zed extension (LSP + tree-sitter grammar)
```
## 开发
```
# 启用 pre-commit 钩子（运行 cargo fmt、clippy、doc 和测试）
git config core.hooksPath .githooks
# 构建
cargo build
# 运行测试（全部、特定套件或带输出）
cargo test
cargo test --test full_models_test
cargo test -- --nocapture
# 生成 API 文档
cargo doc --open
```
## 语言服务器与 IDE 支持
`eventb-lsp` Language Server Protocol 实现为 Event-B 开发提供了现代 IDE 功能：
- **实时诊断** — 带有错误恢复的语法和语义错误提示
- **补全与悬停** — 上下文感知的关键字、运算符、标识符、代码片段
- **导航** — 转到定义、查找引用以及文档/工作区符号
- **重命名重构** — 带有验证的安全标识符重命名
- **格式化与语义高亮** — Unicode/ASCII 运算符、基于 AST 的 token
- **代码操作** — Unicode/ASCII 转换、提取常量、对子句排序
- **代码折叠、智能选择、签名帮助和文档链接**
- **跨文件解析** — 传递性的 SEES / REFINES / EXTENDS 遍历
### 编辑器扩展
扩展可在 `editors/` 目录中找到：
- **VS Code** (`editors/vscode/`) — 语法高亮、LSP 集成、代码片段以及输入时的 ASCII→Unicode 符号自动转换
- **Neovim** (`editors/neovim/`) — 文件检测、语法高亮、LSP 配置
- **Sublime Text** (`editors/sublime/`) — 语法高亮、LSP 集成以及输入时的 ASCII→Unicode 符号自动转换（也被 `bat` 和 `delta` 仅用于语法高亮）
- **Emacs** (`editors/emacs/`) — Event-B 主模式（major mode）
- **Zed** (`editors/zed/`) — LSP 集成加上用于高亮的 tree-sitter 语法；支持语义 token 覆盖
有关设置说明，请参阅每个编辑器的 README 和 INSTALL 文件。
## 相关项目
- [Rodin 平台](https://www.event-b.org/) - 基于 Eclipse 的 Event-B IDE
- [ProB](https://prob.de/) - Event-B 的动画演示和模型检查器
- [Event-B 文档](https://wiki.event-b.org/)
## 许可证
根据以下任一许可证授权：
- Apache License, Version 2.0 ([LICENSE-APACHE](LICENSE-APACHE) 或 http://www.apache.org/licenses/LICENSE-2.0)
- MIT license ([LICENSE-MIT](LICENSE-MIT) 或 http://opensource.org/licenses/MIT)
由您自行选择。
## 参考
- [Event-B 语言摘要](https://wiki.event-b.org/index.php/Event-B_Language)
- [Event-B 符号指南](https://wiki.event-b.org/index.php/Mathematical_Notation)
- [Rodin 键盘用户指南](https://wiki.event-b.org/index.php/Rodin_Keyboard_User_Guide)
- [Rodin 用户手册](https://wiki.event-b.org/index.php/Rodin_User_Manual)
## 作者
Rossi 贡献者
标签：Event-B, Rust, SOC Prime, 可视化界面, 开发工具, 形式化方法, 网络流量审计, 语言服务协议, 通知系统, 静态检查