SPIN模型檢查器中的多線程

Question

我們如何使用線程數參數化SPIN模型？ 我正在使用標準的SPIN模型檢查器。它有選項來設置並行線程的數量嗎？我檢查了參考，但沒有發現任何有用的東西

Answer 1

您可以使用run運算符動態產生Promela進程。因此，您可以循環爲：

#define TRY_COUNT 5 
byte index = 0; 
do 
:: index == TRY_COUNT -> break 
:: else -> index++; run theProcess() 
od 

你也可以這樣定義一個文件：

active [TRY_COUNT] proctype foo() { 
    printf ("PID: %d\n", _pid); 
    assert (true) 
} 

init { 
    assert (true) 
} 

，然後運行SPIN模擬：

$ spin -DTRY_COUNT=4 bar.pml 
       PID: 2 
     PID: 0 
      PID: 1 
        PID: 3 
5 processes created 

或驗證

$ spin -DTRY_COUNT=4 -a bar.pml 
$ gcc -o bar pan.c 
$ ./bar 
hint: this search is more efficient if pan.c is compiled -DSAFETY 

(Spin Version 6.3.2 -- 17 May 2014) 
    + Partial Order Reduction 
...