Error : VECTORSZ가 너무 작습니다.

Question

Promela 및 특히 SPIN에서 일하는 것이 처음입니다. 나는 문제를 해결하기 위해 SPIN의 출력을 이해할 수없는 모델을 가지고 있습니다. 여기

내가 무슨 짓을 :

pan:1: VECTORSZ is too small, edit pan.h (at depth 0) 
pan: wrote untitled.pml.trail 

(Spin Version 6.4.5 -- 1 January 2016) 
Warning: Search not completed 
+ Partial Order Reduction 

Full statespace search for: 
    never claim   - (none specified) 
    assertion violations + 
    acceptance cycles - (not selected) 
    invalid end states + 

State-vector 8172 byte, depth reached 0, errors: 1 
    0 states, stored 
    0 states, matched 
    0 transitions (= stored+matched) 
    0 atomic steps 
hash conflicts:   0 (resolved) 

내가 다음 추적 파일을 검사하여 문제의 원인을 확인하려고 다시 SPIN 실행 다음과 같이

spin -a untitled.pml 
gcc -o pan pan.c 
./pan 

출력했다. (제가 이해), 검증은 "초기화"절차를 수행하는 동안 실패이 출력에 따르면

using statement merging 
spin: trail ends after -4 steps 
#processes: 1 
(global variable dump omitted) 
-4: proc 0 (:init::1) untitled.pml:173 (state 1) 
1 process created 

:

spin -t -v -p untitled.pml 

이

이 결과였다 :이 명령을 사용했다. untitled.pml 내에서 관련 코드는 이것이다 : 나는 나에게 있기 때문에 문제의 원인이 무엇 아무 생각이 시점에서

init { 
    int count = 0; 
    int ordinal = N; 

    do // This is line 173 
    :: (count < 2 * N + 1) -> 

은 "할"문은 잘 실행한다.

누구든지 SPIN 출력을 이해하는 데 도움을 줄 수 있습니까? 그렇다면 확인 과정에서이 오류를 제거 할 수 있습니까? 모델은 참조 용으로 올바른 출력을 생성합니다.

Answer 1

이 경우 trail 파일을 무시해도 상관 없습니다. 전혀 관련이 없습니다.

pan:1: VECTORSZ is too small, edit pan.h (at depth 0) 

지시어 VECTORSZ의 크기가 성공적 모델을 확인 너무 작 있음을 알려줍니다 오류 메시지입니다.

기본적으로 VECTORSZ의 크기는 1024입니다.

이 문제를 해결하려면 더 큰 VECTORSZ 크기로 검증을 컴파일하려고 : 너무 작동하지 않습니다

spin -a untitled.pml 
gcc -DVECTORSZ=2048 -o run pan.c 
./run 

2048 경우, 좀 더 (점점 크게) 값을보십시오.