movesrwth/stormpy

Stormpy Docker镜像文档

镜像概述和主要用途

Stormpy是概率模型检查器Storm的Python绑定库，该Docker镜像封装了Stormpy及其依赖环境，提供便捷的部署方式。通过Python接口，用户可高效利用Storm的核心功能，对马尔可夫链、马尔可夫决策过程、概率自动机等概率模型进行建模、验证与分析，广泛应用于形式化方法、系统验证及概率系统研究领域。

核心功能和特性

• Storm核心集成：完整集成Storm模型检查器的功能，支持多种概率模型的解析与分析
• Python友好API：提供简洁易用的Python接口，降低概率模型检查的使用门槛
• 丰富算法支持：包含概率可达性分析、期望奖励计算、稳态概率计算等多种模型检查算法
• 模型表示灵活：支持PRISM语言、JANI格式等多种输入格式，便于模型定义与导入
• 跨平台兼容：通过Docker容器化，确保在不同操作系统环境下的一致性运行

使用场景和适用范围

• 学术研究：概率系统验证、形式化方法研究、随机算法分析等领域的科研工作
• 工业应用：可靠性工程、网络协议验证、自动驾驶系统安全性分析等关键系统的概率行为评估
• 教学实践：形式化方法课程中概率模型检查的教学演示与实验

使用方法和配置说明

基本使用流程

1. 拉取镜像
   从Docker仓库拉取Stormpy镜像：

   bash
   docker pull movesrwth/stormpy:latest
   

2. 运行容器
   启动容器并挂载本地工作目录（将/path/to/local/code替换为实际代码目录）：

   bash
   docker run -it --rm -v /path/to/local/code:/app movesrwth/stormpy bash
   

3. 执行Python脚本
   在容器内运行包含Stormpy代码的Python脚本：

   bash
   cd /app
   python your_script.py
   

Python代码示例

以下是使用Stormpy进行简单概率模型检查的示例（your_script.py）：

python
import stormpy

# 创建一个简单的马尔可夫链模型
model = stormpy.build_model_from_prism_string("""
dtmc
module counter
    x : [0..2] init 0;
    [] x=0 -> 0.5:x'=1 + 0.5:x'=2;
    [] x=1 -> 1.0:x'=2;
    [] x=2 -> 1.0:x'=2;
endmodule
""")

# 定义待检查的属性（到达状态x=2的概率）
properties = stormpy.parse_properties("P=? [F x=2]", model)

# 进行模型检查
result = stormpy.model_checking(model, properties[0])

# 输出结果
print(f"到达x=2的概率: {result.value()}")

高级配置

环境变量

• STORMPY_LOG_LEVEL：设置日志级别，可选值：DEBUG、INFO、WARNING、ERROR，默认INFO
• STORMPY_TIMEOUT：模型检查超时时间（秒），默认无超时

示例：设置调试日志级别并运行容器

bash
docker run -it --rm -e STORMPY_LOG_LEVEL=DEBUG -v /path/to/code:/app movesrwth/stormpy bash

持久化数据

通过挂载卷保存模型文件、分析结果等数据：

bash
docker run -it --rm -v /local/models:/app/models -v /local/results:/app/results movesrwth/stormpy bash

更多信息

完整文档及API参考请访问：https://moves-rwth.github.io/stormpy