Spin Verification, проверка переменной достигает определенного значения
Это мой первый вопрос на Stack Exchange, так что если есть что-то, что нарушает правила, пожалуйста, дайте мне знать.
У меня есть программа, написанная на Promela для ОС колледжа и класса параллельных систем. Есть два запущенных процесса, которые увеличивают переменную n. Наша задача - написать процессы и затем использовать инструмент проверки в Spin, чтобы доказать, что n может принять значение 4. Я прочитал все аргументы командной строки и запутался, но ничего не вычеркнуло. для меня как "вставить этот модификатор, а затем имя переменной, чтобы проверить все возможные значения".
byte n;
proctype p()
{
byte countp = 0;
byte temp;
do
:: countp != 2 -> temp = n; temp = temp + 1; n = temp; countp = countp + 1;
:: countp >= 2 -> break;
od
}
proctype q()
{
byte countq = 0;
do
:: countq != 2 -> n = n + 1; countq = countq + 1;
:: countq >= 2 -> break;
od
}
init
{
run p();
run q();
}
1 ответ
Есть несколько способов сделать это, хотя как учитель я бы предпочел основанный на ltl, поскольку, по крайней мере, он показывает, что вы понимаете, как его использовать.
Мониторинг процесса.
Это, безусловно, самое простое, концептуально: вы просто добавляете процесс, который утверждает, что n != 4 в любое время, а затем проверьте, не проходит ли это утверждение в конце концов или нет.
byte n;
active proctype p()
{
byte countp = 0;
byte temp;
do
:: countp != 2 -> temp = n; temp = temp + 1; n = temp; countp = countp + 1;
:: countp >= 2 -> break;
od
}
active proctype q()
{
byte countq = 0;
do
:: countq != 2 -> n = n + 1; countq = countq + 1;
:: countq >= 2 -> break;
od
}
active proctype monitor()
{
do
:: true -> assert(n != 4);
od;
}
Примечание: цикл в процессе мониторинга совершенно не нужен, но он делает его назначение более понятным для начинающих.
Вы можете проверить эту программу со следующим одним вкладышем:
~$ spin -search -bfs buggy_01.pml
Spin находит контрпример в нулевое время:
Depth=10 States=56 Transitions=84 Memory=128.195
pan:1: assertion violated (n!=4) (at depth 19)
pan: wrote buggy_01.pml.trail
(Spin Version 6.4.3 -- 16 December 2014)
Warning: Search not completed
+ Breadth-First Search
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 28 byte, depth reached 19, errors: 1
215 states, stored
215 nominal states (stored-atomic)
181 states, matched
396 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.011 equivalent memory usage for states (stored*(State-vector + overhead))
0.290 actual memory usage for states
128.000 memory used for hash table (-w24)
128.195 total actual memory usage
pan: elapsed time 0 seconds
Вы можете проверить трассировку выполнения, которая нарушает утверждение, с помощью:
~$ spin -t -p -g -l buggy_01.pml
Опции имеют следующее значение:
-t: повтори.trailконтрпример, сгенерированный вращением-p: распечатать все выписки-g: вывести все глобальные переменные-l: вывести все локальные переменные
Это вывод:
using statement merging
1: proc 2 (monitor:1) buggy_01.pml:27 (state 1) [(1)]
2: proc 1 (q:1) buggy_01.pml:19 (state 1) [((countq!=2))]
3: proc 0 (p:1) buggy_01.pml:8 (state 1) [((countp!=2))]
4: proc 1 (q:1) buggy_01.pml:19 (state 2) [n = (n+1)]
n = 1
5: proc 1 (q:1) buggy_01.pml:19 (state 3) [countq = (countq+1)]
q(1):countq = 1
6: proc 1 (q:1) buggy_01.pml:19 (state 1) [((countq!=2))]
7: proc 1 (q:1) buggy_01.pml:19 (state 2) [n = (n+1)]
n = 2
8: proc 1 (q:1) buggy_01.pml:19 (state 3) [countq = (countq+1)]
q(1):countq = 2
9: proc 1 (q:1) buggy_01.pml:20 (state 4) [((countq>=2))]
10: proc 0 (p:1) buggy_01.pml:8 (state 2) [temp = n]
p(0):temp = 2
11: proc 0 (p:1) buggy_01.pml:8 (state 3) [temp = (temp+1)]
p(0):temp = 3
12: proc 0 (p:1) buggy_01.pml:8 (state 4) [n = temp]
n = 3
13: proc 0 (p:1) buggy_01.pml:8 (state 5) [countp = (countp+1)]
p(0):countp = 1
14: proc 0 (p:1) buggy_01.pml:8 (state 1) [((countp!=2))]
15: proc 0 (p:1) buggy_01.pml:8 (state 2) [temp = n]
p(0):temp = 3
16: proc 0 (p:1) buggy_01.pml:8 (state 3) [temp = (temp+1)]
p(0):temp = 4
17: proc 0 (p:1) buggy_01.pml:8 (state 4) [n = temp]
n = 4
18: proc 0 (p:1) buggy_01.pml:8 (state 5) [countp = (countp+1)]
p(0):countp = 2
19: proc 0 (p:1) buggy_01.pml:9 (state 6) [((countp>=2))]
spin: buggy_01.pml:27, Error: assertion violated
spin: text of failed assertion: assert((n!=4))
20: proc 2 (monitor:1) buggy_01.pml:27 (state 2) [assert((n!=4))]
spin: trail ends after 20 steps
#processes: 3
n = 4
20: proc 2 (monitor:1) buggy_01.pml:26 (state 3)
20: proc 1 (q:1) buggy_01.pml:22 (state 9) <valid end state>
20: proc 0 (p:1) buggy_01.pml:11 (state 11) <valid end state>
3 processes created
как вы видите, он сообщает (один) из возможных следов выполнения, которые приводят к нарушению утверждения.
LTL.
Можно вспомнить несколько свойств ltl, которые могут помочь проверить, n в конечном итоге будет равен 4, Одним из таких свойств является [] (n != 4), который гласит:
начиная с исходного состояния, в каждом достижимом состоянии по всем исходящим путям всегда
trueтотnотличается от4,
Новая модель выглядит так:
byte n;
active proctype p()
{
byte countp = 0;
byte temp;
do
:: countp != 2 -> temp = n; temp = temp + 1; n = temp; countp = countp + 1;
:: countp >= 2 -> break;
od
}
active proctype q()
{
byte countq = 0;
do
:: countq != 2 -> n = n + 1; countq = countq + 1;
:: countq >= 2 -> break;
od
}
ltl p0 { [] (n != 4) }
Вы проверяете это свойство практически так же, как и в утверждении. Чтобы этот ответ был коротким, я не буду копировать и вставлять весь вывод здесь, а просто перечислю используемые команды:
~$ spin -search -bfs buggy_02.pml
ltl p0: [] ((n!=4))
Depth=10 States=40 Transitions=40 Memory=128.195
pan:1: assertion violated !( !((n!=4))) (at depth 15)
pan: wrote buggy_02.pml.trail
...
Full statespace search for:
never claim + (p0)
...
State-vector 28 byte, depth reached 15, errors: 1
...
~$ spin -t -p -g -l buggy_02.pml
...
Если вы хотите гарантировать, что n всегда в конечном итоге равен 4затем вы должны рассмотреть какой-нибудь подход взаимного исключения для защиты критического раздела или, в качестве альтернативы, проверить документацию d_step {},