---

WriterPreferenceReadWriteLock.java

class WriterPreferenceReadWriteLock 
{
     protected int activeReaders_;
     protected int activeWriter_;
     protected final WriterLock writerLock_;
     protected int waitingWriters_;
     protected final ReaderLock readerLock_;
     protected int waitingReaders_;
     
     public WriterPreferenceReadWriteLock()
     {
          this.activeReaders_ = 0;
          this.activeWriter_ = 0;
          this.waitingReaders_ = 0;
          this.waitingWriters_ = 0;
          this.readerLock_ = new ReaderLock(this);
          if (MainReadWriteLock.quantification$wl1  == null)
          if (Bandera.choose())
          MainReadWriteLock.quantification$wl1 = new WriterLock(this);
          if (MainReadWriteLock.quantification$wl2  == null)
          if (Bandera.choose())
          MainReadWriteLock.quantification$wl2 = new WriterLock(this);
          this.writerLock_ = new WriterLock(this);
     }
     
     protected synchronized boolean startReadFromNewReader ()
     {
          boolean pass = (this.startRead());
          if (!pass)
          {
               this.waitingReaders_ = (this.waitingReaders_ + 1);
          }
          return pass;
     }
     
     protected synchronized boolean startReadFromWaitingReader ()
     {
          boolean pass = (this.startRead());
          if (pass)
          {
               this.waitingReaders_ = (this.waitingReaders_ - 1);
          }
          return pass;
     }
     
     protected synchronized void cancelledWaitingReader ()
     {
          this.waitingReaders_ = (this.waitingReaders_ - 1);
     }
     
     protected synchronized boolean startRead ()
     {
          boolean allowRead = (this.allowReader());
          if (allowRead)
          {
               this.activeReaders_ = (this.activeReaders_ + 1);
          }
          return allowRead;
     }
     
     protected synchronized Signaller endRead ()
     {
          if (((this.activeReaders_ - 1) == 0) && (this.waitingWriters_ > 0))
          {
               return this.writerLock_;
          } else
          {
               return null;
          }
     }
     
     protected synchronized boolean startWriteFromNewWriter ()
     {
          boolean pass = (this.startWrite());
          if (!pass)
          {
               this.waitingWriters_ = (this.waitingWriters_ + 1);
          }
          return pass;
     }
     
     protected synchronized boolean startWriteFromWaitingWriter ()
     {
          boolean pass = (this.startWrite());
          if (pass)
          {
               this.waitingWriters_ = (this.waitingWriters_ - 1);
          }
          return pass;
     }
     
     protected synchronized void cancelledWaitingWriter ()
     {
          this.waitingWriters_ = (this.waitingWriters_ - 1);
     }
     
     protected synchronized boolean startWrite ()
     {
          boolean allowWrite = (this.activeReaders_ == 0);
          if (allowWrite)
          {
               this.activeWriter_ = 1;
          }
          return allowWrite;
     }
     
     protected synchronized Signaller endWrite ()
     {
          this.activeWriter_ = 0;
          if ((this.waitingReaders_ > 0) && (this.allowReader()))
          {
               return this.readerLock_;
          } else
          {
               if (this.waitingWriters_ > 0)
               {
                    return this.writerLock_;
               } else
               {
                    return null;
               }
          }
     }
     
     protected boolean allowReader ()
     {
          return (this.waitingWriters_ == 0);
     }
     
     public Sync readLock ()
     {
          return this.readerLock_;
     }
     
     public Sync writeLock ()
     {
          return this.writerLock_;
     }
}

---