在Promela中選擇語句要比等價的if語句慢得多？

Question

所以我在我的Promela代碼中使用了以下行。

select(cycles: 26..31); 

然而，這是造成狀態爆炸。我用下面的if聲明替換它，突然間州爆炸問題消失了。我上面顯示的select聲明是否應該等於下面的if聲明？這裏發生了什麼？

if 
:: cycles = 26; 
:: cycles = 27; 
:: cycles = 28; 
:: cycles = 29; 
:: cycles = 30; 
:: cycles = 31; 
fi; 

Answer 1

你的SELECT語句，通過旋轉轉換成

cycles = 26; 
do 
    :: cycles < 31 -> cycles++ 
    :: break 
od 

這意味着還有，在每一個循環執行，兩種可能性中進行選擇，在過渡系統，即兩個不同的繼承國。如果未選擇break，則必須進行比較和分配（兩種狀態），然後繼續。如果你想達到31的值，你之前有5次比較和5次賦值，而在if版本中，賦值只是一個非確定性的選擇。

我用spinspider可視化了兩個不同的版本，這會讓問題變得更好理解。

下圖描述了從程序生成的狀態空間用「如果」 -version，那裏顯然只有6個可能性中進行選擇：

int cycles; 

active proctype testWithIf() { 
    if 
    :: cycles = 26; 
    :: cycles = 27; 
    :: cycles = 28; 
    :: cycles = 29; 
    :: cycles = 30; 
    :: cycles = 31; 
    fi; 

    assert(cycles >= 26 && cycles <= 31); 
} 

比較這對

int cycles; 
active proctype test1() { 
    cycles = 26; 
    do 
    :: cycles < 31 -> cycles++ 
    :: break 
    od; 

    assert(cycles >= 26 && cycles <= 31); 
} 

：從圖像獲得你的SELECT語句的轉變成一個做循環的程序產生

您是否看到不同？正如我所說的，我認爲主要的問題在於，在if版本中，您只需選擇一項任務，但在每個不選擇中斷的狀態下，您必須在do-version中執行多項任務：您必須進行比較，增加計數器，然後繼續。這顯然會產生更大的狀態空間。