自旋验证错误

Question

我在 Spin 中创建了一个模型。模拟结果如预期的那样运行。但是，当我尝试验证 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。然后在Extra Compile-Time Directives字段中添加-DVECTORSZ=4096然后重新运行验证

自旋验证错误

Spin verification error

verification

spin