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 
...