自旋驗證，驗證變量達到一定的數值​​

Question

這是我在Stack Exchange上的第一個問題，所以如果有任何違規指標，請告訴我。

我有一個用Promela編寫的大學OS和併發系統課程。有兩個進程正在運行，增加一個變量n。我們的任務是編寫這些流程，然後使用Spin中的驗證工具來證明n有可能獲得值4.我已經通讀了所有的命令行參數，但是沒有任何結果對我來說，「插入這個修飾符後跟一個變量名來檢查所有可能的值。」

byte n; 

proctype p() 
{ 
    byte countp = 0; 
    byte temp; 
    do 
    :: countp != 2 -> temp = n; temp = temp + 1; n = temp; countp = countp + 1; 
    :: countp >= 2 -> break; 
    od 
} 

proctype q() 
{ 

    byte countq = 0; 

    do 
    :: countq != 2 -> n = n + 1; countq = countq + 1; 
    :: countq >= 2 -> break; 
    od 
} 

init 
{ 
    run p(); 
    run q(); 
} 

Answer 1

有幾種方式做到這一點，但作爲一名教師，我寧願基於一個零擔，因爲至少它表明你瞭解如何使用它。

---

監視過程。

這是迄今爲止最簡單的概念：您只需添加一個過程，隨時聲明n != 4，然後檢查這個斷言是否最終會失敗。

byte n; 

active proctype p() 
{ 
    byte countp = 0; 
    byte temp; 
    do 
    :: countp != 2 -> temp = n; temp = temp + 1; n = temp; countp = countp + 1; 
    :: countp >= 2 -> break; 
    od 
} 

active proctype q() 
{ 

    byte countq = 0; 

    do 
    :: countq != 2 -> n = n + 1; countq = countq + 1; 
    :: countq >= 2 -> break; 
    od 
} 

active proctype monitor() 
{ 
    do 
     :: true -> assert(n != 4); 
    od; 
} 

注：在監控過程中的循環是完全不必要的，但它使得它的目的更加清晰初學者。

您可以用下面的襯板驗證此程序：

~$ spin -search -bfs buggy_01.pml 

自旋發現在零時間一個反例：

Depth=10 States=56 Transitions=84 Memory=128.195  
pan:1: assertion violated (n!=4) (at depth 19) 
pan: wrote buggy_01.pml.trail 

(Spin Version 6.4.3 -- 16 December 2014) 
Warning: Search not completed 
    + Breadth-First Search 
    + Partial Order Reduction 

Full statespace search for: 
    never claim    - (none specified) 
    assertion violations + 
    cycle checks   - (disabled by -DSAFETY) 
    invalid end states  + 

State-vector 28 byte, depth reached 19, errors: 1 
     215 states, stored 
      215 nominal states (stored-atomic) 
     181 states, matched 
     396 transitions (= stored+matched) 
     0 atomic steps 
hash conflicts:   0 (resolved) 

Stats on memory usage (in Megabytes): 
    0.011  equivalent memory usage for states (stored*(State-vector + overhead)) 
    0.290  actual memory usage for states 
    128.000  memory used for hash table (-w24) 
    128.195  total actual memory usage 

pan: elapsed time 0 seconds 

實際上，你可以檢查執行跟蹤這違反了以下斷言：

~$ spin -t -p -g -l buggy_01.pml 

個

的選項具有以下含義：

• -t：重播通過旋
• -p產生的.trail反例：打印所有報表
• -g：打印所有的全局變量
• -l：打印所有局部變量

這是輸出：

using statement merging 
    1: proc 2 (monitor:1) buggy_01.pml:27 (state 1) [(1)] 
    2: proc 1 (q:1) buggy_01.pml:19 (state 1) [((countq!=2))] 
    3: proc 0 (p:1) buggy_01.pml:8 (state 1) [((countp!=2))] 
    4: proc 1 (q:1) buggy_01.pml:19 (state 2) [n = (n+1)] 
     n = 1 
    5: proc 1 (q:1) buggy_01.pml:19 (state 3) [countq = (countq+1)] 
     q(1):countq = 1 
    6: proc 1 (q:1) buggy_01.pml:19 (state 1) [((countq!=2))] 
    7: proc 1 (q:1) buggy_01.pml:19 (state 2) [n = (n+1)] 
     n = 2 
    8: proc 1 (q:1) buggy_01.pml:19 (state 3) [countq = (countq+1)] 
     q(1):countq = 2 
    9: proc 1 (q:1) buggy_01.pml:20 (state 4) [((countq>=2))] 
10: proc 0 (p:1) buggy_01.pml:8 (state 2) [temp = n] 
     p(0):temp = 2 
11: proc 0 (p:1) buggy_01.pml:8 (state 3) [temp = (temp+1)] 
     p(0):temp = 3 
12: proc 0 (p:1) buggy_01.pml:8 (state 4) [n = temp] 
     n = 3 
13: proc 0 (p:1) buggy_01.pml:8 (state 5) [countp = (countp+1)] 
     p(0):countp = 1 
14: proc 0 (p:1) buggy_01.pml:8 (state 1) [((countp!=2))] 
15: proc 0 (p:1) buggy_01.pml:8 (state 2) [temp = n] 
     p(0):temp = 3 
16: proc 0 (p:1) buggy_01.pml:8 (state 3) [temp = (temp+1)] 
     p(0):temp = 4 
17: proc 0 (p:1) buggy_01.pml:8 (state 4) [n = temp] 
     n = 4 
18: proc 0 (p:1) buggy_01.pml:8 (state 5) [countp = (countp+1)] 
     p(0):countp = 2 
19: proc 0 (p:1) buggy_01.pml:9 (state 6) [((countp>=2))] 
spin: buggy_01.pml:27, Error: assertion violated 
spin: text of failed assertion: assert((n!=4)) 
20: proc 2 (monitor:1) buggy_01.pml:27 (state 2) [assert((n!=4))] 
spin: trail ends after 20 steps 
#processes: 3 
     n = 4 
20: proc 2 (monitor:1) buggy_01.pml:26 (state 3) 
20: proc 1 (q:1) buggy_01.pml:22 (state 9) <valid end state> 
20: proc 0 (p:1) buggy_01.pml:11 (state 11) <valid end state> 
3 processes created 

如您所見，它報告（一）導致斷言違規的可能執行痕跡。

---

LTL。

人能想到幾個LTL性質，可以幫助驗證n是否最終會等於4。一種這樣的性質，是[] (n != 4)，其內容爲：

從初始狀態開始，在每個可到達狀態沿着所有外出路徑它始終是true即n是從4不同。

新的模式是這樣的：

byte n; 

active proctype p() 
{ 
    byte countp = 0; 
    byte temp; 
    do 
    :: countp != 2 -> temp = n; temp = temp + 1; n = temp; countp = countp + 1; 
    :: countp >= 2 -> break; 
    od 
} 

active proctype q() 
{ 

    byte countq = 0; 

    do 
    :: countq != 2 -> n = n + 1; countq = countq + 1; 
    :: countq >= 2 -> break; 
    od 
} 

ltl p0 { [] (n != 4) } 

你，你會這樣的斷言幾乎以同樣的方式驗證該屬性。爲了保持這個答案總之，我不會複製和粘貼在這裏，整個輸出，只是列出所用的命令：

~$ spin -search -bfs buggy_02.pml 
ltl p0: [] ((n!=4)) 
Depth=10 States=40 Transitions=40 Memory=128.195  
pan:1: assertion violated !(!((n!=4))) (at depth 15) 
pan: wrote buggy_02.pml.trail 

... 

Full statespace search for: 
    never claim    + (p0) 
    ... 
State-vector 28 byte, depth reached 15, errors: 1 
... 

~$ spin -t -p -g -l buggy_02.pml 
... 

---

如果你想保證n總是最終等於4 ，那麼您應該查看一些互斥方法來保護您的關鍵部分或者替代地檢查documentation的d_step {}。