bool turn;
bool flag[2];

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

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

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

active 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;
}

active [2] 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();
FOREVER_LBL:
  if
    :: skip;
    :: goto FOREVER_LBL;
  fi;
  unlock_section();

exit:
  goto start;
}