Возможно ли получить множественные (или все) нарушения для свойства с помощью Spin?Запрашивать множественные (или все) нарушения в Spin
В качестве примера, я создал модель Promela ниже:
byte mutex = 0;
active proctype A() {
A1: mutex==0; /* Is free? */
A2: mutex++; /* Get mutex */
A3: /* A's critical section */
A4: mutex--; /* Release mutex */
}
active proctype B() {
B1: mutex==0; /* Is free? */
B2: mutex++; /* Get mutex */
B3: /* B's critical section */
B4: mutex--; /* Release mutex */
}
ltl {[] (mutex < 2)}
Он имеет наивную реализацию мьютекса. Можно было ожидать, что процессы A и B не достигнут критического раздела вместе, и я написал выражение LTL, чтобы проверить это.
Запуск
spin -run mutex_example.pml
показывает, что свойство не действует и работает
spin -p -t mutex_example.pml
показывают последовательность операторов, которые нарушают свойство.
Never claim moves to line 4 [(1)]
2: proc 1 (B:1) mutex_example.pml:11 (state 1) [((mutex==0))]
4: proc 0 (A:1) mutex_example.pml:4 (state 1) [((mutex==0))]
6: proc 1 (B:1) mutex_example.pml:12 (state 2) [mutex = (mutex+1)]
8: proc 0 (A:1) mutex_example.pml:5 (state 2) [mutex = (mutex+1)]
spin: _spin_nvr.tmp:3, Error: assertion violated
spin: text of failed assertion: assert(!(!((mutex<2))))
Never claim moves to line 3 [assert(!(!((mutex<2))))]
spin: trail ends after 9 steps
#processes: 2
mutex = 2
9: proc 1 (B:1) mutex_example.pml:14 (state 3)
9: proc 0 (A:1) mutex_example.pml:7 (state 3)
9: proc - (ltl_0:1) _spin_nvr.tmp:2 (state 6)
Это показывает, что последовательность операторов (обозначены метками) «B1» -> «A1» -> «B2» -> «A2» нарушают свойства, но есть и другие варианты перемежения, ведущие к тому, что (например 'A1' -> 'B1' -> 'B2' -> 'A2').
Могу ли я попросить Spin дать мне несколько (или все) следов?
В моем примере, оба процесса (A и B) конечны, поэтому число встречных примеров должно быть конечным. –
Дело в том, чтобы систематически находить встречные примеры. У меня нет гарантии, что использование разных параметров поиска я не найду в одном и том же примере счетчика много раз ... :( –
@BraulioHorta, вы правы, я соответственно обновлю ответ. –