エラー：VECTORSZが小さすぎます

Question

私はPromela、特にSPINを使用するのが初めてです。私は検証しようとしているモデルを持っており、問題を解決するためにSPINの出力を理解できません。ここで

は私がやったことで次のように

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

出力されました：

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を走りました。 （私はそれを理解したように）この出力によると

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サイズを使用して検証をコンパイルしてみてください、この問題を修正するには：2048はあまりにも動作しない場合

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

、値（徐々に大きくなる）いくつかのより多くを試してみてください。