SPIN/PROMELA에서 변수의 최대 값을 확인할 수 있습니까

Question

내 모델 검사 코드에서 특정 변수의 최대 값을 찾는 데 관심이 있습니다. 내가 지금 사용하는 절차는 어설 션 문 을 갖고, 바이너리 검색 방식으로 MAX_VALUE를 계속 변경하는 것입니다. 그러나 SPIN이 실제로 한 번의 실행으로 변수의 최대 값을 제공 할 수있는 방법이 있다면 훨씬 더 좋습니다. UPPAAL에는 sup 연산자가 있습니다. SPIN에 상응하는 프로그램이 있습니까?

Answer 1

이 does not appear to existPromela 연산자 (sup에 해당하는 유한 도메인이 관련되어 있음)가 max입니다.

한가지 가능한 방식은 상태 공간을 탐색하는 동안 외부 파일 var 값을 덤프 한 Promela 명세서 내에 embedded C code을 통해 예를 들어, 상태 정보를 기록 할 때마다 var 변경 값 :

c_code{ 
    FILE *fp; 
    int max_value; 
} 

함께 가진 inline :

최대 값을 찾기 위해

int var; 

inline set_var(value){ 
    var = value; 
    c_code{ 
     fp = fopen("max_value.txt", "r"); 
     fscanf(fp, "%d", & max_value); 
     fclose(fp); 
     if (now.var > max_value){ 
      fp = fopen("max_value.txt", "w"); 
      fprintf(fp, max_value); 
      fclose(fp); 
     } 

} 

, 전체 상태 공간은 종류에 의존하는, 열거한다 속성 확인 여부, 부분 주문 감소 적용 여부 등이 있습니다.

이 접근법은 파일에 대한보다 효율적인 액세스로 개선 될 수 있습니다.