Error: VECTORSZ is too small

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 以尝试通过检查跟踪文件来确定问题的原因。我使用了这个命令：

spin -t -v -p untitled.pml

这是结果：

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

根据此输出（据我了解），在 "init" 过程中验证失败。 untitled.pml 中的相关代码是这样的：

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

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

此时我不知道是什么导致了问题，因为对我来说，"do" 语句应该可以正常执行。

任何人都可以帮助我理解 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 也不起作用，请尝试更多 （越来越大） 值。

Error: VECTORSZ is too small

Error: VECTORSZ is too small

concurrency

model-checking

formal-verification

spin

promela