logic - 如何使用 Spin 从命令行检查 Promela 代码

Question

我正在寻找如何在 Windows 10 命令行上使用Spin分析train.pml的输出。

任何帮助使文件提供正确的输出将不胜感激。

Answer 1

先决条件：在 Windows 10 上获得一个带有 gcc 的工作环境（例如，参见这些说明），或者，获得一个带有一些GNU/Linux发行版的虚拟环境。另外，在目标系统中正确安装Spin 。

---

只有两种可能的方法：

• 选项A .：

  ~$ spin -a train.pml
  ~$ gcc pan.c -o verifier
  ~$ ./verifier -a -N c1
  ...
  ~$ ./verifier -a -N c8
  ...
  

• 选项B .：

  ~$ spin -search -ltl c1 train.pml
  ...
  ~$ spin -search -ltl c8 train.pml
  ...
  

---

目前，属性已在您的模型上c1, c5, c7, c8进行验证c2, c3, c4, c6，而未验证。还有一些关于未达到的最终状态的抱怨。请检查后一种情况是否违反您的系统规范（它可能是也可能不是问题），并且验证的结果是否符合您的期望。

---

作为参考，这是您在验证属性时应获得的正确输出c1示例：

~$ spin -search -a -ltl c1 trail.pml
...
pan: ltl formula c1

(Spin Version 6.4.6 -- 2 December 2016)
    + Partial Order Reduction

Full statespace search for:
    never claim             + (c1)
    assertion violations    + (if within scope of claim)
    acceptance   cycles     + (fairness disabled)
    invalid end states  - (disabled by never claim)

State-vector 152 byte, depth reached 4508, errors: 0
    67919 states, stored (97586 visited)
   170919 states, matched
   268505 transitions (= visited+matched)
        0 atomic steps
hash conflicts:       184 (resolved)

Stats on memory usage (in Megabytes):
   11.659   equivalent memory usage for states (stored*(State-vector + overhead))
    5.455   actual memory usage for states (compression: 46.78%)
            state-vector as stored = 56 byte + 28 byte overhead
  128.000   memory used for hash table (-w24)
    0.534   memory used for DFS stack (-m10000)
  133.905   total actual memory usage


unreached in proctype train
    trail.pml:31, state 14, "-end-"
    (1 of 14 states)
unreached in proctype gate
    trail.pml:52, state 17, "-end-"
    (1 of 17 states)
unreached in proctype queue
    trail.pml:74, state 17, "-end-"
    (1 of 17 states)
unreached in claim c1
    _spin_nvr.tmp:10, state 13, "-end-"
    (1 of 13 states)

pan: elapsed time 0.12 seconds
pan: rate 813216.67 states/second