Что означает ошибка: восприятие неинициализированного чана в испине?

Question

ispin генерирует это сообщение в окне прогресса (средний нижний экран на вкладке симуляции): Ошибка: отправка неинициализированному каналу

Странно то, что сообщение об ошибке начинает появляться в серединесимуляции (я установил максимальное число шагов равным 10000, и оно начинает появляться вокруг 6000 шагов).

Как это может быть?неужели спин как-то теряет инициализацию чана в середине симуляции?

это инициализация одного из каналов, которые я использую:

chan VP = [1] of {byte};

и этосообщение об ошибке во время симуляции:

Answer 1

Это mcve для ошибки, с которой вы столкнулись:

chan c;

init {
    c!10;
}

, что дает

~$ spin test.pml 
Error: sending to an uninitialized chan
      timeout
Error: sending to an uninitialized chan
#processes: 1
  0:    proc  0 (:init::1) test.pml:4 (state 1)
1 process created

---

По сути, вы забыли указать, является ли канал синхронным или асинхронным , и какие сообщения он должен содержать. Правильное объявление канала должно выглядеть так:

chan c = [N] of { type_1, ..., type_M };

где N больше или равно 1 для любого асинхронного канала и 0 в противном случае, а type_1, ..., type_M - это список типов (то есть int, bool) поля, содержащиеся в одном сообщении.

Для получения более подробной информации, прочитайте документацию .