Лабораторная работа: Решённая практика (5 заданий)
Описание
Характеристики лабораторной работы
Список файлов
- Прочти меня!!!.txt 136 b
- Решённая практика (5 заданий)
- Task1
- task.txt 735 b
- task_достиж.txt 3,62 Kb
- task_потенц.txt 935 b
- Сдавать
- 422_Snegirev.cpp 5,15 Kb
- solution.txt 4,51 Kb
- task.txt 4,91 Kb
- Task2
- 422_Snegirev_2.cpp 7,96 Kb
- 422_Snegirev_2.pml 783 b
- abstract_lts_m12.dot 850 b
- abstract_lts_m12.png 44,96 Kb
- log.txt 1,02 Kb
- lts_m1.png 37,11 Kb
- lts_m1.txt 548 b
- lts_m12.dot 12,92 Kb
- lts_m12.png 564,44 Kb
- lts_m2.png 30,95 Kb
- lts_m2.txt 445 b
- states.txt 287 b
- task.txt 870 b
- Task3
- 422_Snegirev_3.pml 2,29 Kb
- Program_ruduce.txt 1,32 Kb
- Solution.txt 2,39 Kb
- log.txt 24,04 Kb
- msc.log 77 b
- msc.pdf 15,38 Kb
- msc.ps 30,24 Kb
- sim.out 27,78 Kb
- Task4
- Model Checking Task 4.eml 4,44 Kb
- Model Checking Task 4.eml_OECustomProperty 825 b
- Solution.txt 1,45 Kb
- Solution_2.txt 1,12 Kb
- task4task131.txt 692 b
- Task5
- counterexample_1.txt 1,36 Kb
- counterexample_2.txt 4,59 Kb
- model_assert.pml 1,96 Kb
- prog_counterexample_1.txt 152 b
- prog_counterexample_2.txt 423 b
- spec_1.ltl 293 b
- spec_2.ltl 751 b
- spec_3.ltl 1,13 Kb
Файл скачан с сайта StudIzba.com
При копировании или цитировании материалов на других сайтах обязательно используйте ссылку на источник
int h;
void
f (int a, int b)
{
int x, y;
x = 4;
y = 4;
h = 2;
if (x > 0)
{
h = 3;
if (y < 8)
{
if (h > 6)
{
h = 2;
}
x = 9;
y = 9;
}
}
}
void
g (int a, int b)
{
int x, y;
x = 5;
y = 8;
h = 3;
if (x > 2)
{
if (h > a)
{
h = 1;
}
else
{
h = 2;
}
}
else
{
if (x > 3)
{
y = 3;
y = 2;
}
}
while (x > 9)
{
if (h > 0)
break;
if (h > 7)
{
h = 4;
}
y = 1;
h = 4;
}
}
int h;
void f (int a, int b) h f_a f_b f_x f_y g_x g_y g_a g_b
{
0: int x, y; {#,2,3,1} 2^32 2^32 # # {5,#} {8,#} 2^32 2^32
1: x = 4; {#,2,3,1} 2^32 2^32 # # {5,#} {8,#} 2^32 2^32
2: y = 4; {#,2,3,1} 2^32 2^32 4 # {5,#} {8,#} 2^32 2^32
3: h = 2; {#,2,3,1} 2^32 2^32 4 4 {5,#} {8,#} 2^32 2^32
4: if (x > 0) {2,3,1} 2^32 2^32 4 4 {5,#} {8,#} 2^32 2^32
{
5: h = 3; {2,3,1} 2^32 2^32 4 4 {5,#} {8,#} 2^32 2^32
6: if (y < 8) {2,3,1} 2^32 2^32 4 4 {5,#} {8,#} 2^32 2^32
{
7: if (h > 6) ________________________________________ ____________________________
{
8: h = 2; ________________________________________ ____________________________
}
9: x = 9; ________________________________________ ____________________________
10: y = 9; ________________________________________ ____________________________
}
}
11:} {2,3,1} 2^32 2^32 4 4 {5,#} {8,#} 2^32 2^32
void g (int a, int b) h f_a f_b f_x f_y g_x g_y g_a g_b
{
0: int x, y; {#,2,3} 2^32 2^32 {#,4} {#,4} # # 2^32 2^32
1: x = 5; {#,2,3} 2^32 2^32 {#,4} {#,4} # # 2^32 2^32
2: y = 8; {#,2,3} 2^32 2^32 {#,4} {#,4} 5 # 2^32 2^32
3: h = 3; {#,2,3} 2^32 2^32 {#,4} {#,4} 5 8 2^32 2^32
4: if (x > 2) {2,3} 2^32 2^32 {#,4} {#,4} 5 8 2^32 2^32
{
5: if (h > a) {2,3} 2^32 2^32 {#,4} {#,4} 5 8 2^32 2^32
{
6: h = 1; {2,3} 2^32 2^32 {#,4} {#,4} 5 8 2^32 2^32
}
else
{
7: h = 2; {2,3} 2^32 2^32 {#,4} {#,4} 5 8 2^32 2^32
}
}
else
{
8: if (x > 3) ________________________________________ __________________________
{
9: y = 3; ________________________________________ __________________________
10: y = 2; ________________________________________ __________________________
}
}
11: while (x > 9) {2,3,1} 2^32 2^32 {#,4} {#,4} 5 8 2^32 2^32
{
12: if (h > 0) ________________________________________ __________________________
13: break; ________________________________________ __________________________
14: if (h > 7) ________________________________________ __________________________
{
15: h = 4; ________________________________________ __________________________
}
16: y = 1; ________________________________________ __________________________
17: h = 4; ________________________________________ __________________________
}
18: } {2,3,1} 2^32 2^32 {#,4} {#,4} 5 8 2^32 2^32
12*18*2^(32*9)
int h;
void
f (int a, int b)
{
0: int x, y;
1: x = 4;
2: y = 4;
3: h = 2;
4: if (x > 0)
{
5: h = 3;
6: if (y < 8)
{
8: if (h > 6)
{
9: h = 2;
}
10: x = 9;
11: y = 9;
}
}
12:}
void g (int a, int b)
{
0: int x, y;
1: x = 5;
2: y = 8;
3: h = 3;
4: if (x > 2)
{
5: if (h > a)
{
6: h = 1;
}
else
{
7: h = 2;
}
}
else
{
8: if (x > 3)
{
9: y = 3;
10: y = 2;
}
}
11: while (x > 9)
{
12: if (h > 0)
13: break;
14: if (h > 7)
{
15: h = 4;
}
16: y = 1;
17: h = 4;
}
18: }
int h;
void f (int a, int b) h f_a f_b f_x f_y g_x g_y g_a g_b
{
0: int x, y; {#,2,3,1} 2^32 2^32 # # {5,#} {8,#} 2^32 2^32
1: x = 4; {#,2,3,1} 2^32 2^32 # # {5,#} {8,#} 2^32 2^32
2: y = 4; {#,2,3,1} 2^32 2^32 4 # {5,#} {8,#} 2^32 2^32
3: h = 2; {#,2,3,1} 2^32 2^32 4 4 {5,#} {8,#} 2^32 2^32
4: if (x > 0) {2,3,1} 2^32 2^32 4 4 {5,#} {8,#} 2^32 2^32
{
5: h = 3; {2,3,1} 2^32 2^32 4 4 {5,#} {8,#} 2^32 2^32
6: if (y < 8) {2,3,1} 2^32 2^32 4 4 {5,#} {8,#} 2^32 2^32
{
7: if (h > 6) {2,3,1} 2^32 2^32 4 4 {5,#} {8,#} 2^32 2^32
{
8: h = 2; ________________________________________ ____________________________
}
9: x = 9; {2,3,1} 2^32 2^32 9 4 {5,#} {8,#} 2^32 2^32
10: y = 9; {2,3,1} 2^32 2^32 9 9 {5,#} {8,#} 2^32 2^32
}
}
11:} {2,3,1} 2^32 2^32 9 9 {5,#} {8,#} 2^32 2^32
void g (int a, int b) h f_a f_b f_x f_y g_x g_y g_a g_b
{
0: int x, y; {#,2,3} 2^32 2^32 {#,4,9} {#,4,9} # # 2^32 2^32
1: x = 5; {#,2,3} 2^32 2^32 {#,4,9} {#,4,9} # # 2^32 2^32
2: y = 8; {#,2,3} 2^32 2^32 {#,4,9} {#,4,9} 5 # 2^32 2^32
3: h = 3; {#,2,3} 2^32 2^32 {#,4,9} {#,4,9} 5 8 2^32 2^32
4: if (x > 2) {2,3} 2^32 2^32 {#,4,9} {#,4,9} 5 8 2^32 2^32
{
5: if (h > a) {2,3} 2^32 2^32 {#,4,9} {#,4,9} 5 8 2^32 2^32
{
6: h = 1; {2,3} 2^32 2^32 {#,4,9} {#,4,9} 5 8 2^32 2^32
}
else
{
7: h = 2; {2,3} 2^32 2^32 {#,4,9} {#,4,9} 5 8 2^32 2^32
}
}
else
{
8: if (x > 3) ________________________________________ __________________________
{
9: y = 3; ________________________________________ __________________________
10: y = 2; ________________________________________ __________________________
}
}
11: while (x > 9) {2,3,1} 2^32 2^32 {#,4,9} {#,4,9} 5 8 2^32 2^32
{
12: if (h > 0) ________________________________________ __________________________
13: break; ________________________________________ __________________________
14: if (h > 7) ________________________________________ __________________________
{
15: h = 4; ________________________________________ __________________________
}
16: y = 1; ________________________________________ __________________________
17: h = 4; ________________________________________ __________________________
}
18: } {2,3,1} 2^32 2^32 {#,4,9} {#,4,9} 5 8 2^32 2^32
1) Потенциальные состояния:
Ответ = 12*19*2^(32*9) = 228 * 2^(288)
12 состояний в 1 функции
19 во второй
9 переменных в функциях, каждая из которых может принимать 2^32 значений
2) Достижимые состояния:
Ответ = 4*3*3*2*2*2^(32*4)*11*10 = 15840*2^(128)
Составив таблицу сверху оцениваем мощность множества сверху:
Мощность h = 4
Мощность f_x = f_y = 3
Мощность g_x = g_y = 2
Мощность f_a = f_b = g_a = g_b = 2^32
Множество достижимых состояний f = 11
Множество достижимых состояний g = 10
((c_f >= 0 && с_f < 8) || (c_f >= 9 && c_f <= 11)) &&
((c_g >= 0 && c_g <= 5) || (c_g == 6 && h > a) || (c_g == 7 && h <= a) || (c_g == 11) || (c_g == 18 )) &&
(((f_x == #) || (f_x == 4) || (f_x == 9)) && ((f_y == #) || (f_y == 4) || (f_y == 9)) && ((g_x == #) || (g_x == 5)) && ((g_y == #) || (g_y == 8))
&& ((h == #) || (h == 2) || (h == 1) || (h == 3)))
Дано:
Дана текст программы на языке С с функциями f и g.
Предполагается, что функции f и g выполняются параллельно, в двух разных потоках управления (процессах) P_f и P_g соответственно. Будем считать состоянием модели программы совокупность значений счётчиков команд c_f и c_g процессов P_f и P_g, значения глобальных и локальных переменных заданной программы.
Неинициализированные переменные принимают специальное значение, обозначаемое символом #, лежащее вне диапазона MININT..MAXINT.
Требуется:
1. (5 баллов) Оценить размер множества потенциальных состояний программы. Ответ обосновать.
2. (10 баллов) Оценить размер множества достижимых состояний программы. Ответ обосновать. В обосновании описать множество достижимых состояний с помощью линейных равенств и неравенств на языке C.
Например, (c_f == 3 && a < 5) || (c_g == 4 && b > d).
3. (35 баллов) Написать программу на языке С, которая вычисляет и записывает в текстовой файл states.txt множество достижимых состояний заданной программы для заданных значений параметров функций, а также выводит в стандартный поток вывода количество достижимых состояний.
На выполнение задания отводится две недели.
Требования к файлам решения:
Решение задачи должно включать в себя 3 файла:
1.Исходная формулировка задачи с именем task.txt
2.Описание решения пп. 1-2 в текстовом файле с именем solution.txt. Текстовый файл должен быть в одной из кодировок: utf8, cp1251 (Windows), koi8-r. Файлы других форматов (doc, pdf, etc) не принимаются.
3.Файл group_surname.c с программой подсчёта состояний (group - номер вашей группы, surname - ваша фамилия латиницей).
Требования к программе:
1.Программа должны вычислять множество достижимых состояний программы, присланной вам на почту, для заданных значений параметров функций f и g.
2.Программа должна уметь выводить множество состояний в текстовой файл в формате: значение счётчика f, значение счётчика g, значение h, значение f.x, значение f.y, значение g.x, значение а.y, (через запятую) по одному состоянию в строке. Значения счётчиков нумеруются с 0. Первая строка файла должна содержать описание формата вывода, а именно: c_f, c_g, h, f.x, f.y, g.x, g.y. Обратите внимание, что смена состояния программы происходит после выполнения соответствующего оператора программы (например, присваивания).
3.Программа должны выполняться в консоли. Обязательными входными параметрами являются значения параметров функций a и b в следующем порядке:
имя_программы <f_a> <f_b> <g_a> <g_b>
Также должны поддерживаться параметры:
-file имя_файла - запись состояний в указанный файл,
-count - вывод общего количества состояний программы в стандартный поток вывода.
При запуске без параметров (либо с недостаточным количеством параметров) программа должна выводить информацию о программе, авторе, годе написания и параметрах запуска.
4.Исходный код программы должен содержать информацию об авторе и годе написания программы.
5.Программа должна быть написана на языке ANSI C либо ANSI/ISO C++.
6.Программа должна успешно компилироваться компилятором gcc со следующими параметрами: gcc -O2 -Wall -Werror -Wformat-security -Wignored-qualifiers -Winit-self -Wswitch-default -Wfloat-equal -Wshadow -Wpointer-arith -Wtype-limits -Wempty-body -Wlogical-op -Wstrict-prototypes -Wold-style-declaration -Wold-style-definition -Wmissing-parameter-type -Wmissing-field-initializers -Wnested-externs -Wno-pointer-sign.
7.Допускается использование только библиотек stdlib и STL.
8.Текст программы должен быть снабжён исчерпывающими комментариями. Как минимум, должны быть прокомментированы все объявления функций, операторы ветвления и линейные участки программы.
9.Программа должна быть написана самостоятельно. При заимствовании фрагментов кода из open-source проектов должен быть указан автор кода. Заимствовать код из решений предыдущего года не допускается. Если будет обнаружено, что несколько присланных решений написаны одним человеком, оценка будет снижена для всех похожих работ. Для анализа схожести кода будут использованы соответствующие инструментальные средства.
Методические указания по решению задания можно найти по адресу: http://savenkov.lvk.cs.msu.su/mc/method_ 1.pdf
Программа для анализа:
task1/116.txt
int h;
void
f (int a, int b)
{
int x, y;
x = 4;
y = 4;
h = 2;
if (x > 0)
{
h = 3;
if (y < 8)
{
if (h > 6)
{
h = 2;
}
x = 9;
y = 9;
}
}
}
void
g (int a, int b)
{
int x, y;
x = 5;
y = 8;
h = 3;
if (x > 2)
{
if (h > a)
{
h = 1;
}
else
{
h = 2;
}
}
else
{
if (x > 3)
{
y = 3;
y = 2;
}
}
while (x > 9)
{
if (h > 0)
break;
if (h > 7)
{
h = 4;
}
y = 1;
h = 4;
}
}
(Spin Version 6.0.1 -- 16 December 2010)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 56 byte, depth reached 18, errors: 0
52 states, stored
10 states, matched
62 transitions (= stored+matched)
1 atomic steps
hash conflicts: 0 (resolved)
2.501 memory usage (Mbyte)
unreached in proctype f
Task2.pml:15, state 8, "h = 2"
(1 of 20 states)
unreached in proctype g
Task2.pml:36, state 6, "h = 1"
Task2.pml:42, state 14, "y = 2"
Task2.pml:50, state 24, "((h>0))"
Task2.pml:50, state 24, "else"
Task2.pml:55, state 27, "h = 4"
Task2.pml:60, state 32, "h = 4"
(5 of 38 states)
unreached in init
(0 of 4 states)
pan: elapsed time 0.054 seconds
pan: rate 962.96296 states/second
digraph G {
0 [label = "0, #, #, #"];
1 [label = "1, #, 4, #"];
2 [label = "2, #, 4, 4"];
3 [label = "3, 2, 4, 4"];
4 [label = "4, 2, 4, 4"];
5 [label = "5, 3, 4, 4"];
6 [label = "6, 3, 4, 4"];
8 [label = "8, 3, 4, 4"];
9 [label = "9, 3, 9, 4"];
10 [label = "10, 3, 9, 9"];
0 -> 1 [label = "x = 4"];
1 -> 2 [label = "y = 4"];
2 -> 3 [label = "h = 2"];
3 -> 4 [label = "(x > 0)"];
4 -> 5 [label = "h = 3"];
5 -> 6 [label = "(y < 8)"];
6 -> 8 [label = "!(h > 6)"];
8 -> 9 [label = "x = 9"];
9 -> 10 [label = "y = 9"];
10 -> 10;
}
Распознанный текст из изображения:
о. о. о. о. о. о. о
вв х.у вв х.>
1. о. а. о. а, о„ о
а„ 1. а. о. а. а, о
вв хл вв хт х=с
г. о. о. 4. а. о. о
о. г. о. о, о. с. о
1. 1. О. О. О, О. О
ввх,с' х=4 В11 Х,С' '= 8
1. г. о. о. о..-. о
О. З. О. О. О. с. 8
з. о. о. 4. 4. а. о
г. 1. о, 4. о. о. о
0=2
= 8 ввх,т Ь=З
вв х.>
з, 1. а. 4, 4„ а, а 2. 1. О. 4. О. 5. О
1. з. а. о. а.:. 8
4. о. г. 4, 4. а. а
О. 4. 3, О. О. 5. 8
(х '-. 2>
Сх:. О>
Ь=З Вхл
вв х.т
1=2
З. 1. О. 4. 4,:. О
1. 4. з. о. а. -. 8
О.:. З. О. О,:. 8
.~. а. г. 4. 4. о. о
41144ОО
1Зааасх
Ь=З
(8.*2> Вх,т
'са а>
1=3
б. О. З, 4. 4. О. О
1. '. З. О. О. с. 8
О.;. З. О. О. -. 8
8> : 8>
х = 5 Сх ' 0>
Ь = 3
Сх 2> . = 4
'0>с - а> вв х.т
Ь = 2
вв В.>'
1=3
:, г. г. 4, 4.:. а
г. 5 з 4 о .- 8
1. 7. 3. О. О. 5. 8
-, о. з, 4. 4. а, а
0„ 11. 2. О. О, 5„ 8
б. 1. 3, 4. 4. О. О
б>' -' 8>
'Ос':б> ссх.т
Ь=З
<х г>
'с>с . В> = 4
Ь = 2 В х.у
ах 9>
б. 2. 3. 4. 4, 5. О
ЗЗг4458
3. с. 3. 4.-1. '. 8
1. 11. 1. О. О. 5. 8
О. 18. 2. О. О. '. 8
. 1. 3. 4. 4. О. О
2. 7. 3..1. О. с. 8
О, О. 3. 4. 4. О. О
'0>с- б>
(х ': О> Сх .. 2>
(х ': 2> 1 = 1
Ь = 3
'70 а> =4
0=2
Ьх *в> Вх.т
Сх . О>
Вхз
. -'. 3, .1. 4. 5. О
б. 3. 3. 4. 4. '. 8
4344 с Б
с 4144 - Б
4 с 1 145 Б
3. 7. 3. 4. 4. '. 8
1. 11. 1. 4. О. с. 8
1. 18. г. о. о.:. 8
9 1 3 4.-1. О. О
10. О. 3. 9. 4. О. О
х=5 'ОЬ.- б>
Ь = 3 (х - 2> бх '. О> Сх ' 2> Сх .-. О> '8>с.- а>
Ь = 3
'ОЬ. а> 1=2
0=2
Ьх 9> =4
вв В.с' =9
т=8
1=3
. 3. 3. 4. 4. '. 8
б. 4. 3. 4, 4. 5. 8
2. 1Б. 2, 4. О. 5. 8
9. 2. 3. 4, 4„ 5, О
3. 11. 2. 4. 4, 5„ 8
11. О, 3. 9. 9. О, О
10. 1, 3. 9. 4, 0„ 0
Ь=З 'Ос'-.а> (х-*о>
(х ' 2> 1 = 3
Ь = 2 '(х -. 9>
у. 8>
0=2
а->
Ввх.> =9
1=2
га. г. З. в. 4. -. О
9. 3. З.-с. 4. 5. 8
4, 11. 1. 4. 4. 5. Б
3. 18. 1. 4..1. с. 8
11. 1. 3. 9. 9. О. О
Ь=З 'ОЬ б>
0=2
0=2
х=с
11. 2. 3. 9. 9. 5. О
10. 3. 3. 9. 4. 5. Б
9. 4. 3. 4. 4. '. 8
'. 11. 1. 4. 4. с. 8
х=в х 2>
>. = в
1=3
1=3
11, 3, 3. 9. 9. ', 8
10, 4. 3. 9. 4. 5. 8
9. 5. 3, 4. 4. 5. 8
5. 18. 1. 4. 4. 5. 8
7. 7, 3. 4. 4. 5. 8
б. 11. 2. 4. 4. 5. 8
б. 11. 3. 4. 4. 5, 8
у. Б>
х = 9 'Ос ' а>
ах 9> 1=3
х 2>
1=3
у=в
11. 4. 3. 9. 9. '. В
10. 5. 3. 9. 4. 5. Б
В. 7. 3. 4. 4. 5. 8
. 11. 3. 4. 4. 5. 8
б. 18. 3. 4, 4. '. 8
'ОЬ . б>
ЬЬ' а> =9
Сх ' 2>
11. '. 3. В. 9. 5. 8
10. 7. 3. 9. 4. 5. Б
9. и . г. 4. 4.:. 8
. 18. 2. 4. 4. 5. В
9. 11. 3. 4. 4. с. 8
'ВЬ а>
10. 11. 1. В, 4, 5. 8
9. 18. 2. 4. 4. 5. 8
10. 11. 3. 9. 4, 5. 8
11. '.3. 9,9. 5 8
9. 18, 3. 4. 4. 5. 8
ах' 9> . =9
0=2
ах. 9> =9
11. 11. 2. 9. 9. 5. 8
10. 18. 1. 9. 4. 5. 8
11 11 3 '1 9 с Б
10. 18. 3. 9. 4. с. 8
'Сх -* 9> >' = 9
Ьх 9>
11. 18. 2. 9. 9. '. Б
11. 18. 3. 9. 9. 5. 8
вв х.> Сх О> х=с 1=2
сггаааа 4. г. г. 4. 4..-. о
3. 3. О. 4. 4. '. Б г. 4. з. 4. а.:. 8
4„ з. г. 4. 4. -. 8 3, 4. 3. 4. 4, '. 8
(х:. О> 1= 3 1=2
4. 4. 3. 4. 4. 5. 8 4. 4. 1. 4. 4. 5. 8
5. 3. 4. 4. '. 8 с, - г 4 4, - 8
б. с. 3. 4. 4. '. 8 5. . 3, 4. 4. '. 8
сх ' 2> су В 8> 'ОЬ -* а> 1 = 3 Ь = 3
Мс- > >М '> аут 8> 1=2
а -б> =г 17 8> '18 '-. 9>
. 11. 2. 4. 4. 5. 8 б. 18. 2. 4. 4. '. 8
Ь = 2 '0>с .* 6> Ьх-*9> у '8>
Ь = 2 = 9 Ьх ' 9> 'Ос.. 0>
4. , 3. 4. 4. 5. 8
'ас'-. а> сх ' о>
сх. О> Ьх 9> 4. 18. 2. 4. 4. 5. 8 Ьх.9> сс. О>
Ь::-*9> '. 8>
. 18. 3. 4. 4. 5. 8 Ьх '9> 'ОЬ.- б>
Распознанный текст из изображения:
~=3
чь-м
1=2
ю. г. -. в
'(х - 9)
г,г.:. з
digraph G {
0 [label = "0, #, #, #"];
1 [label = "1, #, 5, #"];
2 [label = "2, #, 5, 8"];
3 [label = "3, 3, 5, 8"];
4 [label = "4, 3, 5, 8"];
6 [label = "6, 3, 5, 8"];
10 [label = "10, 2, 5, 8"];
17 [label = "17, 2, 5, 8"];
0 -> 1 [label = "x = 5"];
1 -> 2 [label = "y = 8"];
2 -> 3 [label = "h = 3"];
3 -> 4 [label = "(x > 2)"];
4 -> 6 [label = "!(h > a)"];
6 -> 10 [label = "h = 2"];
10 -> 17 [label = "!(x > 9)"];
17 -> 17;
}
Возможно не удалось распознать кодировку файла
int h;
void
f (int a, int b)
{
int x, y;
0: x = 4;
1: y = 4;
2: h = 2;
3: if (x > 0)
{
4: h = 3;
5: if (y < 8)
{
6: if (h > 6)
{
7: h = 2;
}
8: x = 9;
9: y = 9;
}
}
}
10:
void
g (int a, int b)
{
int x, y;
0: x = 5;
1: y = 8;
2: h = 3;
3: if (x > 2)
{
4: if (h > a)
{
5: h = 1;
}
else
{
6: h = 2;
}
}
else
{
7: if (x > 3)
{
8: y = 3;
9: y = 2;
}
}
10: while (x > 9)
{
11: if (h > 0)
12: break;
13: if (h > 7)
{
14: h = 4;
}
15: y = 1;
16: h = 4;
}
}
17:
/*
* Function autofs4_wait at linux-2.6.38/fs/autofs4/waitq.c:341-523
* Allocation call kmalloc at 35
* Release call kfree at 69
* DEG: 14 LOC: 34
*/
int autofs4_wait(struct autofs_sb_info *sbi, struct dentry *dentry,
enum autofs_notify notify)
{
if (sbi->catatonic)
return -ENOENT;
if (!dentry->d_inode) {
return -ENOENT;
}
name = kmalloc(NAME_MAX + 1, GFP_KERNEL);
if (!name)
return -ENOMEM;
if (IS_ROOT(dentry) && autofs_type_trigger(sbi->type))
kfree(name);
return -ENOENT;
}
qstr.name = name;
if (mutex_lock_interruptible(&sbi->wq_mutex )) {
kfree(qstr.name);
return -EINTR;
}
if (ret <= 0) {
kfree(qstr.name);
return ret;
}
if (!wq) {
/* Create a new wait queue */
wq = kmalloc(sizeof(struct autofs_wait_queue),GFP_KERNEL);
if (!wq) {
kfree(qstr.name);
return -ENOMEM;
}
}
else {
kfree(qstr.name);
}
if (wq->name.name) {
spin_lock_irqsave(¤t->sighand->sig lock, irqflags);
spin_unlock_irqrestore(¤t->sighand ->siglock, irqflags);
spin_lock_irqsave(¤t->sighand->sig lock, irqflags);
spin_unlock_irqrestore(¤t->sighand ->siglock, irqflags);
}
if (!status) {
spin_lock(&sbi->fs_lock);
spin_unlock(&sbi->fs_lock);
}
if (!--wq->wait_ctr)
kfree(wq);
return status;
}
В ходе абстрации для построения модели были оставлены только те вызовы и
операторы, которые влияют на проверяемый свойства, а именно:
1) Вызовы функций kmalloc и free для 2 ресурсов (name и qw)
2) Вызовы функций spin_lock () и spin_unlock ()
3) Ветвления if, в которых есть вызовы из 1 и 2, а также выходы
из функции по return:
if (sbi->catatonic)
if (!dentry->d_inode)
if (!name)
if (IS_ROOT(dentry) && autofs_type_trigger(sbi->type))
if (mutex_lock_interruptible(&sbi->wq_mutex ))
if (ret <= 0)
if (!wq)
if (wq->name.name)
if (!status)
if (!--wq->wait_ctr)
Моделирование вложенных ветвелиний не нужно, т.к. это не влияет на
проверку заданных свойств:
if(1) if(1 & 2)
if(2) -> return;
return;
Также, возможно следующее упрощение:
if(1) if(1)
if(2) return;
return; ->
else
return;
T.к. проверка условия 2 не влияет на заданное свойство - выход из
функции происходит независимо от его выполнения.
Не учтённые ветвления сами не влияют ни на захват / освобождение ресурса,
ни на работу в критической секции.
В коде модели в комментариях указано каким исходным выражениям
соответствуют моделирующие их команды.
В моделе присутствует только 2 ресурса, не смотря на то, что в функции
используется 3. Это объясняется наличием присваивания, приравнивающего
ресурсы qstr.name = name. Таким образом моделировать необходимо только 2.
Для моделирования менеджера ресурсов были созданы 2 канала ch1 и ch2:
mtype = { ALLOC, FREE, OK, FAIL };
chan ch1 = [0] of { int, mtype };
chan ch2 = [0] of { int, mtype };
В ch1 процессы посылают свой pid и тип запроса (ALLOC, FREE).
Менеджер считывает их и посылает ответы в ch2 в виде pid
процесса-адресата и результата (OK, FAIL). Для обработкb результата в
дальнейшем будут использоваться переменые ans_1 и ans_2 - по одному на
каждый ресурс.
ans_1 используется для ресурса qstr.name = name
ans_2 используется для ресурса wq
Для моделирования критической секции использовался алгоритм Петерсона.
Т.к. процессам выдаются pid соответственно 1 и 2, а нумерация массива
идет с 0, то для обозначения одного процесса используется _pid ? 1,
а другого ? 2 - _pid.
bool flag[2];
int turn;
inline lock ()
{
flag[_pid - 1] = true;
turn = 2 - _pid;
(flag[2-_pid] == false) || (turn == _pid - 1);
}
inline unlock ()
{
flag[_pid - 1] = false;
}
0:proc - (:root:) creates proc 0 (:init:)
Starting process with pid 1
1:proc 0 (:init:) creates proc 1 (process)
1:proc 0 (:init:) task3.pml:127 (state 4)[(run process())]
Starting process with pid 2
2:proc 0 (:init:) creates proc 2 (process)
2:proc 0 (:init:) task3.pml:127 (state 2)[(run process())]
Starting manager with pid 3
3:proc 0 (:init:) creates proc 3 (manager)
3:proc 0 (:init:) task3.pml:127 (state 3)[(run manager())]
4:proc 2 (process) task3.pml:54 (state 3)[goto END]
5:proc 2 (process) task3.pml:54 (state 3)[(1)]
6:proc 1 (process) task3.pml:54 (state 3)[(1)]
9:proc 1 (process) task3.pml:60 (state 7)[(1)]
10:proc 2 (process) task3.pml:60 (state 7)[goto END]
11:proc 2 (process) task3.pml:54 (state 3)[(1)]
14:proc 1 (process) task3.pml:66 (state 9)[ch1!pid,ALLOC]
14:proc 3 (manager) task3.pml:41 (state 1)[ch1?cl_pid,ALLOC]
15:proc 3 (manager) task3.pml:41 (state 2)[ch2!cl_pid,FAIL]
15:proc 1 (process) task3.pml:67 (state 10)[ch2?pid,ans_1]
16:proc 2 (process) task3.pml:60 (state 7)[(1)]
17:proc 1 (process) task3.pml:70 (state 14)[((ans_1==FAIL))]
18:proc 1 (process) task3.pml:71 (state 12)[goto END]
20:proc 2 (process) task3.pml:66 (state 9)[ch1!pid,ALLOC]
20:proc 3 (manager) task3.pml:41 (state 1)[ch1?cl_pid,ALLOC]
21:proc 1 (process) task3.pml:54 (state 3)[(1)]
22:proc 3 (manager) task3.pml:41 (state 2)[ch2!cl_pid,FAIL]
22:proc 2 (process) task3.pml:67 (state 10)[ch2?pid,ans_1]
24:proc 1 (process) task3.pml:60 (state 7)[goto END]
25:proc 2 (process) task3.pml:70 (state 14)[((ans_1==FAIL))]
26:proc 1 (process) task3.pml:54 (state 3)[goto END]
27:proc 2 (process) task3.pml:71 (state 12)[goto END]
28:proc 1 (process) task3.pml:54 (state 3)[(1)]
29:proc 2 (process) task3.pml:54 (state 3)[(1)]
32:proc 1 (process) task3.pml:60 (state 7)[(1)]
34:proc 2 (process) task3.pml:60 (state 7)[goto END]
35:proc 2 (process) task3.pml:54 (state 3)[goto END]
36:proc 1 (process) task3.pml:66 (state 9)[ch1!pid,ALLOC]
36:proc 3 (manager) task3.pml:41 (state 1)[ch1?cl_pid,ALLOC]
37:proc 3 (manager) task3.pml:41 (state 2)[ch2!cl_pid,FAIL]
37:proc 1 (process) task3.pml:67 (state 10)[ch2?pid,ans_1]
38:proc 1 (process) task3.pml:70 (state 14)[((ans_1==FAIL))]
39:proc 1 (process) task3.pml:71 (state 12)[goto END]
40:proc 1 (process) task3.pml:54 (state 3)[goto END]
41:proc 1 (process) task3.pml:54 (state 3)[goto END]
42:proc 1 (process) task3.pml:54 (state 3)[(1)]
43:proc 2 (process) task3.pml:54 (state 3)[goto END]
44:proc 2 (process) task3.pml:54 (state 3)[(1)]
46:proc 1 (process) task3.pml:60 (state 7)[(1)]
48:proc 2 (process) task3.pml:60 (state 7)[(1)]
50:proc 1 (process) task3.pml:66 (state 9)[ch1!pid,ALLOC]
50:proc 3 (manager) task3.pml:42 (state 3)[ch1?cl_pid,ALLOC]
52:proc 3 (manager) task3.pml:42 (state 4)[ch2!cl_pid,OK]
52:proc 1 (process) task3.pml:67 (state 10)[ch2?pid,ans_1]
53:proc 2 (process) task3.pml:66 (state 9)[ch1!pid,ALLOC]
53:proc 3 (manager) task3.pml:41 (state 1)[ch1?cl_pid,ALLOC]
54:proc 1 (process) task3.pml:70 (state 14)[else]
56:proc 1 (process) task3.pml:26 (state 22)[(1)]
58:proc 3 (manager) task3.pml:41 (state 2)[ch2!cl_pid,FAIL]
58:proc 2 (process) task3.pml:67 (state 10)[ch2?pid,ans_1]
59:proc 1 (process) task3.pml:26 (state 29)[(1)]
60:proc 2 (process) task3.pml:70 (state 14)[((ans_1==FAIL))]
62:proc 2 (process) task3.pml:71 (state 12)[goto END]
63:proc 2 (process) task3.pml:54 (state 3)[goto END]
64:proc 1 (process) task3.pml:26 (state 36)[(1)]
66:proc 1 (process) task3.pml:93 (state 46)[ch1!pid,FREE]
66:proc 3 (manager) task3.pml:44 (state 7)[ch1?cl_pid,FREE]
67:proc 3 (manager) task3.pml:44 (state 8)[ch2!cl_pid,OK]
67:proc 1 (process) task3.pml:93 (state 47)[ch2?pid,ans_1]
68:proc 2 (process) task3.pml:54 (state 3)[(1)]
70:proc 2 (process) task3.pml:60 (state 7)[goto END]
71:proc 2 (process) task3.pml:54 (state 3)[(1)]
72:proc 1 (process) task3.pml:122 (state 84)[goto START]
74:proc 2 (process) task3.pml:60 (state 7)[goto END]
75:proc 2 (process) task3.pml:54 (state 3)[(1)]
76:proc 1 (process) task3.pml:54 (state 3)[(1)]
78:proc 1 (process) task3.pml:60 (state 7)[goto END]
79:proc 1 (process) task3.pml:54 (state 3)[goto END]
81:proc 1 (process) task3.pml:54 (state 3)[goto END]
82:proc 1 (process) task3.pml:54 (state 3)[(1)]
84:proc 2 (process) task3.pml:60 (state 7)[(1)]
86:proc 2 (process) task3.pml:66 (state 9)[ch1!pid,ALLOC]
86:proc 3 (manager) task3.pml:41 (state 1)[ch1?cl_pid,ALLOC]
87:proc 1 (process) task3.pml:60 (state 7)[(1)]
88:proc 3 (manager) task3.pml:41 (state 2)[ch2!cl_pid,FAIL]
88:proc 2 (process) task3.pml:67 (state 10)[ch2?pid,ans_1]
89:proc 2 (process) task3.pml:70 (state 14)[((ans_1==FAIL))]
91:proc 2 (process) task3.pml:71 (state 12)[goto END]
92:proc 1 (process) task3.pml:66 (state 9)[ch1!pid,ALLOC]
92:proc 3 (manager) task3.pml:41 (state 1)[ch1?cl_pid,ALLOC]
93:proc 3 (manager) task3.pml:41 (state 2)[ch2!cl_pid,FAIL]
93:proc 1 (process) task3.pml:67 (state 10)[ch2?pid,ans_1]
94:proc 2 (process) task3.pml:54 (state 3)[goto END]
95:proc 1 (process) task3.pml:70 (state 14)[((ans_1==FAIL))]
96:proc 2 (process) task3.pml:54 (state 3)[(1)]
98:proc 2 (process) task3.pml:60 (state 7)[(1)]
99:proc 1 (process) task3.pml:71 (state 12)[goto END]
100:proc 1 (process) task3.pml:54 (state 3)[(1)]
103:proc 1 (process) task3.pml:60 (state 7)[(1)]
105:proc 2 (process) task3.pml:66 (state 9)[ch1!pid,ALLOC]
105:proc 3 (manager) task3.pml:41 (state 1)[ch1?cl_pid,ALLOC]
106:proc 3 (manager) task3.pml:41 (state 2)[ch2!cl_pid,FAIL]
106:proc 2 (process) task3.pml:67 (state 10)[ch2?pid,ans_1]
107:proc 2 (process) task3.pml:70 (state 14)[((ans_1==FAIL))]
108:proc 2 (process) task3.pml:71 (state 12)[goto END]
109:proc 2 (process) task3.pml:54 (state 3)[(1)]
111:proc 1 (process) task3.pml:66 (state 9)[ch1!pid,ALLOC]
111:proc 3 (manager) task3.pml:41 (state 1)[ch1?cl_pid,ALLOC]
112:proc 2 (process) task3.pml:60 (state 7)[(1)]
113:proc 3 (manager) task3.pml:41 (state 2)[ch2!cl_pid,FAIL]
113:proc 1 (process) task3.pml:67 (state 10)[ch2?pid,ans_1]
115:proc 2 (process) task3.pml:66 (state 9)[ch1!pid,ALLOC]
115:proc 3 (manager) task3.pml:41 (state 1)[ch1?cl_pid,ALLOC]
116:proc 3 (manager) task3.pml:41 (state 2)[ch2!cl_pid,FAIL]
116:proc 2 (process) task3.pml:67 (state 10)[ch2?pid,ans_1]
117:proc 1 (process) task3.pml:70 (state 14)[((ans_1==FAIL))]
118:proc 1 (process) task3.pml:71 (state 12)[goto END]
119:proc 2 (process) task3.pml:70 (state 14)[((ans_1==FAIL))]
120:proc 2 (process) task3.pml:71 (state 12)[goto END]
121:proc 1 (process) task3.pml:54 (state 3)[(1)]
122:proc 2 (process) task3.pml:54 (state 3)[goto END]
123:proc 2 (process) task3.pml:54 (state 3)[(1)]
125:proc 2 (process) task3.pml:60 (state 7)[goto END]
127:proc 2 (process) task3.pml:54 (state 3)[(1)]
129:proc 2 (process) task3.pml:60 (state 7)[goto END]
130:proc 1 (process) task3.pml:60 (state 7)[goto END]
131:proc 1 (process) task3.pml:54 (state 3)[goto END]
132:proc 2 (process) task3.pml:54 (state 3)[goto END]
133:proc 2 (process) task3.pml:54 (state 3)[goto END]
134:proc 2 (process) task3.pml:54 (state 3)[goto END]
135:proc 2 (process) task3.pml:54 (state 3)[(1)]
137:proc 2 (process) task3.pml:60 (state 7)[(1)]
139:proc 1 (process) task3.pml:54 (state 3)[goto END]
140:proc 1 (process) task3.pml:54 (state 3)[(1)]
141:proc 2 (process) task3.pml:66 (state 9)[ch1!pid,ALLOC]
141:proc 3 (manager) task3.pml:41 (state 1)[ch1?cl_pid,ALLOC]
143:proc 1 (process) task3.pml:60 (state 7)[goto END]
144:proc 1 (process) task3.pml:54 (state 3)[(1)]
Вариант 11
Задача 1
После события 'значение глобальной переменной state равно enter_critical'
и до наступления события 'значение глобальной переменной state равно
leave_critical' верно: если наступило событие 'процесс p находится на
метке unlock', то до него было событие 'значение глобальной переменной
state равно unlocked'
#define p (state == enter_critical)
#define q (state == leave_critical)
#define p_un p@unlock
#define st_un (state == unlocked)
//[]((p && !q) -> ((r U q) || []r))
//define p W q = ([]p) | (p U q)
//P becomes true before R = !R W (P & !R)
//r = ([]!p_un || (!p_un U (st_un & !p_un)))
[]((p && !q) -> ((([]!p_un || (!p_un U (st_un & !p_un))) U q) || []([]!p_un || (!p_un U (st_un & !p_un)))))
Задача 2
До наступления события 'значение глобальной переменной state равно leave'
верно: всегда выполняется 'значение глобальной переменной x равно 3'
#define p (x == 3)
#define q (state == leave)
[](<>q -> (p U q))
Задача 3
Между событиями 'процесс p находится на метке iter_begin' и
'процесс p находится на метке iter_end' верно:
событие 'процесс p находится на метке sent' наступает не более одного раза
#define it_b p@iter_begin
#define it_e p@iter_end
#define it_s p@sent
[]((it_b && !it_e && <>it_e) -> ((([]!p || (p->[]!p)) U it_e))
1. p наступает не более одного раза
1.1 p наступает 0 раз
1.2 после p больше p не наступает
[](!p || (p->[]!p))
2. Между it_b и it_e берём из лекции
Задача 1
После события 'процесс p находится на метке iter_begin' и до наступления события
'процесс p находится на метке iter_end' верно:
после события 'значение глобальной переменной x равно 3' рано или
поздно наступит событие 'значение глобальной переменной y равно 5'
#define it_b p@iter_begin
#define it_e p@iter_end
#define p (x == 3)
#define q (y == 5)
[]( it_b -> ( (p -> (!it_e U (q && !it_e))) U it_e ) || ([](p -> <>q)) )
Задача 2
Между событиями 'процесс p находится на метке iter_begin' и 'процесс p находится
на метке iter_end' верно: если наступило событие
'значение глобальной переменной x равно 3',
то до него было событие 'значение глобальной переменной y равно 5'
#define it_b p@iter_begin
#define it_e p@iter_end
#define p (x == 3)
#define q (y == 5)
[]((it_b && !it_e && <>it_e) -> (!p U (q || it_e)))
Задача 3
После наступления события 'процесс p находится на метке iter_begin' верно:
событие 'значение глобальной переменной state равно locked'
наступает ровно один раз
#define it_b p@iter_begin
#define p (state == locked)
[](it_b -> (p -> ([]p || (p U []!p))))
чБТЙБОФ 11
ъБДБЮБ 1
рПУМЕ УПВЩФЙС 'ЪОБЮЕОЙЕ ЗМПВБМШОПК РЕТЕНЕООПК state ТБЧОП enter_critical' Й ДП ОБУФХРМЕОЙС УПВЩФЙС 'ЪОБЮЕОЙЕ ЗМПВБМШОПК РЕТЕНЕООПК state ТБЧОП leave_critical' ЧЕТОП: ЕУМЙ ОБУФХРЙМП УПВЩФЙЕ 'РТПГЕУУ p ОБИПДЙФУС ОБ НЕФЛЕ unlock', ФП ДП ОЕЗП ВЩМП УПВЩФЙЕ 'ЪОБЮЕОЙЕ ЗМПВБМШОПК РЕТЕНЕООПК state ТБЧОП unlocked'
ъБДБЮБ 2
дП ОБУФХРМЕОЙС УПВЩФЙС 'ЪОБЮЕОЙЕ ЗМПВБМШОПК РЕТЕНЕООПК state ТБЧОП leave' ЧЕТОП: ЧУЕЗДБ ЧЩРПМОСЕФУС 'ЪОБЮЕОЙЕ ЗМПВБМШОПК РЕТЕНЕООПК x ТБЧОП 3'
ъБДБЮБ 3
нЕЦДХ УПВЩФЙСНЙ 'РТПГЕУУ p ОБИПДЙФУС ОБ НЕФЛЕ iter_begin' Й 'РТПГЕУУ p ОБИПДЙФУС ОБ НЕФЛЕ iter_end' ЧЕТОП: УПВЩФЙЕ 'РТПГЕУУ p ОБИПДЙФУС ОБ НЕФЛЕ sent' ОБУФХРБЕФ ОЕ ВПМЕЕ ПДОПЗП ТБЪБ
C:\Vpnm>spin601.exe -N spec_1.ltl -t -p task5_ver_1.pml
Never claim moves to line 6 [(1)]
Starting process with pid 2
2: proc 0 (:init:) task5_ver_1.pml:124 (state 1) [(run process())]
Starting manager with pid 3
3: proc 0 (:init:) task5_ver_1.pml:124 (state 2) [(run manager())]
Never claim moves to line 4 [((!((process[1]._p==alloc))&&(process[1 ]._p==ST
ART)))]
5: proc 1 (process) task5_ver_1.pml:58 (state 1) [(1)]
Never claim moves to line 10 [(!((process[1]._p==alloc)))]
7: proc 1 (process) task5_ver_1.pml:65 (state 6) [goto END]
9: proc 1 (process) task5_ver_1.pml:119 (state 85) [(1)]
11: proc 1 (process) task5_ver_1.pml:58 (state 1) [(1)]
13: proc 1 (process) task5_ver_1.pml:65 (state 6) [goto END]
Never claim moves to line 11 [((!((process[1]._p==alloc))&&(process[1 ]._p==EN
D)))]
15: proc 1 (process) task5_ver_1.pml:119 (state 85) [(1)]
Never claim moves to line 14 [(1)]
spin: trail ends after 17 steps
#processes: 3
flag[0] = 0
flag[1] = 0
turn = 0
17: proc 2 (manager) task5_ver_1.pml:43 (state 9)
17: proc 1 (process) task5_ver_1.pml:57 (state 3)
17: proc 0 (:init:) task5_ver_1.pml:125 (state 4) <valid end state>
17: proc - (never_0) spec_1.ltl:15 (state 16) <valid end state>
3 processes created
C:\Vpnm>spin601.exe -N spec_2.ltl -t -p task5_ver_2.pml
Never claim moves to line 6 [(1)]
Starting process with pid 2
2: proc 0 (:init:) task5_ver_2.pml:120 (state 1) [(run process())]
Starting manager with pid 3
3: proc 0 (:init:) task5_ver_2.pml:120 (state 2) [(run manager())]
Never claim moves to line 4 [((!((process[1]._p==END))&&(process[1]. _p==STAR
T)))]
5: proc 1 (process) task5_ver_2.pml:53 (state 1) [(1)]
Never claim moves to line 20 [(!((process[1]._p==END)))]
7: proc 1 (process) task5_ver_2.pml:59 (state 5) [(1)]
9: proc 1 (process) task5_ver_2.pml:64 (state 9) [ch1!pid,ALLOC]
10: proc 2 (manager) task5_ver_2.pml:40 (state 3) [ch1?cl_pid,ALLOC]
12: proc 2 (manager) task5_ver_2.pml:40 (state 4) [ch2!cl_pid,OK]
13: proc 1 (process) task5_ver_2.pml:65 (state 10) [ch2?pid,ans]
15: proc 1 (process) task5_ver_2.pml:70 (state 13) [else]
Never claim moves to line 21 [(((!((process[1]._p==free))&&!((process [1]._p==
END)))&&(process[1]._p==alloc_done)))]
17: proc 1 (process) task5_ver_2.pml:28 (state 16) [(1)]
Never claim moves to line 27 [(!((process[1]._p==free)))]
19: proc 1 (process) task5_ver_2.pml:28 (state 17) [(1)]
21: proc 1 (process) task5_ver_2.pml:28 (state 23) [(1)]
23: proc 1 (process) task5_ver_2.pml:28 (state 24) [(1)]
25: proc 1 (process) task5_ver_2.pml:28 (state 30) [(1)]
27: proc 1 (process) task5_ver_2.pml:28 (state 31) [(1)]
29: proc 1 (process) task5_ver_2.pml:92 (state 44) [(1)]
31: proc 1 (process) task5_ver_2.pml:92 (state 45) [(1)]
33: proc 1 (process) task5_ver_2.pml:15 (state 48) [flag[(pid-1)] = 1]
35: proc 1 (process) task5_ver_2.pml:16 (state 49) [turn = (2-pid)]
37: proc 1 (process) task5_ver_2.pml:17 (state 50) [(((flag[(2-pid)]==0)||(
turn==(pid-1))))]
39: proc 1 (process) task5_ver_2.pml:98 (state 52) [(1)]
41: proc 1 (process) task5_ver_2.pml:22 (state 53) [flag[(pid-1)] = 0]
43: proc 1 (process) task5_ver_2.pml:15 (state 55) [flag[(pid-1)] = 1]
45: proc 1 (process) task5_ver_2.pml:16 (state 56) [turn = (2-pid)]
47: proc 1 (process) task5_ver_2.pml:17 (state 57) [(((flag[(2-pid)]==0)||(
turn==(pid-1))))]
49: proc 1 (process) task5_ver_2.pml:101 (state 59) [(1)]
51: proc 1 (process) task5_ver_2.pml:22 (state 60) [flag[(pid-1)] = 0]
53: proc 1 (process) task5_ver_2.pml:15 (state 65) [flag[(pid-1)] = 1]
55: proc 1 (process) task5_ver_2.pml:16 (state 66) [turn = (2-pid)]
57: proc 1 (process) task5_ver_2.pml:17 (state 67) [(((flag[(2-pid)]==0)||(
turn==(pid-1))))]
59: proc 1 (process) task5_ver_2.pml:109 (state 69) [(1)]
61: proc 1 (process) task5_ver_2.pml:22 (state 70) [flag[(pid-1)] = 0]
Never claim moves to line 25 [((!((process[1]._p==free))&&(process[1] ._p==END
)))]
63: proc 1 (process) task5_ver_2.pml:115 (state 75) [(1)]
Never claim moves to line 10 [(!((process[1]._p==free)))]
65: proc 1 (process) task5_ver_2.pml:53 (state 1) [(1)]
67: proc 1 (process) task5_ver_2.pml:59 (state 5) [(1)]
69: proc 1 (process) task5_ver_2.pml:64 (state 9) [ch1!pid,ALLOC]
70: proc 2 (manager) task5_ver_2.pml:39 (state 1) [ch1?cl_pid,ALLOC]
72: proc 2 (manager) task5_ver_2.pml:39 (state 2) [ch2!cl_pid,FAIL]
73: proc 1 (process) task5_ver_2.pml:65 (state 10) [ch2?pid,ans]
75: proc 1 (process) task5_ver_2.pml:69 (state 11) [((ans==FAIL))]
77: proc 1 (process) task5_ver_2.pml:115 (state 75) [(1)]
79: proc 1 (process) task5_ver_2.pml:53 (state 1) [(1)]
81: proc 1 (process) task5_ver_2.pml:59 (state 5) [(1)]
83: proc 1 (process) task5_ver_2.pml:64 (state 9) [ch1!pid,ALLOC]
84: proc 2 (manager) task5_ver_2.pml:39 (state 1) [ch1?cl_pid,ALLOC]
86: proc 2 (manager) task5_ver_2.pml:39 (state 2) [ch2!cl_pid,FAIL]
87: proc 1 (process) task5_ver_2.pml:65 (state 10) [ch2?pid,ans]
89: proc 1 (process) task5_ver_2.pml:69 (state 11) [((ans==FAIL))]
Never claim moves to line 11 [((!((process[1]._p==free))&&(process[1] ._p==END
)))]
91: proc 1 (process) task5_ver_2.pml:115 (state 75) [(1)]
Never claim moves to line 36 [(1)]
spin: trail ends after 92 steps
#processes: 3
flag[0] = 0
flag[1] = 0
turn = 1
92: proc 2 (manager) task5_ver_2.pml:38 (state 9)
92: proc 1 (process) task5_ver_2.pml:52 (state 3)
92: proc 0 (:init:) task5_ver_2.pml:121 (state 4) <valid end state>
92: proc - (never_0) spec_2.ltl:37 (state 44) <valid end state>
3 processes created
Строки
58 первое условие if - skip
65 второе условие if - goto END
Возврат из фунции без вызова alloc - условие не выполняется.
Строки
53 1 if - skip
592 if - skip
64req alloc
65alloc ok
702 if - skip
76check_error - skip
79check_error - skip
82check_error - skip
92внешний if - skip (free не выполняется)
98skip в критической секции
101skip в критической секции
105skip в критической секции
115END: goto START
Alloc выполнился успешно.
free не выполняется.
Доходим до END -> нарушение спецификации
Начать зарабатывать
zzyxel
