Лабораторная работа: Вся решённая практика за семестр

int h;

proctype G (int a,b)

{

int x, y;

x = 1;

y = 1;

h = 0;

x = 3;

if

::(x > 5) ->

y = 2

::else

x = 6;

y = 2

fi;

do

:: (x > 1) ->

if

::(h > 0) -> break

::else

fi;

x = 7;

if

::(y > 7) ->

y = 3;

h = b

::else

fi

:: else break

od

}

proctype F (int a,b)

{

int x, y;

x = 4;

y = 3;

h = 3;

if

::(h > a)-> y = 5

::else

fi;

h = y;

if

::(x > 7) ->

if

::(h > x) ->

h = x;

y = 9

::else

fi

::else

fi

}

init{

atomic{

run G(3,4);run F(1,2)

}

}

Число потенциальных состояний для функции f

Переменных: 5 (a,b,h,x,y)

Операторов: 12

Потенциальных состояний - 12 * 2 ^(32 * 5) = 12 * 2^160

Число достижимых состояний для функции f

x принимает 3 значения (#, 5, 8)

y принимает 2 значения (#, 2)

Данный кусок кода не достижим, т.к. x = 2, а в условии y > 5

{

x = 2;

}

Итого: 10 * 3 * 2 * 2^96

(f_x == # || f_x == 5 || f_x == 8) && (f_y == # || f_y == 2) && (c_f != 8) && (c_f < 10)

Число потенциальных состояний для функции g

Переменных: 5(a,b,h,x,y)

Операторов: 18

Потенциальных состояний - 18 * 2^160

Число достижимых состояний для функции g

x принимает 3 значения (#, 10, 4)

y принимает 3 значения (#, 7, 6)

Данный кусок не достижим, т.к. x = 10, а в условии x < 0

{

if (y > 10)

{

if (h > 5)

{

x = 6;

h = 3;

}

x = 7;

}

}

Данный кусок не достижим, т.к. x = 10, а в условии x > 10

{

x = 2;

}

Итого: 12 * 3 * 3 * 2^96

(g_x == # || g_x == 10 || g_x == 4) && (g_y == # || g_y == 7 || g_y == 6) && (c_g < 4 || (c_g > 8 && c_g != 13 && c_g < 16))

Для всей программы.

В функциях f и g по 4 переменных и переменная h глобальная

Потенциальных: 12 * 18 * 2^(32*(4+4+1)) = 150 * 2^288

Достижимых: 10 * 3 * 2 * 12 * 3 * 3 * 2^(2*5) = 6480 * 2^160

int h;

void

f (int a, int b)

{

int x, y;

x = 4;

y = 3;

h = 3;

if (h > a)

{

y = 5;

}

h = y;

if (x > 7)

{

if (h > x)

{

h = x;

y = 9;

}

}

}

void

g (int a, int b)

{

int x, y;

x = 1;

y = 1;

h = 0;

x = 3;

if (x > 5)

{

y = 2;

}

else

{

x = 6;

y = 2;

}

while (x > 1)

{

if (h > 0)

break;

x = 7;

if (y > 7)

{

y = 3;

h = b;

}

}

}

D:\Univer\7sem\vpnm\Task_5>spin -p -t task5_check_2.pml

Never claim moves to line 145 [(1)]

Starting proc with pid 2

2: proc 0 (:init:) task5_check_2.pml:168 (state 1) [(run proc())]

Starting manager with pid 3

3: proc 0 (:init:) task5_check_2.pml:168 (state 2) [(run manager())

]

Never claim moves to line 143 [((!((proc._p==END))&&(proc._p==START))) ]

5: proc 1 (proc) task5_check_2.pml:30 (state 1) [(1)]

Never claim moves to line 149 [(!((proc._p==END)))]

7: proc 1 (proc) task5_check_2.pml:67 (state 7) [(1)]

Never claim moves to line 159 [(!((proc._p==END)))]

9: proc 1 (proc) task5_check_2.pml:30 (state 8) [(1)]

Never claim moves to line 150 [(((!((proc._p==END))&&!((proc._p==FFREE )))&&(pr

oc._p==ALLC)))]

11: proc 1 (proc) task5_check_2.pml:37 (state 14) [ask_m!pid,ALLOCATE]

12: proc 2 (manager) task5_check_2.pml:51 (state 1) [ask_m?p_pid,ALL

OCATE]

Never claim moves to line 154 [(!((proc._p==FFREE)))]

14: proc 2 (manager) task5_check_2.pml:51 (state 2) [ans_p!p_pid,OK]

15: proc 1 (proc) task5_check_2.pml:38 (state 15) [ans_p?pid,answer]

17: proc 1 (proc) task5_check_2.pml:77 (state 19) [else]

19: proc 1 (proc) task5_check_2.pml:82 (state 22) [(1)]

21: proc 1 (proc) task5_check_2.pml:30 (state 23) [(1)]

23: proc 1 (proc) task5_check_2.pml:88 (state 29) [(1)]

25: proc 1 (proc) task5_check_2.pml:91 (state 30) [(1)]

27: proc 1 (proc) task5_check_2.pml:30 (state 31) [(1)]

29: proc 1 (proc) task5_check_2.pml:107 (state 45) [(1)]

31: proc 1 (proc) task5_check_2.pml:30 (state 54) [(1)]

33: proc 1 (proc) task5_check_2.pml:17 (state 60) [interested[(pid-1)] = 1

]

35: proc 1 (proc) task5_check_2.pml:18 (state 61) [turn = (2-pid)]

<<<<<START OF CYCLE>>>>>

37: proc 1 (proc) task5_check_2.pml:19 (state 62) [(((turn!=(2-pid))||(int

erested[(2-pid)]!=1)))]

39: proc 1 (proc) task5_check_2.pml:123 (state 64) [(1)]

41: proc 1 (proc) task5_check_2.pml:24 (state 65) [interested[(pid-1)] = 0

]

43: proc 1 (proc) task5_check_2.pml:136 (state 72) [(1)]

45: proc 1 (proc) task5_check_2.pml:30 (state 1) [(1)]

47: proc 1 (proc) task5_check_2.pml:67 (state 7) [(1)]

49: proc 1 (proc) task5_check_2.pml:30 (state 8) [(1)]

51: proc 1 (proc) task5_check_2.pml:37 (state 14) [ask_m!pid,ALLOCATE]

52: proc 2 (manager) task5_check_2.pml:51 (state 1) [ask_m?p_pid,ALL

OCATE]

54: proc 2 (manager) task5_check_2.pml:51 (state 2) [ans_p!p_pid,OK]

55: proc 1 (proc) task5_check_2.pml:38 (state 15) [ans_p?pid,answer]

57: proc 1 (proc) task5_check_2.pml:77 (state 19) [else]

59: proc 1 (proc) task5_check_2.pml:82 (state 22) [(1)]

61: proc 1 (proc) task5_check_2.pml:30 (state 23) [(1)]

63: proc 1 (proc) task5_check_2.pml:88 (state 29) [(1)]

65: proc 1 (proc) task5_check_2.pml:91 (state 30) [(1)]

67: proc 1 (proc) task5_check_2.pml:30 (state 31) [(1)]

69: proc 1 (proc) task5_check_2.pml:107 (state 45) [(1)]

71: proc 1 (proc) task5_check_2.pml:30 (state 54) [(1)]

73: proc 1 (proc) task5_check_2.pml:17 (state 60) [interested[(pid-1)] = 1

]

75: proc 1 (proc) task5_check_2.pml:18 (state 61) [turn = (2-pid)]

spin: trail ends after 75 steps

#processes: 3

interested[0] = 1

interested[1] = 0

turn = 1

75: proc 2 (manager) task5_check_2.pml:50 (state 9)

75: proc 1 (proc) task5_check_2.pml:19 (state 62)

75: proc 0 (:init:) task5_check_2.pml:169 (state 4) <valid end state>

75: proc - (never_0) task5_check_2.pml:153 (state 19)

3 processes created

контрпример для

4.1. В ходе выполнения тела функции рано или поздно происходит попытка захвата ресурса при помощи указанного вызова *alloc*.

строки указаны для процесса proc

---------------------------------------- -

строка программы действие

63if_return();

29if ::true

66 if ::true

68if_return();

30if ::true -> goto END

135skip

(вот мы уже и на метке END, а alloc так и не случился)

1. В ходе выполнения тела функции рано или поздно происходит попытка захвата ресурса

при помощи указанного вызова *alloc*.

Модель модифицирована - запускается только один процесс, моделирующий функцию,

на котором свойство и проверяется.

#define start (proc@START)

#define end (proc@END)

#define allc (proc@ALLC)

/* ) */

2. В ходе выполнения тела функции после успешного захвата ресурса рано или поздно ресурс освобождается при помощи вызова *free*

Модель модифицирована - запускается только один процесс, моделирующий функцию,

на котором свойство и проверяется.

#define start (proc@START)

#define end (proc@END)

#define allc (proc@ALLC)

#define ffree (proc@FFREE)

/* ) U end)) */

3. На каждый вызов системной функции выделения и освобождения ресурса обязательно поступит отклик от менеджера ресурсов.

Модель модифицирована - запускается только один процесс, моделирующий функцию,

на котором свойство и проверяется.

#define start (proc@START)

#define end (proc@END)

#define allc (proc@ALLC)

#define ffree (proc@FFREE)

#define allc_ok (proc@ALLC)

#define ffree_ok (proc@FFREE)

/* )&&(ffree -> (!end U ffree_ok))) U end)) */

4. В критической секции (между вызовами spin_lock* и spin_unlock*) может находиться не более одного процесса.

#define locked_1 (proc[1]@LOCKED)

#define locked_2 (proc[2]@LOCKED)

/* <>(locked_1 && locked_2) */

5. В ходе выполнения тела функции, функция kfree вызывается не более одного раза.

Модель модифицирована - запускается только один процесс, моделирующий функцию,

на котором свойство и проверяется.

#define start (proc@START)

#define end (proc@END)

#define ffree (proc@FFREE)

/* )) */

D:\Univer\7sem\vpnm\Task_5>pan -a

warning: for p.o. reduction to be valid the never claim must be stutter-invarian

t

(never claims generated from LTL formulae are stutter-invariant)

pan:1: acceptance cycle (at depth 5)

pan: wrote task5_check_1.pml.trail

(Spin Version 6.0.1 -- 16 December 2010)

Warning: Search not completed

+ Partial Order Reduction

Full statespace search for:

never claim + (never_0)

assertion violations + (if within scope of claim)

acceptance cycles + (fairness disabled)

invalid end states - (disabled by never claim)

State-vector 40 byte, depth reached 12, errors: 1

7 states, stored

0 states, matched

7 transitions (= stored+matched)

1 atomic steps

hash conflicts: 0 (resolved)

2.501 memory usage (Mbyte)

pan: elapsed time 0.031 seconds

pan: rate 225.80645 states/second

D:\Univer\7sem\vpnm\Task_5>pan -a

warning: for p.o. reduction to be valid the never claim must be stutter-invarian

t

(never claims generated from LTL formulae are stutter-invariant)

pan:1: acceptance cycle (at depth 35)

pan: wrote task5_check_2.pml.trail

(Spin Version 6.0.1 -- 16 December 2010)

Warning: Search not completed

+ Partial Order Reduction

Full statespace search for:

never claim + (never_0)

assertion violations + (if within scope of claim)

acceptance cycles + (fairness disabled)

invalid end states - (disabled by never claim)

State-vector 40 byte, depth reached 74, errors: 1

72 states, stored (105 visited)

26 states, matched

131 transitions (= visited+matched)

1 atomic steps

hash conflicts: 0 (resolved)

2.501 memory usage (Mbyte)

pan: elapsed time 0.031 seconds

pan: rate 3387.0968 states/second

D:\Univer\7sem\vpnm\Task_5>pan -a

warning: for p.o. reduction to be valid the never claim must be stutter-invarian

t

(never claims generated from LTL formulae are stutter-invariant)

(Spin Version 6.0.1 -- 16 December 2010)

+ Partial Order Reduction

Full statespace search for:

never claim + (never_0)

assertion violations + (if within scope of claim)

acceptance cycles + (fairness disabled)

invalid end states - (disabled by never claim)

State-vector 40 byte, depth reached 90, errors: 0

146 states, stored (227 visited)

136 states, matched

363 transitions (= visited+matched)

1 atomic steps

hash conflicts: 0 (resolved)

2.501 memory usage (Mbyte)

unreached in proctype manager

task5_check_3.pml:58, state 12, "-end-"

(1 of 12 states)

unreached in proctype proc

task5_check_3.pml:142, state 74, "-end-"

(1 of 74 states)

unreached in claim never_0

task5_check_3.pml:176, state 40, "-end-"

(1 of 40 states)

unreached in init

(0 of 4 states)

pan: elapsed time 0.062 seconds

pan: rate 3661.2903 states/second

D:\Univer\7sem\vpnm\Task_5>pan -a

warning: for p.o. reduction to be valid the never claim must be stutter-invarian

t

(never claims generated from LTL formulae are stutter-invariant)

(Spin Version 6.0.1 -- 16 December 2010)

+ Partial Order Reduction

Full statespace search for:

never claim + (never_0)

assertion violations + (if within scope of claim)

acceptance cycles + (fairness disabled)

invalid end states - (disabled by never claim)

State-vector 44 byte, depth reached 1788, errors: 0

1770 states, stored

3778 states, matched

5548 transitions (= stored+matched)

2 atomic steps

hash conflicts: 12 (resolved)

2.501 memory usage (Mbyte)

unreached in proctype manager

task5_check_4.pml:55, state 12, "-end-"

(1 of 12 states)

unreached in proctype proc

task5_check_4.pml:139, state 74, "-end-"

(1 of 74 states)

unreached in claim never_0

task5_check_4.pml:149, state 8, "-end-"

(1 of 8 states)

unreached in init

(0 of 5 states)

pan: elapsed time 0.063 seconds

pan: rate 28095.238 states/second

D:\Univer\7sem\vpnm\Task_5>pan -a

warning: for p.o. reduction to be valid the never claim must be stutter-invarian

t

(never claims generated from LTL formulae are stutter-invariant)

(Spin Version 6.0.1 -- 16 December 2010)

+ Partial Order Reduction

Full statespace search for:

never claim + (never_0)

assertion violations + (if within scope of claim)

acceptance cycles + (fairness disabled)

invalid end states - (disabled by never claim)

State-vector 40 byte, depth reached 90, errors: 0

65 states, stored

37 states, matched

102 transitions (= stored+matched)

1 atomic steps

hash conflicts: 0 (resolved)

2.501 memory usage (Mbyte)

unreached in proctype manager

task5_check_5.pml:55, state 12, "-end-"

(1 of 12 states)

unreached in proctype proc

task5_check_5.pml:137, state 74, "-end-"

(1 of 74 states)

unreached in claim never_0

task5_check_5.pml:153, state 16, "-end-"

(1 of 16 states)

unreached in init

(0 of 4 states)

pan: elapsed time 0.063 seconds

pan: rate 1031.746 states/second

D:\Univer\7sem\vpnm\Task_5>spin -a task5.pml

D:\Univer\7sem\vpnm\Task_5>gcc -DNP -o pan pan.c

D:\Univer\7sem\vpnm\Task_5>pan -l

(Spin Version 6.0.1 -- 16 December 2010)

+ Partial Order Reduction

Full statespace search for:

never claim + (:np_:)

assertion violations + (if within scope of claim)

non-progress cycles + (fairness disabled)

invalid end states - (disabled by never claim)

State-vector 44 byte, depth reached 2006, errors: 0

3433 states, stored (4911 visited)

10954 states, matched

15865 transitions (= visited+matched)

4 atomic steps

hash conflicts: 16 (resolved)

2.598 memory usage (Mbyte)

unreached in proctype manager

task5.pml:49, state 12, "-end-"

(1 of 12 states)

unreached in proctype proc

task5.pml:132, state 74, "-end-"

(1 of 74 states)

unreached in init

(0 of 5 states)

pan: elapsed time 0.046 seconds

pan: rate 106760.87 states/second

D:\Univer\7sem\vpnm\Task_5>spin -a task5.pml

D:\Univer\7sem\vpnm\Task_5>gcc -DSAFETY -o pan pan.c

D:\Univer\7sem\vpnm\Task_5>pan

(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 36 byte, depth reached 677, errors: 0

1274 states, stored

1322 states, matched

2596 transitions (= stored+matched)

2 atomic steps

hash conflicts: 2 (resolved)

2.501 memory usage (Mbyte)

unreached in proctype manager

task5.pml:49, state 12, "-end-"

(1 of 12 states)

unreached in proctype proc

task5.pml:131, state 74, "-end-"

(1 of 74 states)

unreached in init

(0 of 5 states)

pan: elapsed time 0.031 seconds

pan: rate 41096.774 states/second

всё, что у меня было на компе, выгрузила сюда

п.с. по просьбе Смагина М.

******* №1. ********

int h;

void f (int a, int b)

{

int x, y;

1: x = 4;

2: y = 8;

3: h = 0;

4: if (h < b)

{

5: h = y + b;

6: x = 4;

}

7: if (h < y)

{

8: if (x > 5)

{

9: x = 3;

}

10: h = x;

}

}

void g (int a, int b)

{

int x, y;

1: x = 4;

2: y = 6;

3: h = 10;

4: if (x < 1)

{

5: y = 4;

6: y = 8;

}

else

{

7: if (x > 5)

{

8: x = 3;

}

9: x = 3;

}

10: while (x > 4)

{

11: if (h > 0)

12: break;

13: h = y - a;

14: if (x > 4)

{

15: x = 2;

}

16: h = b - a;

}

}

Общее количество переменных: 9 = 1 + 4 + 4

Счетчик f: 11 значений

Счетчик g: 17 значений

2 потока => 187 = 11 * 17 комбинаций

Потенкциальных состояний: 187 * (2^32 + 1)^9

******* №2. ********

ALL = 2^32 + 1

ha_fb_fx_fy_fa_gb_gx_gy_g

int h;

void f (int a, int b)

{

int x, y;

x = 4;{#,10}ALLALL{#}{#}ALLALL{#,4,3}{#,6}AL L^4*12

y = 8;{#,10}ALLALL{4}{#}ALLALL{#,4,3}{#,6}AL L^4*12

h = 0;{#,10}ALLALL{4}{8}ALLALL{#,4,3}{#,6}AL L^4*12

if (h < b){#,10,0}ALLALL{4}{8}ALLALL{#,4,3}{#,6} ALL^4*18

{

h = y + b;{#,10,0}ALLALL{4}{8}ALLALL{#,4,3}{#,6} ALL^4*18

x = 4;ALLALLALL{4}{8}ALLALL{#,4,3}{#,6}ALL^5 *6

}

if (h < y)ALLALLALL{4}{8}ALLALL{#,4,3}{#,6}ALL^5 *6

{

if (x > 5)ALLALLALL{4}{8}ALLALL{#,4,3}{#,6}ALL^5 *6

{

// x = 3;

}

h = x;ALLALLALL{4}{8}ALLALL{#,4,3}{#,6}ALL^5 *6

}

}

finishALLALLALL{4}{8}ALLALL{#,4,3}{#,6}A LL^5*6

234*ALL^4 + 120*ALL^5

void g (int a, int b)

{

int x, y;

x = 4;ALLALLALL {#,4}{#,8}ALLALL{#}{#}ALL^5*4

y = 6;ALLALLALL {#,4}{#,8}ALLALL{4}{#}ALL^5*4

h = 10;ALLALLALL {#,4}{#,8}ALLALL{4}{6}ALL^5*4

if (x < 1)ALLALLALL {#,4}{#,8}ALLALL{4}{6}ALL^5*4

{

// y = 4;

// y = 8;

}

else

{

if (x > 5)ALLALLALL {#,4}{#,8}ALLALL{4}{6}ALL^5*4

{

// x = 3;

}

x = 3;ALLALLALL {#,4}{#,8}ALLALL{4}{6}ALL^5*4

}

while (x > 4)ALLALLALL {#,4}{#,8}ALLALL{3}{6}ALL^5*4

// {

// if (h > 0)

// break;

// h = y - a;

// if (x > 4)

// {

// x = 2;

// }

// h = b - a;

}

}

finishALLALLALL {#,4}{#,8}ALLALL{3}{6}ALL^5*4

160*ALL^5

Всего достижимых состояний: (234*ALL^4 + 120*ALL^5)*160*ALL^5

Дан текст программы на языке С с функциями f и g. Предполагается, что функции f и g

могут выполняться параллельно в двух разных потоках управления

(процессах) P_f и P_g соответственно. Будем считать состоянием модели

значения счётчиков команд c_f и c_g процессов P_f и P_g, значения

глобальных и локальных переменных заданной программы.

Неинициализированные переменные принимают специальное значение,

обозначаемое символом #, лежащее вне диапазона MININT..MAXINT.

Требуется:

1. Оценить размер множества потенциальных состояний программы. Ответ

обосновать.

2. Оценить размер множества достижимых состояний программы. Ответ

обосновать. В обосновании описать множество достижимых состояний с

помощью линейных равенств и неравенств на языке C.

Например, (c_f == 3 && a < 5) || (c_g == 4 && b > d).

3. Написать программу на языке С, которая вычисляет и записывает в текстовой файл states.txt множество достижимых состояний заданной программы для значений параметров a = 1, b = 2, c = 3, d = 4., а также выводит в стандартный поток вывода количество достижимых состояний.

Starting :init: with pid 0

0:proc - (:root:) creates proc 0 (:init:)

Starting model with pid 1

1:proc 0 (:init:) creates proc 1 (model)

1:proc 0 (:init:) line 75 "pan_in" (state 4)[(run model())]

Starting model with pid 2

2:proc 0 (:init:) creates proc 2 (model)

2:proc 0 (:init:) line 77 "pan_in" (state 2)[(run model())]

Starting manager with pid 3

3:proc 0 (:init:) creates proc 3 (manager)

3:proc 0 (:init:) line 78 "pan_in" (state 3)[(run manager())]

4:proc 1 (model) line 23 "pan_in" (state 42)[(1)]

5:proc 1 (model) line 29 "pan_in" (state 4)[.(goto)]

6:proc 2 (model) line 23 "pan_in" (state 42)[goto :b0]

7:proc 1 (model) line 29 "pan_in" (state 5)[ch!alloc]

7:proc 3 (manager) line 62 "pan_in" (state 1)[ch?alloc]

7:proc 1 (model) line 29 "pan_in" (state -)[values: 1!alloc]

7:proc 3 (manager) line 62 "pan_in" (state -)[values: 1?alloc]

8:proc 3 (manager) line 64 "pan_in" (state 2)[ch!alloc_ok]

8:proc 1 (model) line 32 "pan_in" (state 8)[ch?alloc_ok]

8:proc 3 (manager) line 64 "pan_in" (state -)[values: 1!alloc_ok]

8:proc 1 (model) line 32 "pan_in" (state -)[values: 1?alloc_ok]

9:proc 2 (model) line 23 "pan_in" (state 42)[goto :b0]

10:proc 2 (model) line 23 "pan_in" (state 42)[goto :b0]

11:proc 1 (model) line 32 "pan_in" (state 9)[(1)]

12:proc 2 (model) line 23 "pan_in" (state 42)[(1)]

13:proc 1 (model) line 34 "pan_in" (state 11)[.(goto)]

14:proc 2 (model) line 29 "pan_in" (state 4)[.(goto)]

15:proc 2 (model) line 29 "pan_in" (state 5)[ch!alloc]

15:proc 3 (manager) line 62 "pan_in" (state 1)[ch?alloc]

15:proc 2 (model) line 29 "pan_in" (state -)[values: 1!alloc]

15:proc 3 (manager) line 62 "pan_in" (state -)[values: 1?alloc]

16:proc 3 (manager) line 64 "pan_in" (state 2)[ch!alloc_ok]

16:proc 2 (model) line 32 "pan_in" (state 8)[ch?alloc_ok]

16:proc 3 (manager) line 64 "pan_in" (state -)[values: 1!alloc_ok]

16:proc 2 (model) line 32 "pan_in" (state -)[values: 1?alloc_ok]

17:proc 1 (model) line 36 "pan_in" (state 12)[ch!free]

17:proc 3 (manager) line 68 "pan_in" (state 6)[ch?free]

17:proc 1 (model) line 36 "pan_in" (state -)[values: 1!free]

17:proc 3 (manager) line 68 "pan_in" (state -)[values: 1?free]

18:proc 3 (manager) line 69 "pan_in" (state 7)[ch!free_ok]

18:proc 1 (model) line 36 "pan_in" (state 13)[ch?free_ok]

18:proc 3 (manager) line 69 "pan_in" (state -)[values: 1!free_ok]

18:proc 1 (model) line 36 "pan_in" (state -)[values: 1?free_ok]

19:proc 2 (model) line 32 "pan_in" (state 9)[(1)]

20:proc 2 (model) line 34 "pan_in" (state 11)[.(goto)]

21:proc 1 (model) line 23 "pan_in" (state 44)[break]

22:proc 1 (model) line 54 "pan_in" (state 45)[goto B]

23:proc 1 (model) line 23 "pan_in" (state 42)[(1)]

24:proc 2 (model) line 34 "pan_in" (state 16)[(1)]

25:proc 2 (model) line 40 "pan_in" (state 17)[.(goto)]

26:proc 1 (model) line 29 "pan_in" (state 4)[.(goto)]

27:proc 1 (model) line 29 "pan_in" (state 5)[ch!alloc]

27:proc 3 (manager) line 62 "pan_in" (state 1)[ch?alloc]

27:proc 1 (model) line 29 "pan_in" (state -)[values: 1!alloc]

27:proc 3 (manager) line 62 "pan_in" (state -)[values: 1?alloc]

28:proc 3 (manager) line 64 "pan_in" (state 2)[ch!alloc_ok]

28:proc 1 (model) line 32 "pan_in" (state 8)[ch?alloc_ok]

28:proc 3 (manager) line 64 "pan_in" (state -)[values: 1!alloc_ok]

28:proc 1 (model) line 32 "pan_in" (state -)[values: 1?alloc_ok]

29:proc 1 (model) line 32 "pan_in" (state 9)[(1)]

30:proc 1 (model) line 34 "pan_in" (state 11)[.(goto)]

31:proc 2 (model) line 12 "pan_in" (state 23)[flag[procNum] = 1]

32:proc 1 (model) line 36 "pan_in" (state 12)[ch!free]

32:proc 3 (manager) line 68 "pan_in" (state 6)[ch?free]

32:proc 1 (model) line 36 "pan_in" (state -)[values: 1!free]

32:proc 3 (manager) line 68 "pan_in" (state -)[values: 1?free]

33:proc 2 (model) line 9 "pan_in" (state 19)[turn = (1-procNum)]

34:proc 2 (model) line 9 "pan_in" (state 20)[(((flag[(1-procNum)]==0)||(turn==pro cNum)))]

35:proc 2 (model) line 10 "pan_in" (state 21)[mutex = (mutex+1)]

36:proc 3 (manager) line 69 "pan_in" (state 7)[ch!free_ok]

36:proc 1 (model) line 36 "pan_in" (state 13)[ch?free_ok]

36:proc 3 (manager) line 69 "pan_in" (state -)[values: 1!free_ok]

36:proc 1 (model) line 36 "pan_in" (state -)[values: 1?free_ok]

Возможно не удалось распознать кодировку файла