关于SPIN模型检查器仿真模式的外部传参及输出存储问询

1. 是否为封闭系统？ #

SPIN基于Promela语言构建，默认的模型检查逻辑针对封闭系统（所有行为由模型内部定义，无外部环境主动输入）。但在仿真模式下，你可以通过外部参数、手动输入或脚本控制来模拟开放系统的交互场景——核心模型本身仍是封闭的，但仿真过程可引入外部干预。

2. 能否从Python/批处理向仿真模式传入参数？ #

完全可以，通过命令行参数结合Promela内置函数实现：

• 批处理调用：直接在spin命令后通过-arg传递参数，示例：

  spin -run -arg 50 20 model.pml
  

  在Promela模型中用getarg(n)获取第n个参数（n从1开始）：

  int max_steps = getarg(1);
  int threshold = getarg(2);
  

• Python调用：用subprocess模块执行spin命令并传递参数，示例：

  import subprocess
  # 传递参数50和20到仿真
  subprocess.run(["spin", "-run", "-arg", "50", "20", "model.pml"])
  

3. 仿真模式无需嵌入C代码写入输出到文件？ #

有两种简单方法，无需修改或嵌入C代码：

• 命令行重定向：直接将仿真的标准输出重定向到文件，批处理示例：

  spin -run model.pml > simulation_result.txt
  

  Python中可通过subprocess的stdout参数指定输出文件：

  with open("sim_result.txt", "w", encoding="utf-8") as out_file:
      subprocess.run(["spin", "-run", "model.pml"], stdout=out_file)
  

• Promela内置printf+重定向：在模型中用printf输出需要的内容到标准输出，再通过上述重定向方式写入文件，示例Promela代码：

  printf("Simulation step %d: current value = %d\n", step, value);
  

内容的提问来源于stack exchange，提问作者Andrea ER