/** 1) В каждом вычислении рано или поздно происходит попытка захвата ресурса при помощи указанного вызова *alloc*
		![](c_start -> (!c_exit U c_alloc))
**/
#define c_start (pcbit_receive[2]@start)
#define c_exit  (pcbit_receive[2]@exit)
#define c_alloc (pcbit_receive[2]@alloc_lbl)

/** 2) В каждом вычислении, после успешного захвата ресурса рано или поздно ресурс освобождается при помощи вызова *free*
		![]((c_start && <>c_exit) -> ((c_alloc -> (!c_exit U c_free)) U c_exit))
**/
#define c_free  (pcbit_receive[2]@free_lbl)

/** 3) На каждый вызов системной функции выделения и освобождения ресурса обязательно поступит отклик от менеджера  ресурсов
		![]((c_start && <>c_exit) -> ((c_gimme -> (!c_exit U c_gimme_ok)) && (c_free -> (!c_exit U c_free_ok))) U c_exit)
**/
#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)

/** 4) В критической секции (между вызовами spin_lock* и spin_unlock*) может находиться  не более одного процесса
		<>(c_forever_1 && c_forever_2)
**/
#define c_forever_1 (pcbit_receive[2]@forever_lbl)
#define c_forever_2 (pcbit_receive[3]@forever_lbl)

/** 5) В ходе одной итерации функции функция kfree вызывается не более одного раза
		![]((c_start && <>c_exit) -> ((c_kfree -> ((c_kfree U c_exit) || (c_kfree U (!c_kfree U c_exit)))) U c_exit))
**/
#define c_kfree (pcbit_receive[2]@free_lbl)


bool turn;
bool flag[2];

mtype = { FROM_M, FROM_P, DONE, EPIC_FAIL, GIMME, FREE };
chan channel = [0] of { int, mtype, mtype };

inline lock_section()
{
  flag[_pid - 2] = true;
  turn = _pid - 2;
  (flag[3 - _pid] == false || turn == 3 - _pid);
}

inline unlock_section()
{
  flag[_pid - 2] = false;
}

proctype memory_manager()
{
  int who;
  do
    ::channel? who, FROM_P, GIMME -> channel!who, FROM_M, DONE;
    ::channel? who, FROM_P, GIMME -> channel!who, FROM_M, EPIC_FAIL;    
    ::channel? who, FROM_P, FREE -> channel!who, FROM_M, DONE;
    ::channel? who, FROM_P, FREE -> channel!who, FROM_M, EPIC_FAIL;
  od;
}

proctype pcbit_receive()
{
  mtype result;

start:
  if
    :: skip;
    ::
    {	
			skip;
			alloc_lbl:
			gimme_lbl:
      channel! _pid, FROM_P, GIMME;			
      channel? _pid, FROM_M, result;
			gimme_ok_lbl:
      if 
        :: (result == EPIC_FAIL) -> goto exit;
        :: else
      fi;
    }
    if
      :: skip;
      :: 			
      {
				skip;
				free_lbl:
        channel! _pid, FROM_P, FREE;
        channel? _pid, FROM_M, result;
				free_ok_lbl:			
        goto exit;
      }    
      :: goto exit;
    fi;
    :: goto exit;
  fi;
  
  lock_section();
forever_lbl:
  if
    :: skip;
    :: goto forever_lbl;
  fi;
  unlock_section();

exit:
  goto start;
}

init
{
  atomic
  {
    run memory_manager();
    run pcbit_receive();
    run pcbit_receive();
  }
}