2

我刚接触 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 输出，以便我可以在验证过程中消除此错误？该模型确实产生了正确的输出以供参考。

4

1 回答 1

2

在这种情况下，您可以简单地忽略该trail文件，它根本不相关。

错误信息

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

告诉您指令的大小VECTORSZ太小而无法成功验证您的模型。

默认情况下，VECTORSZ有 size 1024。

要解决此问题，请尝试使用更大的VECTORSZ大小编译您的验证器：

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

如果2048也不起作用，请尝试更多（越来越大）的值。

于 2017-11-23T13:23:47.757 回答