В этом примере
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 завершается с недопустимым конечным состоянием ошибка.
~$ 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 сообщает о любом бесконечном цикле , который не содержит никакого состояния. с меткой progress .
Это вывод исходной проблемы:
~$ 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 оказываются ложными. 'сообщения, добавление конечной метки в цикл 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
...
Всегда следует использовать конец метка, когда кто-то готов гарантировать , что процесс, застрявший без исполняемой инструкции, не является признаком нежелательной ситуации взаимоблокировки.