#ticktime 200
#monitor m WriterPreferenceReadWriteLock

#conditions 
	// ReaderLock.attempt(msecs)
	C1	0 iterations of the loop
	C2	1 iteration of the loop
	C3	many iterations of the loop
	// ReaderLock.acquire()
	C4	0 iterations of the loop
	C5	1 iteration of the loop
	C6	many iterations of the loop
	// WriterLock.attempt(msecs)
	C7	0 iterations of the loop
	C8	1 iteration of the loop
	C9	many iterations of the loop
	// WriterLock.acquire()
	C10	0 iterations of the loop
	C11	1 iteration of the loop
	C12	many iterations of the loop
	// processes suspended on the queue  (attempt)
	C13	no readers or writers waiting
	C14	1 reader waiting
	C15	1 writer waiting
	C16 	many readers waiting
	C17	many writers waiting
	C18	1 reader and 1 writer waiting with writer locking
	C19     1 reader and 1 writer waiting with reader locking
	C20	many readers and many writers waiting with writer locking
	C21     many readers and many writers waiting with reader locking
	       // endRead
	C22	no readers or writers waiting  (acquire)
	C23	1 reader waiting
	C24	1 writer waiting
	C25 	many readers waiting
	C26	many writers waiting
	C27	1 reader and 1 writer waiting with writer locking
	C28     1 reader and 1 writer waiting with reader locking
	C29	many readers and many writers waiting with writer locking
	C30     many readers and many writers waiting with reader locking
	       // endRead
#end

#top
import EDU.oswego.cs.dl.util.concurrent.*;
#end

//READERLOCK.ATTEMPT
// (T1) Test simple ReaderLock.attempt()
#begin
#test C1 C13
#tick
    #thread
        #excMonitor m.readLock().attempt(1000); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 2 #end
    #end
#end
#end 

 
// (T2) Test reader attempt waiting while writer writes
#begin
#test C2 C14
#tick
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread
        #excMonitor m.readLock().attempt(1000); #end
        #valueCheck time() # 3 #end
    #end
#end
#tick
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 3 #end
    #end
#end
#tick
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#end    


// READERLOCK.ACQUIRE

// (T3) Test simple ReaderLock.acquire()
#begin
#test C4 
#tick
    #thread
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 2 #end
    #end
#end
#end     

// (T4) Test reader acquire waiting while writer writes
#begin
#test C5  C23
#tick
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 3 #end
    #end
#end
#tick
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 3 #end
    #end
#end
#tick
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#end    


// WRITERLOCK.ATTEMPT
 
// (T5) Test simple WriterLock.attempt()
#begin
#test C7
#tick
    #thread
        #excMonitor m.writeLock().attempt(1000); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 2 #end
    #end
#end
#end   
              
// (T6) Test writer attempt waiting while reader reading
#begin
#test C8 C15
#tick
    #thread
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread 
        #excMonitor m.writeLock().attempt(1000); #end
        #valueCheck time() # 3 #end
    #end
#end
#tick
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 3 #end
    #end
#end
#tick
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#end    

// WRITERLOCK.ACQUIRE                   
// (T7) Test simple WriterLock.acquire()
#begin
#test C10 C22
#tick
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 2 #end
    #end
#end
#end                 

// (T8) Test writer acquire waiting while reader reading
#begin
#test C11 C24
#tick
    #thread
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread 
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 3 #end
    #end
#end
#tick
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 3 #end
    #end
#end
#tick
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#end                       

// PROCESSES SUSPENDED  ------------------------

// (T9) Test reader attempt waiting while writer waiting  (writer locking)
#begin
#test C18
#tick
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread
        #excMonitor m.readLock().attempt(1000); #end
        #valueCheck time() # 5 #end
    #end
#end
#tick
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#end               

// (T10) Test reader acquire waiting while writer waiting  (writer locking)
#begin
#test C27
#tick
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 5 #end
    #end
#end
#tick
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#end               


// (T11) Test reader attempt waiting while writer waiting (reader locking)
#begin
#test C19
#tick
    #thread
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick
    #thread
        #excMonitor m.readLock().attempt(1000); #end
        #valueCheck time() # 5 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#end        

// (T12) Test reader acquire waiting while writer waiting (reader locking)
#begin
#test C28
#tick
    #thread
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick
    #thread
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 5 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#end        


// (T13) Test readers attempt waiting while writer writing
#begin
#test C16 
#tick 
    #thread 
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick 
    #thread <r1>
        #excMonitor m.readLock().attempt(1000); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick 
    #thread <r2>
        #excMonitor m.readLock().attempt(1000); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick 
    #thread 
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick 
    #thread <r1>
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 5 #end
    #end
    #thread <r2>
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#end       

// (T14) Test many readers acquire waiting while writer writing
#begin
#test C25
#tick 
    #thread 
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick 
    #thread <r1>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick 
    #thread <r2>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick 
    #thread 
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick 
    #thread <r1>
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 5 #end
    #end
    #thread <r2>
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#end       

// (T15) Test many writers attempt waiting when multiple readers reading
#begin
#test C17
#shared <s>
    ConanVector validTimes = new ConanVector();
    public void setup() {
        validTimes.add(6);
        validTimes.add(7);
    }
#end
#tick 
    #thread
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 2 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().attempt(1000); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().attempt(1000); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#tick 
    #thread
	    #excMonitor m.writeLock().release(); #end
    	#valueCheck time() # 7 #end 
    #end                      
#end
#tick
    #thread
    	#excMonitor m.writeLock().release(); #end
    	#valueCheck time() # 8 #end
    #end
#end    
#end

 
// (T16) Test many writers acquire waiting when multiple readers reading
#begin
#test C26
#shared <s>
    ConanVector validTimes = new ConanVector();
    public void setup() {
        validTimes.add(6);
        validTimes.add(7);
    }
#end
#tick 
    #thread
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 2 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#tick 
    #thread
	    #excMonitor m.writeLock().release(); #end
    	#valueCheck time() # 7 #end 
    #end                      
#end
#tick
    #thread
    	#excMonitor m.writeLock().release(); #end
    	#valueCheck time() # 8 #end
    #end
#end    
#end



// (T17) Test readers attempt waiting and writers waiting with writer locking
#begin
#test C20
#shared <s>
    ConanVector validTimes = new ConanVector();
    public void setup() {
        validTimes.add(6);
        validTimes.add(7);
    }
#end
#tick 
    #thread 
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().attempt(2000); #end
        #valueCheck time() # 8 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().attempt(2000); #end
	    #valueCheck time() # 8 #end
	#end
#end
#tick 
    #thread
        #excMonitor m.writeLock().attempt(2000); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().attempt(2000); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 7 #end    
    #end                       
#end
#tick
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 8 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 9 #end
    #end   
#end
#tick
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 10 #end
    #end
#end    
#end 
     
// (T18) Test readers acquire waiting and writers waiting with writer locking
#begin
#test C29
#shared <s>
    ConanVector validTimes = new ConanVector();
    public void setup() {
        validTimes.add(6);
        validTimes.add(7);
    }
#end
#tick 
    #thread 
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 8 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().acquire(); #end
	    #valueCheck time() # 8 #end
	#end
#end
#tick 
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 7 #end    
    #end                       
#end
#tick
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 8 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 9 #end
    #end   
#end
#tick
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 10 #end
    #end
#end    
#end      

          
          
// (T19) Test many readers attempt waiting and writers waiting with reader locking
#begin
#test C21
#shared <s>
    ConanVector validTimes = new ConanVector();
    public void setup() {
        validTimes.add(6);
        validTimes.add(7);
    }
#end
#tick 
    #thread 
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().attempt(2000); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end 
#tick 
    #thread
        #excMonitor m.readLock().attempt(2000); #end
	    #valueCheck time() # 8 #end
	#end
#end
#tick 
    #thread
        #excMonitor m.readLock().attempt(2000); #end
	    #valueCheck time() # 8 #end
	#end
#end
#tick 
    #thread
        #excMonitor m.writeLock().attempt(2000); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 7 #end    
    #end                       
#end
#tick
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 8 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 9 #end
    #end   
#end
#tick
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 10 #end
    #end
#end    
#end 

                   
// (T20) Test many readers acquire waiting and writers waiting with reader locking
#begin
#test C30
#shared <s>
    ConanVector validTimes = new ConanVector();
    public void setup() {
        validTimes.add(6);
        validTimes.add(7);
    }
#end
#tick 
    #thread 
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end 
#tick 
    #thread
        #excMonitor m.readLock().acquire(); #end
	    #valueCheck time() # 8 #end
	#end
#end
#tick 
    #thread
        #excMonitor m.readLock().acquire(); #end
	    #valueCheck time() # 8 #end
	#end
#end
#tick 
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 7 #end    
    #end                       
#end
#tick
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 8 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 9 #end
    #end   
#end
#tick
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 10 #end
    #end
#end    
#end