1) � ������ ���������� ���� ��� ������ ���������� ������� ������� ������� ��� ������ ���������� ������ *alloc*
#define c_start (pcbit_receive[2]@start)
#define c_exit  (pcbit_receive[2]@exit)
#define c_alloc (pcbit_receive[2]@alloc_lbl)

![](c_start -> (!c_exit U c_alloc))

2) � ������ ����������, ����� ��������� ������� ������� ���� ��� ������ ������ ������������� ��� ������ ������ *free*
#define c_free  (pcbit_receive[2]@free_lbl)

![]((c_start && <>c_exit) -> ((c_alloc -> (!c_exit U c_free)) U c_exit))

3) �� ������ ����� ��������� ������� ��������� � ������������ ������� ����������� �������� ������ �� ���������  ��������
#define c_gimme    (pcbit_receive[2]@gimme_lbl) 
#define c_gimme_ok (pcbit_receive[2]@gimme_ok_lbl)
#define c_free_ok  (pcbit_receive[2]@free_ok_lbl)

![]((c_start && <>c_exit) -> ((c_gimme -> (!c_exit U c_gimme_ok)) && (c_free -> (!c_exit U c_free_ok))) U c_exit)

4) � ����������� ������ (����� �������� spin_lock* � spin_unlock*) ����� ����������  �� ����� ������ ��������
#define c_forever_1 (pcbit_receive[2]@forever_lbl)
#define c_forever_2 (pcbit_receive[3]@forever_lbl)

<>(c_forever_1 && c_forever_2)

5) � ���� ����� �������� ������� ������� kfree ���������� �� ����� ������ ����
#define c_kfree (pcbit_receive[2]@free_lbl)

![]((c_start && <>c_exit) -> ((c_kfree -> ((c_kfree U c_exit) || (c_kfree U (!c_kfree U c_exit)))) U c_exit))