旋轉驗證錯誤

Question

我在旋轉中創建了一個模型。仿真按預期運行。然而，當我嘗試驗證的LTL性質，我得到如下結果：

C:/cygwin64/bin/gcc.exe -DMEMLIM=1024 -O2 -DXUSAFE -w -o pan pan.c 
./pan -m10000 -a 
Pid: 9372 
pan:1: VECTORSZ is too small, edit pan.h (at depth 0) 
pan: wrote cs.pml.trail 

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

Full statespace search for: 
    never claim    + (p1) 
    assertion violations + (if within scope of claim) 
    acceptance cycles  + (fairness disabled) 
    invalid end states - (disabled by never claim) 

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

Stats on memory usage (in Megabytes): 
    0.000 equivalent memory usage for states (stored*(State-vector + overhead)) 
    0.000 actual memory usage for states (less than 1k) 
    128.000 memory used for hash table (-w24) 
    0.534 memory used for DFS stack (-m10000) 
    0.632 total actual memory usage 



pan: elapsed time 4.11e+03 seconds 
To replay the error-trail, goto Simulate/Replay and select "Run" 

使用跟蹤文件運行仿真並沒有提供多少信息，因爲模擬立即結束（我只得到警告，有關未使用的變量）。我懷疑VECTORSZ is too small是造成這個問題。如何使用iSpin更改此值？

Answer 1

好的，我能解決這個問題。

使用iSpin，轉到Verification選項卡，然後單擊Show Advanced Parameter Settings。然後將-DVECTORSZ=4096添加到Extra Compile-Time Directives字段，然後重新運行驗證。