SPIN 模型检查器中的多线程

Question

我们如何用线程数参数化 SPIN 模型？我正在使用标准的 SPIN 模型检查器。它是否有设置并行线程数的选项？我检查了参考资料，但没有找到任何有用的东西

Answer 1

您可以使用 run 运算符动态生成 Promela 进程。 因此，您可以迭代为：

#define TRY_COUNT 5
byte index = 0;
do
:: index == TRY_COUNT -> break
:: else -> index++; run theProcess()
od

您还可以定义如下文件：

active [TRY_COUNT] proctype foo () {
  printf ("PID: %dn", _pid);
  assert (true)
}
init {
  assert (true)
}

然后运行 SPIN 模拟：

$ spin -DTRY_COUNT=4 bar.pml
              PID: 2
      PID: 0
          PID: 1
                  PID: 3
5 processes created

或验证

$ spin -DTRY_COUNT=4 -a bar.pml
$ gcc -o bar pan.c
$ ./bar
hint: this search is more efficient if pan.c is compiled -DSAFETY
(Spin Version 6.3.2 -- 17 May 2014)
    + Partial Order Reduction
...