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

Question

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

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

Answer 1

先决条件：得到用gcc一个工作环境上的Windows 10（例如看到these instructions）或，可选地，获得虚拟环境一些的GNU/Linux分布。目标系统中还有correctly install 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