Jspin에서 mtype을 사용할 때 선언되지 않은 변수 오류

Question

나는 Jspin 및 Promela을 처음 사용합니다.

개인 ID 키 또는 암호를 사용하여 집 경보 시스템을 활성화 및 비활성화 할 수 있습니다. 활성화 후 시스템은 사용자가 대피 할 수있는 대기 시간 (약 30 초)으로 들어갑니다. 경보가 발령 된 보안 구역, 침입이 감지 된 경우에도 경보가 울리는 시간 또는 15 초의 지연이 내장되어있어 침입자가 암호를 입력하거나 카드 키를 스 와이프하여 자신을 식별 할 수 있도록합니다. 식별은 할당 된 15 초 이내에 이루어지지 않고 경보는 울리며 ID 카드 나 암호를 사용하여 비활성화 할 때까지 켜집니다. 내가 Jspin으로 코드를 실행하면

mtype = {sigact, sigdeact}; 
chan signal = [0] of {mtype}; 
/*chan syntax for declaring and initializing message passing channels*/ 



int count; 
bool alarm_off = true; /*The initial state of the alarm is off*/ 

active proctype alarm() 

{ 
off: 
    if 
    :: count >= 30 -> atomic {signal!sigdeact; count = 0;alarm_off = false; goto on;} 
    :: else -> atomic {count++; alarm_off = true; goto off;} 
    fi; 

on: 
    if 
    :: count >=15 -> atomic { signal!sigact; count = 0; 
    alarm_off = false; goto off;} 
    :: else -> atomic {signal!sigact; alarm_off = true; goto off;} 
    fi; 

pending: 

    if 
    :: count >= 30 -> atomic {count = 0; alarm_off = false; goto on;} 
    :: count < 30 -> atomic {count++; alarm_off = false; goto pending;} 
    fi; 
} 

나는이 메시지를 얻을 :

Error: undeclared variable: sigact 

을하지만 헤더에이 선언

이

는 코드입니다.

어떻게 해결할 수 있습니까?

Answer 1

documentationPromela에 따르면 mtype을 올바르게 사용하고 있습니다.

실제로 spin 버전 6.4.3을 사용하여 오류를 재현 할 수 없습니다. 따라서 Jspin이 올바르게 업데이트되지 않았다고 의심됩니다. ,

#define sigact 0 
#define sigdeact 1 
chan signal = [0] of {short}; // or bool for only 2 values 

... 

---

을 아무도 signal에서 읽어 없기 때문에 :

당신은 당신도 Jspin와 함께 작동합니다, 다음 주위에 작업을 시도 할 수 있습니다, 대신 Jspin의 spin를 사용하지 않으려면 나는 시스템 모델이 이고, 불완전한이고 나중에 더 많은 프로세스가 추가 될 것이라고 가정한다.

1. 하면 다음 명령 시퀀스, 즉 유의 : signal가 동기 채널 때문에

   가

   atomic { signal!sigdeact; count = 0; alarm_off = false; goto on; } 
   

   자성가 alarm 의해 temporarily lost 될 것이다 (그 크기 0 있음) 및 따라서 다른 프로세스 은 즉시 메시지를 읽기 위해으로 예약해야합니다 . 당신이 0 다시 count를 다시 count >= 30off 상태에서

2. 는 alarm_off = false을 설정 한 후 상태 on로 이동합니다. on 상태에서 즉시 alarm_off을 true으로 다시 설정하십시오. 이것은 의도 된 것입니까?실수로 보입니다. 아마 pending으로 가고 싶었을 것입니다.

3. 시스템의 설명을 읽으면 alarm에 어떤 종류의 input 신호가 누락 된 것 같습니다. signal 채널을 의도 된 목적과 다르게 사용하고있는 것으로 의심됩니다.

4. 모델은 경우에 off에 상태 pending 일부 전환, 적절한 개인 ID/비밀번호를 사용하지 말았어야?