동등한 if 문보다 훨씬 느린 Promela에서 Select 문을 선택 하시겠습니까?

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

당신의 선택 문은 모든 루프 실행에, 두 가지 가능성, 중 전환 시스템 즉, 두 개의 서로 다른 후속 상태를 선택,

이 있다는 것을 의미

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

에 스핀에 의해 변환된다. break을 선택하지 않으면 비교와 할당 (두 상태)을 수행 한 다음 계속해야합니다. 값 31에 도달하려면 이전에 5 번의 비교와 5 번의 할당이 있었지만 if 버전에서는 할당에 대한 비 결정적 선택 만있었습니다.

spinspider를 사용하여 두 가지 버전을 시각화했습니다. 이로 인해 문제를 더 잘 이해할 수있게되었습니다.

다음 그림과 함께 프로그램에서 생성 된 상태 공간을 묘사 명확 단지 6 가능성이있다 -version이 중 하나를 선택하는 "경우"

int cycles; 

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

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

가 비교 이것을 select 문을 do 루프로 변환하여 얻은 프로그램에서 생성 된 이미지 :

차이점이 있습니까? 앞에서 말했듯이 주된 문제는 if 버전에서 과제를 선택하는 것과 달리 휴식을 선택하지 않는 각 주마다 do 버전에서 여러 가지 일을해야한다는 것입니다. 비교를해야합니다 , 카운터를 증가시킨 다음 계속하십시오. 이것은 명확하게 더 큰 상태 공간을 생성합니다.