🥮 mooncakes.io

    moonctl

    Finite-state CTL model checking with replayable witnesses and counterexamples

    model-checking
    ctl
    formal-verification
    Download zip
    Version
    0.2.0
    License
    Apache-2.0
    Repository
    Last updated
    10 hours ago
    Downloads
    3

    Dependencies

    #MoonCTL

    MoonCTL 是一个用 MoonBit 编写的 CTL（计算树逻辑）有限状态模型检查库。给它一个完整的状态转换图和一条性质，它会判断初始状态是否满足性质，并为常见的可达性与活性结果给出可重放的路径。

    它适合检查工作流、协议、工具调用及其他可枚举状态系统。它检查你提供的模型，不会从任意 MoonBit 程序自动提取状态图。

    能力说明
    CTL 检查支持 EX、AX、EF、AF、EG、AG、E[p U q]、A[p U q]
    结果解释对支持的公式返回有限路径或带循环入口的路径；也可输出 JSON
    图形导出将模型导出为 Graphviz DOT，并标红见证或反例路径
    建模方式从 JSON、状态 ID 与转移，或带预算的转换函数构建有限图
    运行目标核心库通过 wasm、wasm-gc、js、native 检查；命令行示例使用 native

    #快速体验

    需要 MoonBit 工具链。克隆仓库并进入根目录后运行：

    moon run --target native cmd/main -- examples/buggy.json 'AG !double_charge'

    预期输出：

    FAIL: AG !double_charge
states=4 satisfying=1
counterexample (shortest path):
  new
  --charge--> charged_once
  --retry_without_idempotency--> charged_twice

    性质失败时退出码为 1。修复后的工作流可运行：

    moon run --target native cmd/main -- examples/fixed.json 'AG !double_charge'
moon run --target native cmd/main -- examples/fixed.json 'AF completed'

    两条性质都应得到 PASS。独立可执行文件对模型或公式输入错误返回 2；moon run 是开发包装命令，可能把非零退出码统一报告为 1。

    多个性质可以写入一份套件文件，每行一个 CTL 公式，空行和 # 注释会被忽略：

    moon run --target native cmd/main -- --suite examples/buggy.json examples/payment.suite

    命令会逐项输出 PASS / FAIL 和汇总；全部通过时退出码为 0，任一性质失败时为 1，文件或公式错误时为 2。

    需要展示状态图时，可导出 Graphviz DOT（此命令本身不需要安装 Graphviz）：

    moon run --target native cmd/main -- --dot examples/buggy.json 'AG !double_charge' > buggy.dot

    初始状态画成双圈，检查结果给出的见证或反例转移标成红色。库用户也可以调用 model.to_dot() 或 model.to_dot_with_trace(report)。

    机器可读输出使用 --json：

    moon run --target native cmd/main -- --json examples/buggy.json 'AF completed'

    输出是单个 JSON 对象：formula 为输入公式，report 含 schema_version、holds、state_count、satisfying_count、satisfying_states、trace_role、trace 和 loop_start。satisfying_states[i] 对应输入模型第 i 个状态；循环路径的最后一步重访 loop_start 指向的步骤。输入错误时 JSON 模式输出 {"error":"..."}。

    #作为库使用

    本模块名为 length-super/moonctl。使用 API 可直接构造状态和转移，无需 JSON：

    let states : Array[@moonctl.State] = [
      { id: "new", labels: [] },
      { id: "done", labels: ["completed"] },
    ]
    let edges : Array[@moonctl.Edge] = [
      { from: 0, to: 1, action: "finish" },
    ]
    let model = match @moonctl.Model::new(states, edges, initial=0) {
      Ok(m) => m
      Err(_) => abort("invalid model")
    }
    let property = @moonctl.parse("EF completed")
    let report = @moonctl.check(model, property)
    assert_true(report.holds())

    在调用方 moon.pkg 中导入 "length-super/moonctl" @moonctl。可用 moon add length-super/moonctl 添加依赖。Model::new 验证非空状态、初始索引、状态 ID 唯一性和转移索引。parse 与 load_model_json 分别以 ParseError 和 ModelJsonError 报告输入问题。Report 提供 holds()、state_count()、satisfying_count()、satisfies_at(index)、trace()、trace_role()、loop_start() 和 to_json()。

    #用状态 ID 构图

    不必手工维护数字索引。Model::from_named 接受同样的状态列表和 NamedEdge，用状态 ID 指定初态及转移；未知或重复的 ID 会返回错误。

    ///|
    let states : Array[@moonctl.State] = [
      { id: "queued", labels: [], },
      { id: "done", labels: ["completed"], },
    ]

    ///|
    let edges : Array[@moonctl.NamedEdge] = [
      { from: "queued", to: "done", action: "finish", },
    ]

    ///|
    let model = @moonctl.Model::from_named(states, edges, "queued")

    #从转换函数探索

    explore 从初态按广度优先调用转换函数，只纳入可达状态。调用方必须给出 max_states 和 max_edges；前者含初态，后者统计显式转移，不统计死端的隐式自环。刚好达到预算仍可能完成；只有还需发现新状态或转移时才返回 Incomplete。状态 ID 再次出现时，其标签集合必须一致。Incomplete 不含 Model，因此不能把未探索的行为当成性质通过。

    let result = @moonctl.explore(
      initial,
      state => transitions_from(state),
      max_states=1000,
      max_edges=5000,
    )
    match result {
      Ok(Complete(model)) => {
        let report = @moonctl.check(model, @moonctl.parse("AG !double_charge"))
        println("holds=\{report.holds()}")
      }
      Ok(Incomplete(limit, states, edges)) =>
        println("incomplete: \{Repr(limit)}, \{states} states, \{edges} edges")
      Err(error) => println("invalid exploration: \{Repr(error)}")
    }

    完整可运行版本：moon run --target wasm-gc examples/explore。转换回调必须对同一状态 ID 稳定地返回该状态的全部可能转移；若历史会改变后续行为，应把相关历史纳入状态 ID。预算约束的是 MoonCTL 保存的图，不限制回调内部自行分配的内存。

    #JSON 模型格式

    examples/buggy.json 展示完整格式：

    {
  "initial": 0,
  "states": [
    {"id": "new", "labels": ["safe"]},
    {"id": "charged", "labels": ["safe"]}
  ],
  "edges": [
    {"from": 0, "to": 1, "action": "charge"}
  ]
}

    状态和转移索引从 0 开始。每个状态的 id 必须唯一；labels 是在该状态为真的原子命题。action 用于输出路径。无出边的状态按隐式 <stutter> 自环解释，使每条计算路径无限延续。输入图必须列出系统的全部相关状态和转移；缺失的行为无法被检查出来。

    #公式与语义

    公式含义
    p, true, false原子命题与布尔常量
    !p, p & q, p \| q否定、合取、析取
    EX p, AX p存在 / 所有下一状态满足 p
    EF p, AF p存在 / 所有路径最终到达 p
    EG p, AG p存在 / 所有路径始终满足 p
    E[p U q], A[p U q]存在 / 所有路径保持 p 直到 q

    ! 高于 &，& 高于 |；可用括号分组。U 是强直到：必须最终到达右式。标识符支持 ASCII 字母、数字、下划线、连字符、点和冒号；true、false、EX 等关键字保留。

    求值采用有限图固定点算法，holds() 只报告初始状态的真值。satisfying_count() 是全图中满足该公式的状态数，可能包括初始状态不可达的状态。Model::unreachable_states() 会按输入顺序列出无法从初态到达的状态 ID，便于检查建模范围。

    对顶层 EX p、EF p、E[p U q] 的成功，以及 AX p、AG p 的失败，trace() 返回最短有限见证或反例。A[p U q] 失败时优先返回最短的有限违反路径；若失败只能由无限等待造成，则返回一条循环路径。AF p 的失败和 EG p 的成功也返回循环路径；loop_start() 指向第一次出现的循环入口，末尾步骤是重访该状态。其他结果的 trace() 暂为空；这不影响真假判定。循环路径保证有效，但未优化为最短。

    #验证与演示

    moon check --target all --deny-warn
moon build --target all
moon test --target wasm-gc --deny-warn
moon test --target native --deny-warn
moon run --target wasm-gc examples/explore

    测试中另有一个独立参考求值器：它在小图上逐条枚举简单路径并识别循环，与正式求值器的前驱固定点算法分开；测试对照每个状态的真值，并重放所有生成的有限和循环路径。支付、分布式锁和 Agent 审批的可复现场景见 docs/scenarios.md，三分钟演示脚本见 docs/demo.md。调研依据与竞品比较见 mooncake-ecosystem-analysis.md、github-ecosystem-analysis.md 和 project-proposal.md。

    #当前边界

    • 使用显式有限图，单个时序子公式的固定点求值按状态和转移数线性增长；按需探索有明确预算，手工构图仍由调用方控制规模；尚无符号状态压缩。
    • 模型是否忠实于业务系统由建模者负责；PASS 只适用于已给出的图与标签。
    • CLI 使用 native 后端；核心库已按 MoonBit 的 wasm、wasm-gc、js、native 目标检查。

    #项目与来源

    MoonCTL 是独立实现的 CTL 显式状态模型检查库。仓库中的支付流程模型、测试图和演示脚本为本项目编写；生态调研中提及的 MoonBDD、MoonPetri 和 moon prove 是相邻项目，并非本项目的代码来源。源码以 Apache-2.0 发布。

    项目维护者：length-super。在 GitHub Issues 反馈问题或提出改进建议时，请附上最小状态图、CTL 公式、实际输出和预期结果。当前公开 API 以 pkg.generated.mbti 为准。

    ModelJsonError

    source
    pub(all) suberror ModelJsonError {
      InvalidJson
      MissingField(String)
      WrongType(String)
      InvalidGraph(ModelError)
    } derive(
    Debug    )

    ParseError

    source
    pub(all) suberror ParseError {
      UnexpectedEnd
      UnexpectedToken(String)
      ExpectedToken(String)
      InvalidCharacter(Char)
    } derive(
    Debug    )

    Edge

    source
    pub(all) struct Edge {
      from : Int
      to : Int
      action : String
    } derive(
    Debug    )

    A directed transition. action is used in counterexample traces.

    Edge::to_repr

    source

    Exploration

    source
    pub enum Exploration {
      Complete(Model)
      Incomplete(ExploreLimit, Int, Int)
    }

    Incomplete deliberately contains no Model. A partial graph cannot be passed to check and mistaken for a proof about the whole system.

    ExploreError

    source
    pub(all) enum ExploreError {
      InvalidBudget(Int, Int)
      ConflictingState(String)
      InvalidExploredGraph(ModelError)
    } derive(
    Debug    )

    ExploreLimit

    source
    pub(all) enum ExploreLimit {
      StateBudgetReached
      EdgeBudgetReached
    } derive(
    Debug    )

    Formula

    source
    pub enum Formula {
      True
      False
      Atom(String)
      Not(Formula)
      And(Formula, Formula)
      Or(Formula, Formula)
      EX(Formula)
      AX(Formula)
      EF(Formula)
      AF(Formula)
      EG(Formula)
      AG(Formula)
      EU(Formula, Formula)
      AU(Formula, Formula)
    } derive(
    Debug    )

    CTL formulas over state labels. Every temporal operator is path-quantified.

    Formula::to_repr

    source

    Model

    source
    pub struct Model {
      states : Array[State]
      outgoing : Array[Array[Edge]]
      incoming : Array[Array[Int]]
      initial : Int
    }

    A complete, finite transition system. Dead-end states have an implicit self-loop when interpreting CTL, following the usual total Kripke semantics.

    Model::from_named

    source
    fn Model::from_named(states : Array[State], edges : Array[NamedEdge], initial : String) -> Result[Model, NamedModelError]

    Build a finite graph using stable state IDs. Every named transition must refer to a declared state. A terminal state receives a stutter self-loop.

    Model::has_label

    source
    fn Model::has_label(self : Model, index : Int, label : String) -> Bool

    Model::initial

    source
    fn Model::initial(self : Model) -> Int

    Model::new

    source
    fn Model::new(states : Array[State], edges : Array[Edge], initial~ : Int) -> Result[Model, ModelError]

    Model::state_count

    source
    fn Model::state_count(self : Model) -> Int

    Model::state_id

    source
    fn Model::state_id(self : Model, index : Int) -> String?

    Model::successors

    source
    fn Model::successors(self : Model, index : Int) -> Array[Edge]

    Model::to_dot

    source
    fn Model::to_dot(self : Model) -> String

    Export the explicit transition graph as Graphviz DOT. The initial state is a double circle, and terminal stutter loops are shown explicitly.

    Model::to_dot_with_trace

    source
    fn Model::to_dot_with_trace(self : Model, report : Report) -> String

    Export the graph with a check result's witness or counterexample edges in red. The report must have been produced from this model.

    Model::unreachable_states

    source
    fn Model::unreachable_states(self : Model) -> Array[String]

    Return state IDs that cannot be reached from the initial state, in the model's input order. This helps spot states that cannot affect a verdict.

    ModelError

    source
    pub(all) enum ModelError {
      EmptyStates
      InvalidInitial(Int)
      DuplicateState(String)
      InvalidEdge(Int, Int)
    } derive(
    Debug    )

    NamedEdge

    source
    pub(all) struct NamedEdge {
      from : String
      to : String
      action : String
    } derive(
    Debug    )

    A transition identified by state IDs instead of numeric indices.

    NamedEdge::to_repr

    source

    NamedModelError

    source
    pub(all) enum NamedModelError {
      DuplicateName(String)
      UnknownState(String)
      InvalidModel(ModelError)
    } derive(
    Debug    )

    Report

    source
    pub struct Report {
      holds : Bool
      state_count : Int
      satisfying_count : Int
      satisfying : Array[Bool]
      trace : Array[TraceStep]
      trace_role : String
      loop_start : Int?
    }

    Report::holds

    source
    fn Report::holds(self : Report) -> Bool

    Report::loop_start

    source
    fn Report::loop_start(self : Report) -> Int?

    If a trace ends by revisiting a state, this is the index of its first occurrence. The final step closes the infinite loop.

    Report::satisfies_at

    source
    fn Report::satisfies_at(self : Report, index : Int) -> Bool?

    Whether a state satisfies the formula. Indices follow the input model's state order; out-of-range indices return None.

    Report::satisfying_count

    source
    fn Report::satisfying_count(self : Report) -> Int

    Report::state_count

    source
    fn Report::state_count(self : Report) -> Int

    Report::to_json

    source
    fn Report::to_json(self : Report) -> Json

    Serialize a check result for CI and other tools. State truth values use the same index order as the model supplied to check.

    Report::trace

    source
    fn Report::trace(self : Report) -> Array[TraceStep]

    Returns a defensive copy of the witness/counterexample available for the top-level formula. Empty means no path is exposed. Finite paths are shortest under their formula constraints; looping paths end with a repeated state identified by loop_start.

    Report::trace_role

    source
    fn Report::trace_role(self : Report) -> String

    State

    source
    pub(all) struct State {
      id : String
      labels : Array[String]
    } derive(
    Debug    )

    One state in an explicitly enumerated finite transition system.

    State::to_repr

    source

    TraceStep

    source
    pub(all) struct TraceStep {
      state : String
      via : String?
    } derive(
    Debug    )

    A path from the initial state to an observed state. via is the transition taken from the preceding step; it is None for the initial state.

    TraceStep::to_repr

    source

    Transition

    source
    pub(all) struct Transition {
      to : State
      action : String
    } derive(
    Debug    )

    A generated transition. Returning the same state ID with different labels is an error, because atomic propositions must be stable for each state.

    Transition::to_repr

    source

    check

    source
    fn check(model : Model, formula : Formula) -> Report

    Evaluate a CTL formula at the model's initial state. Includes paths for top-level EX/AX/EF/AF/EG/AG/EU/AU when one path can witness the result. Universal until failure may be a finite violation or an infinite loop avoiding the goal.

    explore

    source
    fn explore(initial : State, next : (State) -> Array[Transition], max_states~ : Int, max_edges~ : Int) -> Result[Exploration, ExploreError]

    Explore reachable states in breadth-first order. Limits include the initial state and explicit transitions; synthesized stutter edges do not consume the edge budget. Exactly reaching a limit can still be complete. The callback receives a defensive copy of each discovered state.

    load_model_json

    source
    fn load_model_json(source : String) -> Model raise ModelJsonError

    Parse an explicit finite graph from JSON. The input is validated before any temporal formula is checked.

    parse

    source
    fn parse(source : String) -> Formula raise ParseError

    Source Files

    Powered by MoonBit

    Site sourceReport issuePackagesBuild queueSkillsStatistics

    © 2026 mooncakes.io