다음 코드를

Question

하는 Promela의 미전도 종족 오류가 나는 다음과 같은 오류가

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) 

왜 그런가요? Promela는 cond1의 모든 값 (cond1 == 0 및 cond1! = 0)을 모두 실행해서는 안됩니다. 적어도 이것은 here에 쓰여진 것입니다.

확인 중에는 모든 동작 옵션이 효과적으로이 모드에서 한 번에 하나씩 탐색되므로 효과적으로 호출하지 않습니다.

Answer 1

이와 같이 select 문을 사용하여 해결했습니다.

select (cond1 : 0..1); 

Answer 2

cond1의 초기 값은 0이 아니며 스핀이나 코드에 의해 변경되지 않습니다. 따라서 조건 cond1 != 0은 사실이 아닙니다. 해당 옵션을 실행하려면 다음을 사용하여 cond1에 대한 기타/추가 값을 생성하도록 확인을 설정해야합니다.

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

    … 
}