Почему бесконечный цикл не приводит к ошибке при проверке модели с помощью Promela и Spin?

В этом примере

byte x = 0; byte y = 0;
active proctype toggle() {
    do
    :: x == 1 -> x = 0
    :: x == 0 -> x = 1
    od
}
init {
    (y == 1);
}

процесс init навсегда заблокирован (поскольку y == 1 всегда равен false), но процесс toggle всегда может выполнить что-то. Таким образом, нет недопустимой ошибки конечного состояния.

Вместо этого в этом примере

byte x = 0; byte y = 0;
active proctype toggle() {
    skip;
}
init {
    (y == 1);
}

процесс init по-прежнему заблокирован навсегда, но процесс toggle может выполнить свою единственную инструкцию skip; и затем завершиться. На данный момент ни один из оставшихся процессов (то есть только init) не имеет инструкций, которые он может выполнить, поэтому Spin завершается с ошибкой invalid end state.

~$ spin -a -search test.pml
pan:1: invalid end state (at depth 0)
pan: wrote test.pml.trail

(Spin Version 6.5.0 -- 17 July 2019)
...
State-vector 20 byte, depth reached 1, errors: 1
...

Есть ли способ заставить симулятор сообщать о бесконечном цикле как об ошибке?

Да. На самом деле есть несколько способов.

Самый простой подход — использовать опцию -l Spin:

~$ spin --help
...
-l: search for non-progress cycles
...

С этой опцией Spin сообщает о любом бесконечном цикле, не содержащем никакого состояния, с прогресс.

Это результат вашей исходной проблемы:

~$ spin -search -l test.pml
pan:1: non-progress cycle (at depth 2)
pan: wrote test.pml.trail

(Spin Version 6.5.0 -- 17 July 2019)
...
State-vector 28 byte, depth reached 9, errors: 1
...

~$ spin -t test.pml
spin: couldn't find claim 2 (ignored)
  <<<<<START OF CYCLE>>>>>
spin: trail ends after 10 steps
#processes: 2
        x = 0
        y = 0
 10:    proc  1 (:init::1) test.pml:10 (state 1)
 10:    proc  0 (toggle:1) test.pml:5 (state 4)
2 processes created

Альтернативный подход заключается в использовании проверки модели LTL. Например, вы можете указать, что в какой-то момент число процессов (см. _nr_pr), находящихся в процессе выполнения, становится равным 0 (или больше, если вы допускаете некоторые бесконечные циклы), или проверьте правильность завершения конкретного процесса, используя удаленные ссылки.

Оба случая содержатся в следующем примере:

byte x = 0; byte y = 0;
active proctype toggle() {
    do
    :: x == 1 -> x = 0
    :: x == 0 -> x = 1
    od;
end:
}
init {
    (y == 1);
}

// sooner or later, the process toggle
// with _pid == 0 will reach the end
// state
ltl p1 { <> toggle[0]@end };

// sooner or later, the number of processes
// that are currently running becomes 0,
// (hence, there can be no infinite loops)
ltl p2 { <> (_nr_pr == 0) };

Оба первые

~$ spin -a -search -ltl p1 test.pml
~$ spin -t test.pml
ltl p1: <> ((toggle[0]@end))
ltl p2: <> ((_nr_pr==0))
  <<<<<START OF CYCLE>>>>>
Never claim moves to line 4 [(!((toggle[0]._p==end)))]
spin: trail ends after 8 steps
#processes: 2
        x = 0
        y = 0
        end = 0
  8:    proc  1 (:init::1) test.pml:10 (state 1)
  8:    proc  0 (toggle:1) test.pml:3 (state 5)
  8:    proc  - (p1:1) _spin_nvr.tmp:3 (state 3)
2 processes created

и второй

~$ spin -a -search -ltl p2 test.pml
~$ spin -t test.pml
ltl p1: <> ((toggle[0]@end))
ltl p2: <> ((_nr_pr==0))
  <<<<<START OF CYCLE>>>>>
Never claim moves to line 11    [(!((_nr_pr==0)))]
spin: trail ends after 8 steps
#processes: 2
        x = 0
        y = 0
        end = 0
  8:    proc  1 (:init::1) test.pml:10 (state 1)
  8:    proc  0 (toggle:1) test.pml:3 (state 5)
  8:    proc  - (p2:1) _spin_nvr.tmp:10 (state 3)
2 processes created

Свойства LTL оказались ложными.

Что касается сообщений «unreached in proctype», добавление конечной метки в цикл do ничего не дает.

Метки end используются для удаления "недопустимого конечного состояния" ошибки, которая в противном случае была бы обнаружена.

Например, изменив предыдущий пример следующим образом:

byte x = 0; byte y = 0;
active proctype toggle() {
    skip;
}

init {
end:
    (y == 1);
}

Убирает ошибку:

~$ spin -a -search test.pml
(Spin Version 6.5.0 -- 17 July 2019)
...
State-vector 20 byte, depth reached 1, errors: 0
...

Метку end следует использовать только тогда, когда готовы гарантировать, что процесс, зависший без исполняемой инструкции, не является признаком нежелательной тупиковой ситуации.