🥮 mooncakes.io

    moonpetri

    Deterministic discrete Petri net modeling and reachability analysis for MoonBit

    petri-net
    reachability
    pnml
    model-checking
    moonbit
    Download zip
    Version
    0.1.4
    License
    MIT
    Repository
    Last updated
    19 hours ago
    Downloads
    19

    Dependencies

    #MoonPetri

    维护者：okmanba（GitHub 登录名 okMambaOut）

    MoonPetri 是用 MoonBit 编写的离线加权 Petri 网分析库。它从 place、transition、arc 和初始 token 出发，执行 firing，用有限 BFS 探索状态、重建最短轨迹并发现死锁。面向队列和并发资源建模，不是 HTTP 库或 GUI。

    #安装

    需要 MoonBit 工具链，项目锁定并验证 moonc v0.10.14+7d59c7ec9 及以上版本。CLI 文件读取依赖 moonbitlang/x。

    moon add okMambaOut/moonpetri@0.1.3

    源码运行：

    git clone https://github.com/okMambaOut/moonpetri.git
cd moonpetri
moon update
moon check --target wasm-gc --deny-warn
moon test --target wasm-gc
moon run examples/api-demo

    #功能

    • 构建并验证加权 place/transition 网
    • enabled、fire、fire_sequence
    • 有限 BFS 可达性、最短 firing 轨迹、死锁证据
    • 受限 PNML 导入导出
    • CLI：validate、explore、fire、report

    #示例

    let net = @petri.PetriNet::new()
    let free = net.add_place("free", 2).unwrap()
    let buffer = net.add_place("buffer", 0).unwrap()
    let produce = net.add_transition("produce").unwrap()
    let consume = net.add_transition("consume").unwrap()
    ignore(net.add_input(free, produce, 1).unwrap())
    ignore(net.add_output(produce, buffer, 1).unwrap())
    ignore(net.add_input(buffer, consume, 1).unwrap())
    ignore(net.add_output(consume, free, 1).unwrap())
    let result = @petri.reachable(net, net.initial_marking(), 100).unwrap()
    let report = @petri.analysis_report(net, result)

    CLI：

    moon run cmd/moonpetri -- validate examples/producer-consumer.pnml
moon run cmd/moonpetri -- explore examples/traffic-light.pnml
moon run cmd/moonpetri -- report examples/deadlock.pnml

    #边界

    不承诺完整 PNML 互操作、时间网、随机网、GUI 或系统安全认证。PNML 只接受单个 net，以及 name、initialMarking、inscription 文本字段。

    #许可证

    MIT。维护者为 okmanba，GitHub 账号为 okMambaOut。

    #验收检查

    仓库包含 GitHub Actions 持续集成，覆盖格式检查、四目标检查与构建、测试、CLI 场景和接口文件一致性。提交前可运行：

    python scripts/readiness.py --skip-native-runtime

    该参数只在没有系统 C 编译器的本地环境跳过 native 运行时；GitHub Actions 在 Ubuntu runner 上执行完整 native 检查。MoonCakes 发布由参与者按当前版本手动执行。

    AnalysisReport

    source
    pub struct AnalysisReport {
      states : Int
      edges : Int
      deadlocks : Int
      truncated : Bool
      max_tokens : Int
    }

    Summarize a bounded exploration.

    AnalysisReport::to_json

    source
    fn AnalysisReport::to_json(self : AnalysisReport) -> String

    Deterministic JSON summary; false boundedness is unknown when truncated.

    Arc

    source
    pub struct Arc {
      place : Int
      transition : Int
      weight : Int
    }

    Boundedness

    source
    pub(all) enum Boundedness {
      ProvenBounded
      Unknown
    } derive(Eq, 
    Debug    )

    A truncated finite search proves neither boundedness nor unboundedness.

    Boundedness::equal

    source
    fn Boundedness::equal(Boundedness, Boundedness) -> Bool

    Boundedness::not_equal

    source
    fn Boundedness::not_equal(x : Boundedness, y : Boundedness) -> Bool

    Boundedness::to_repr

    source

    Marking

    source
    pub struct Marking {
      // private fields
    } derive(Eq, 
    Debug    )

    Marking::equal

    source
    fn Marking::equal(Marking, Marking) -> Bool

    Marking::not_equal

    source
    fn Marking::not_equal(x : Marking, y : Marking) -> Bool

    Marking::to_repr

    source

    Marking::token

    source
    fn Marking::token(self : Marking, place : Int) -> Int?

    Marking::tokens

    source
    fn Marking::tokens(self : Marking) -> Array[Int]

    Return a defensive copy, never the marking's backing array.

    PetriError

    source
    pub(all) enum PetriError {
      EmptyName
      InvalidName
      NegativeTokens
      InvalidWeight
      InvalidPlace
      InvalidTransition
      InvalidMarking
      NotEnabled
      InvalidMaxStates
      DuplicateName(String)
      TokenOverflow
      SequenceFailed(Int, Int, PetriError)
      ParseError(String)
    } derive(Eq, 
    Debug    )

    PetriError::equal

    source
    fn PetriError::equal(PetriError, PetriError) -> Bool

    PetriError::not_equal

    source
    fn PetriError::not_equal(x : PetriError, y : PetriError) -> Bool

    PetriError::to_repr

    source

    PetriNet

    source
    pub struct PetriNet {
      // private fields
    }

    PetriNet::add_input

    source
    fn PetriNet::add_input(self : PetriNet, p : Int, t : Int, w : Int) -> Result[Unit, PetriError]

    PetriNet::add_output

    source
    fn PetriNet::add_output(self : PetriNet, t : Int, p : Int, w : Int) -> Result[Unit, PetriError]

    PetriNet::add_place

    source
    fn PetriNet::add_place(self : PetriNet, name : String, tokens : Int) -> Result[Int, PetriError]

    PetriNet::add_transition

    source
    fn PetriNet::add_transition(self : PetriNet, name : String) -> Result[Int, PetriError]

    PetriNet::find_pnml_transition

    source
    fn PetriNet::find_pnml_transition(self : PetriNet, id : String) -> Int?

    Resolve an original imported PNML ID, independently of display labels.

    PetriNet::find_transition

    source
    fn PetriNet::find_transition(self : PetriNet, name : String) -> Int?

    Resolve a transition's unique domain name, not its PNML serialization ID.

    PetriNet::initial_marking

    source
    fn PetriNet::initial_marking(self : PetriNet) -> Marking

    PetriNet::new

    source
    fn PetriNet::new() -> PetriNet

    PetriNet::place_count

    source
    fn PetriNet::place_count(self : PetriNet) -> Int

    PetriNet::place_name

    source
    fn PetriNet::place_name(self : PetriNet, id : Int) -> String?

    PetriNet::transition_count

    source
    fn PetriNet::transition_count(self : PetriNet) -> Int

    PetriNet::transition_name

    source
    fn PetriNet::transition_name(self : PetriNet, id : Int) -> String?

    PetriNet::validate

    source
    fn PetriNet::validate(self : PetriNet) -> Result[Unit, Array[PetriError]]

    Verify model invariants without modifying the net.

    ReachabilityResult

    source
    pub struct ReachabilityResult {
      edges : Int
      truncated : Bool
      max_tokens : Int
      // private fields
    }

    ReachabilityResult::state_count

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

    ReachabilityResult::states

    source

    Return detached state snapshots in BFS order.

    Transition

    source
    type Transition

    analysis_report

    source
    fn analysis_report(net : PetriNet, r : ReachabilityResult) -> AnalysisReport

    boundedness

    source
    fn boundedness(result : ReachabilityResult) -> Boundedness

    deadlock_traces

    source
    fn deadlock_traces(result : ReachabilityResult) -> Array[(Marking, Array[Int])]

    Deadlock witnesses and their shortest traces in discovery order.

    deadlocks

    source
    fn deadlocks(_net : PetriNet, r : ReachabilityResult) -> Array[Marking]

    enabled

    source
    fn enabled(net : PetriNet, m : Marking, t : Int) -> Bool

    enabled_transitions

    source
    fn enabled_transitions(net : PetriNet, m : Marking) -> Array[Int]

    fire

    source
    fn fire(net : PetriNet, m : Marking, t : Int) -> Result[Marking, PetriError]

    fire_sequence

    source
    fn fire_sequence(net : PetriNet, m : Marking, seq : Array[Int]) -> Result[Marking, PetriError]

    is_bounded

    source
    fn is_bounded(r : ReachabilityResult) -> Bool

    marking

    source
    fn marking(tokens : Array[Int]) -> Marking

    Create a marking with explicit token values.

    marking_fingerprint

    source
    fn marking_fingerprint(m : Marking) -> String

    Return a stable textual fingerprint for diagnostics and snapshots.

    observed_place_maxima

    source
    fn observed_place_maxima(result : ReachabilityResult) -> Array[Int]

    Observed maxima per place, not proven bounds unless search is complete.

    parse_pnml

    source
    fn parse_pnml(input : String) -> Result[PetriNet, Array[PetriError]]

    Parse the documented flat, namespace-free PNML subset. First error wins.

    reachable

    source
    fn reachable(net : PetriNet, start : Marking, max : Int) -> Result[ReachabilityResult, PetriError]

    run_command

    source
    fn run_command(command : String, input : String, args : Array[String]) -> Result[String, Array[PetriError]]

    Pure CLI engine: file access and process exit live in cmd/moonpetri.

    serialize_pnml

    source
    fn serialize_pnml(net : PetriNet) -> String

    Emit canonical flat PNML with generated IDs and preserved model order.

    shortest_trace

    source
    fn shortest_trace(r : ReachabilityResult, target : Marking) -> Array[Int]?

    Source Files

    Powered by MoonBit

    Site sourceReport issuePackagesBuild queueSkillsStatistics

    © 2026 mooncakes.io