public void pin( int frameNo ) throws InvalidFrameNumberException 
  {
    
    if ((frameNo < 0) || (frameNo >= (int)mgr.getNumBuffers())) {
   
      throw new InvalidFrameNumberException (null, "BUFMGR: BAD_BUFFRAMENO.");
    }


    (mgr.frameTable())[frameNo].pin();
    state_bit[frameNo].state = Pinned;
  }