如何使用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