在PROMELA

Question

對於下面的代碼未得錯誤，

proctype A() 
{ 
byte cond1; 

time = time + 1; 
time = time + 2; 
t[0] = 3; 
a[0] = 2; 
do 
:: (a[0] == 0)->break; 
:: else -> a[0] = a[0] - 1; 
    do 
    :: (t[0] <= t[1])->break; 
    od; 
    if 
     :: (cond1 != 0) -> 
      lock(mutex); 
      time = time + 1; 
      time = time + 2; 
      t[0] = t[0] + 3; 
      unlock(mutex); 
     :: (cond1 == 0) -> time = time + 1; 
    fi 
od; 
t[0] = 1000; 
} 

我碰到下面的錯誤，

unreached in proctype A 
code.pml:15, state 20, "time = (time+1)" 
code.pml:14, state 23, "((mutex==0))" 
code.pml:14, state 23, "else" 
code.pml:18, state 25, "time = (time+1)" 
code.pml:12, state 26, "((mutex==0))" 
code.pml:12, state 26, "((mutex==1))" 
code.pml:12, state 29, "((mutex==0))" 
code.pml:12, state 29, "((mutex==1))" 
code.pml:45, state 31, "time = (time+2)" 
code.pml:46, state 32, "t[0] = (t[0]+3)" 
(7 of 43 states) 

爲什麼會這樣呢？不應該爲每個cond1的值執行promela（cond1 == 0和cond1！= 0）。至少這是寫在here。

在驗證過程中，沒有進行這樣的調用，因爲實際上所有行爲選項都將在此模式下一次探測。

Answer 1

我使用select語句解決了這個問題，就像這樣。

select (cond1 : 0..1); 

Answer 2

的cond1初始值爲零，這是從來沒有改變 - 通過旋或代碼。因此條件cond1 != 0永遠不會是真的。要獲得該選項來執行你需要設置驗證生成其他/附加值利用cond1，例如：

proctype A() 
{ 
    byte cond1; 
    if 
    :: cond1 = 0; 
    :: cond1 = 1; 
    /* … */ 
    fi; 

    … 
}