mseve/bigrapher

mseve/bigrapher镜像说明

镜像概述

mseve/bigrapher是一个专注于Bigraph模型的工具集合，提供编程式操作、分析与模拟能力，适用于形式化系统建模、反应系统验证等场景，支持与概率模型检查器PRISM的集成，助力学术研究与工程实践。

核心功能

1. bigraph库：支持Bigraph、反应规则及BRS系统的编程式操作，涵盖共享Bigraph、概率/随机规则、优先级规则、状态空间探索、PRISM导出等功能，基于高效SAT匹配引擎。
2. bigrapher工具：命令行工具，计算BRS转换系统并导出至PRISM或图形格式。
3. big_json编解码器：实现Bigraph结构与JSON格式的互转，提供JSON接口访问匹配引擎。
4. 求解器绑定：包含MiniSAT（SAT求解器）与MiniCARD（基数求解器）的绑定。

使用场景

• 形式化系统建模与验证（如通信代理、分布式系统）；
• 反应系统的模拟与状态空间分析；
• Bigraph模型转换为PRISM格式进行安全性分析；
• 学术研究中Bigraph理论的实践验证。

配置与部署

构建方式

使用dune（版本≥2）构建：

bash
dune build --profile=release

安装至本地opam仓库：

bash
dune install --profile=release

Docker部署示例

1. 拉取镜像：

bash
docker pull docker.xuanyuan.run/mseve/bigrapher

2. 交互式运行容器：

bash
docker run -it --rm docker.xuanyuan.run/mseve/bigrapher /bin/bash

3. 使用bigrapher工具：

bash
bigrapher --help  # 查看命令帮助

参考资料

• Robin Milner. 《The space and motion of communicating agents》. Cambridge University Press (2009).
• Michele Sevegnani & Muffy Calder. 《Bigraphs with sharing》. Theoretical Computer Science 577 (2015).
• PRISM模型检查器：[***]
• MiniSAT求解器：https://github.com/niklasso/minisat

版权与许可

版权所有2012-2020 Glasgow Bigraph Team，遵循简化BSD许可证。 ===FULL_DESC===