如何远程操作 Apalache：Shai RPC 服务与 TransitionExecutor 接口完全指南

Apalache 是 TLA+ 和 Quint 语言的符号模型检查器，它的 server 模式可以常驻后台，通过 Shai gRPC 服务和 JSON-RPC 探索器对外暴露 API，让你用任意编程语言远程驱动 TransitionExecutor 进行交互式符号执行，省去重复启动 JVM 的成本。本文带你快速理解 Apalache API 的两套远程交互方式并上手调用。

🧭 一、Apalache 服务器模式概览

命令行子命令 apalache-mc server 提供两种服务器实现（见 ServerCmd.scala）：

server-type	实现	协议	定位
checker（默认）	Shai（shai/ 模块）	gRPC + protobuf	官方 RPC 服务，暴露 TransEX 与命令执行能力
explorer	JSON-RPC 探索器（json-rpc/ 模块）	JSON-RPC over HTTP	轻量替代，专注 TLA+ 符号探索，语言无关

两者默认都监听 8822 端口，可通过 --port 或配置文件中的 "server" 分组修改（详见 config.md）。

📡 二、Shai：gRPC 服务的两大服务

Shai 是 "Server for Human-Apalache Interaction" 的缩写，基于 ZIO-gRPC 构建。API 按版本隔离（当前为 v1），服务注册中心是 RpcServer.scala，接口契约由两份 protobuf 文件定义：

1. TransExplorer 服务：交互式驱动 TransitionExecutor

定义在 transExplorer.proto，核心 RPC 如下：

• openConnection：创建会话，返回一个 UUID 形式的 Connection，后续所有请求都需携带它
• loadModel：提交 TLA+ 模块源码（内存中传字符串），服务器解析后返回 Apalache JSON IR
• ping：健康检查空操作

实现位于 TransExplorerService.scala，它区分了协议级错误（如缺少连接 ID，返回 gRPC Status 码）和应用级错误（如解析失败，封装在 TransExplorerError 消息中），排错时值得留意。

2. CmdExecutor 服务：无状态的 CLI 远程执行

定义在 cmdExecutor.proto，仅有一个 run RPC，但支持 PARSE、CHECK、TYPECHECK、TLA 四种子命令——相当于把 Apalache 命令行能力搬进 RPC，输入输出均为内存中的 JSON，特别适合 CI/CD 集成。实现见 CmdExecutorService.scala。

⚠️ 远程请求只接受内存源（"kind": "string"），会拒绝文件路径和会写文件的 Z3 调优项，这是出于安全考虑。

🚂 三、TransitionExecutor 编程接口详解

TransitionExecutor（绰号 "T-Rex"）是 Apalache 的通用符号转移执行器，顺序与并行模型检查器都复用它的逻辑。它的编程接口可以概括为五步循环：

1. initializeConstants：用常量初始化表达式固定 CONSTANTS
2. prepareTransition：把一个 TLA+ 动作翻译成 SMT 约束并编号
3. assumeTransition：假设某个已准备的转移发生
4. assertState：向当前符号状态（frame）追加断言
5. evaluate：对当前 SMT 模型求值表达式，获得具体状态

配合 stepNo（当前步数）与 execution（累积的符号执行）即可读取进度。它还是 Recoverable 接口，支持快照与回滚——这正是交互式探索"走错路能回头"的关键。完整设计动机可阅读 RFC-010 迁移探索服务器 与 shai/README.md。

🌐 四、JSON-RPC 探索器：12 个方法快速清单

json-rpc/ 模块是当前主推的轻量方案，用 Jetty + Jackson 实现（见 JsonRpcServer.scala），支持 gzip/zstd 压缩。完整方法文档在 json-rpc/README.md，快速清单：

方法	作用	典型时机
health	存活检查	启动后验证
loadSpec	加载并解析规格，返回 sessionId	会话开始
disposeSpec	释放会话与 SMT 求解器	会话结束
rollback	回滚到更早的 snapshotId	走错分支时
assumeTransition	准备并假设某个转移	每步之前
nextState	推进到下一个符号状态	转移之后
checkInvariant	检查不变式，违例时返回 ITF 反例	推进后
query	查询 TRACE / STATE / OPERATOR	任意
nextModel	枚举下一个不同模型	反例遍历
assumeState	对状态变量加等式约束	定向探索
compact	用具体状态压缩长符号轨迹	约 200–300 步后
applyInOrder	单轮询按序批量执行多步	降低网络开销

🚀 五、最快启动步骤与调用示例

第 1 步：启动服务器

apalache-mc server --server-type=explorer --port=8822

第 2 步：健康检查

curl -X POST http://localhost:8822/rpc \
  -H "Content-Type: application/json" \
  -d '{"jsonrpc":"2.0","method":"health","params":{},"id":1}'

返回 {"result":{"status":"OK"}} 即就绪。

第 3 步：加载规格并探索。loadSpec 接收 base64 编码的模块源码数组，可附带 init、next、invariants、exports 参数；随后用 assumeTransition → nextState → checkInvariant 循环推进。所有返回都携带 sessionId 与 snapshotId，回滚时直接引用即可。

🗂 六、架构位置与延伸阅读

RPC 服务位于整体架构的顶层入口，架构示意图 展示了从输入解析、类型检查到模型检查器的完整流水线——服务器模式正是把这条流水线"长开"供外部调用：

• 服务器配置参考：docs/src/apalache/config.md
• Shai 服务说明：shai/README.md
• 探索器方法文档：json-rpc/README.md
• 设计 RFC：docs/src/adr/010rfc-transition-explorer.md

小结：需要严格类型契约和多语言 gRPC 客户端时选 Shai（checker）；需要快速、语言无关地做符号探索与反例枚举时选 JSON-RPC（explorer）。两者共享同一套 TransitionExecutor 内核，掌握它的方法循环，你就掌握了远程驱动 Apalache 的全部关键。