Ошибка: индексация массива «каналы»

Я получаю эту ошибку с 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 всегда инициализируются правильным значением канала, когда я пытаюсь получить к ним доступ.

Вопрос. Почему я получаю сообщение об ошибке и как это исправить?


promela spin model-checking
person Patrick Trentin    schedule 18.04.2018    source источник

Ответы (1)


arrow_upward
1
arrow_downward

ПРИМЕЧАНИЕ: код, предложенный в вопросе, больше не будет вызывать ошибок, начиная с Spin версии 6.4.9, благодаря обновлениям.

Вот решение:

Переменные, которые появляются где-либо в теле proctype, создаются при создании процесса. [...] Чтобы избежать подобных вещей, лучше отделить объявление от инициализации.

[Г. Х., личное сообщение]

По некоторым причинам, если переменная объявлена ​​и инициализирована в одном и том же операторе, когда Spin 6.4.8 создает их экземпляры при создании процесса, он также пытается выполнить инициализацию того же типа, что и в Модели Promela.

В данном примере node с _pid, равным 0, имеет 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];
    }
}
person Patrick Trentin    schedule 18.04.2018