Error: indexing array 'channels'

Question

我在 Spin 6.4.8 中遇到此错误：

spin: indexing channels[-1] - size is 3
spin: 2.pml:13, Error: indexing array 'channels'

当运行模拟以下Promela模型时：

chan channels[3] = [1] of { pid };

active [3] proctype node () {
    short pred = (_pid - 1) % 3;
    short succ = (_pid + 1) % 3;
    printf("Values(%d): %d, %d\n", _pid, pred, succ);
    if
        :: pred == -1 -> pred = 2;
        :: else -> skip;
    fi;
    printf("Corrected Values(%d): %d, %d\n", _pid, pred, succ);
    {
        chan pc = channels[pred];
        chan sc = channels[succ];
    }
}

如以下输出跟踪所示，我没有访问错误消息所声明的有问题的 -1 数组位置：

  Values(0): -1, 1
          Values(2): 1, 0
      Values(1): 0, 2
      Corrected Values(1): 0, 2
          Corrected Values(2): 1, 0
  Corrected Values(0): 2, 1

经过进一步分析（此处未显示），看起来 pc 和 sc 在我尝试访问它们时也总是初始化为正确的通道值。

问：为什么我会收到错误消息，我该如何解决？

Answer 1

注意：由于更新，问题中提出的代码从 Spin 版本 6.4.9 开始将不再产生任何错误。

解决方法如下：

Variables that apper anywhere in a proctype body are instantiated when the process is created. [...] To avoid this kind of thing it's better to separate declaration from initialization.

[G. H., private communication]

出于某些原因，如果一个变量在同一语句中声明和初始化，当 Spin 6.4.8 在进程创建时实例化它们时，它也会尝试执行 [=39= 中指定的相同类型的初始化]Promela 型号.

在给定的示例中，_pid 等于 0 的 node 在创建时具有 pred 等于 -1，因此 Spin 尝试同时执行 chan pc = channels[pred]; 会导致错误，因为存在越界访问。

如上所述，可以通过将声明与初始化分开来解决此问题：

chan channels[3] = [1] of { pid };

active [3] proctype node () {
    short pred = (_pid - 1) % 3;
    short succ = (_pid + 1) % 3;
    printf("Values(%d): %d, %d\n", _pid, pred, succ);
    if
        :: pred == -1 -> pred = 2;
        :: else -> skip;
    fi;
    printf("Corrected Values(%d): %d, %d\n", _pid, pred, succ);
    {
        chan pc;
        chan sc;
        pc = channels[pred];
        sc = channels[succ];
    }
}

具有以下输出：

~$ spin test.pml 
              Values(2): 1, 0
      Values(0): -1, 1
          Values(1): 0, 2
          Corrected Values(1): 0, 2
              Corrected Values(2): 1, 0
      Corrected Values(0): 2, 1
3 processes created

或者，可以绕过该问题并防止 pred 永远具有无效值：

chan channels[3] = [1] of { pid };

active [3] proctype node () {
    short pred = (_pid - 1 + 3) % 3;
    short succ = (_pid + 1) % 3;
    printf("Values(%d): %d, %d\n", _pid, pred, succ);
    {
        chan pc = channels[pred];
        chan sc = channels[succ];
    }
}

Error: indexing array 'channels'

Error: indexing array 'channels'

model-checking

spin

promela