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;
    :: 
    {			
      channel! _pid, FROM_P, GIMME;
      channel? _pid, FROM_M, result;
      if 
        :: (result == EPIC_FAIL) -> goto exit;
        :: else
      fi;
    }
    if
      :: skip;
      :: 
      {
        channel! _pid, FROM_P, FREE;
        channel? _pid, FROM_M, result;
        goto exit;
      }    
      :: goto exit;
    fi;
    :: goto exit;
  fi;
  
  lock_section();
progress:
forever_lbl:
  if
    :: skip;
    :: goto forever_lbl;
  fi;
  unlock_section();

exit:
  goto start;
}

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