/** 1) В каждом вычислении рано или поздно происходит попытка захвата ресурса при помощи указанного вызова *alloc* **/
/** #define ASSERT_1 **/

/** 2) В каждом вычислении, после успешного захвата ресурса рано или поздно ресурс освобождается при помощи вызова *free* **/
/** #define ASSERT_2 **/

/** 3) На каждый вызов системной функции выделения и освобождения ресурса обязательно поступит отклик от менеджера  ресурсов **/
/** #define ASSERT_3 **/

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

bool turn;
bool flag[2];

#ifdef ASSERT_4
int critical_count = 0;
#endif

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);
	#ifdef ASSERT_4
	critical_count++;
	#endif
}

inline unlock_section()
{
	#ifdef ASSERT_4
	critical_count--;
	#endif
  flag[_pid - 2] = false;
}

#ifdef ASSERT_4
proctype check_critical_count()
{
	d_step
	{
		!(critical_count <= 1) -> assert(critical_count <= 1);
	}	
}
#endif

proctype memory_manager()
{
  int who;
	progress:
  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;

	#ifdef ASSERT_1
	bool alloc_made = false;
	#endif

	#ifdef ASSERT_2
	bool alloc_successful = false;
	bool free_successful = false;
	#endif

	#ifdef ASSERT_3
	bool gimme_call_send = false;
	bool gimme_call_answered = false;
	bool free_call_send = false;
	bool free_call_answered = false;	
	#endif  

start:
progress:
  if
    :: skip;
    :: 
    {			
      channel! _pid, FROM_P, GIMME;
			#ifdef ASSERT_3
			gimme_call_send = true;
			#endif
			#ifdef ASSERT_1
			alloc_made = true;
			#endif
      channel? _pid, FROM_M, result;
			#ifdef ASSERT_3
			gimme_call_answered = true;
			#endif
      if 
        :: (result == EPIC_FAIL) -> goto exit;
        :: else
      fi;
			#ifdef ASSERT_2
			alloc_successful = true;
			#endif
    }
    if
      :: skip;
      :: 
      {
        channel! _pid, FROM_P, FREE;
				#ifdef ASSERT_3
				free_call_send = true;
				#endif
        channel? _pid, FROM_M, result;
				#ifdef ASSERT_3
				free_call_answered = true;
				#endif
				#ifdef ASSERT_2
				if 
					:: (result == DONE) -> free_successful = true; 
					:: else
				fi;
				#endif
        goto exit;
      }    
      :: goto exit;
    fi;
    :: goto exit;
  fi;
  
  lock_section();
forever_lbl:
  if
    :: skip;
    :: goto forever_lbl;
  fi;
  unlock_section();

exit:
	#ifdef ASSERT_1
	assert(alloc_made);
	alloc_made = false;
	#endif

	#ifdef ASSERT_2
	assert(!alloc_successful || free_successful);
	alloc_successful = false;
	free_successful = false;
	#endif

	#ifdef ASSERT_3
	assert(!gimme_call_send || gimme_call_answered);
	gimme_call_send = false;
	gimme_call_answered = false;
	assert(!free_call_send  || free_call_answered);
	free_call_send = false;
	free_call_answered = false;
	#endif
  goto start;
}

init
{
  atomic
  {
    run memory_manager();
    run pcbit_receive();
    run pcbit_receive();
		#ifdef ASSERT_4
		run check_critical_count();
		#endif
  }
}