#ticktime 200
#monitor m WriterPreferenceReadWriteLock

#conditions 
	// ReaderLock.attempt(msecs)
	C63	msec =< 0 and start read
	C64	msecs =< 0 and not start read
	C65	timeout
        C66     no timeout
	// WriterLock.attempt(msecs)
	C67	msecs =< 0 and start read
	C68	msecs =< 0 and not start read
	C69	timeout
	C70	no timeout
	// processes suspended on the queue  (attempt)
	C71	1 reader waiting
	C72	1 writer waiting
	C73	1 reader and 1 writer waiting with writer locking (to reader)
	C74	1 reader and 1 writer waiting with writer locking(to writer)
	C75     1 reader and 1 writer waiting with reader locking(to reader)
	C76     1 reader and 1 writer waiting with reader locking(to writer)
	C77 	many readers waiting
	C78	many writers waiting
	C79	many readers and many writers waiting on writer (to reader)
	C80	many readers and many writers waiting on writer (to writer)
	C81     many readers and many writers waiting on reader (to reader)
	C82     many readers and many writers waiting on reader (to writer)
	       // endRead

#end

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

//READERLOCK.ATTEMPT
// (T1) Test simple ReaderLock.attempt()
#begin
#test C63
#tick
    #thread
        #valueCheck m.readLock().attempt(-1) # true #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 fails
#begin
#test C64
#tick  //1
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick   //2
    #thread
        #valueCheck m.readLock().attempt(-1) # false #end
        #valueCheck time() # 2 #end
    #end
#end
#tick   //3
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 3 #end
    #end
#end
#end    




// WRITERLOCK.ATTEMPT
 
// (T5) Test simple WriterLock.attempt()
#begin
#test C67
#tick
    #thread
        #valueCheck m.writeLock().attempt(-1) # true #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 failing to wait 
#begin
#test C68
#tick //1
    #thread
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick //2
    #thread 
        #valueCheck m.writeLock().attempt(-1) # false #end
        #valueCheck time() # 2 #end
    #end
#end
#tick //3
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 3 #end
    #end
#end
#end    

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

// (T9) Test reader attempt timeout while writer locking
#begin
#test C65 C71
#tick //1
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick  //2
    #thread
        #valueCheck m.readLock().attempt(1) # false #end
        #valueCheck time() # 2 #end
    #end
#end
#tick //3
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 3 #end
    #end
#end
#end   
            
// (T9) Test reader attempt timeout while writer locking
#begin
#test C69 C72
#tick //1
    #thread
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick  //2
    #thread
        #valueCheck m.writeLock().attempt(100) # false #end
        #valueCheck time() # 2 #end
    #end
#end
#tick //3
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 3 #end
    #end
#end
#end               

// (T11) Test reader attempt timeout while writer waiting (reader locking)
#begin
#test C73
#tick //1
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick  //2
    #thread
        #valueCheck m.writeLock().attempt(1000) # true #end
        #valueCheck time() # 4 #end
    #end
#end
#tick  //3
    #thread
        #valueCheck m.readLock().attempt(100) # false #end
        #valueCheck time() # 3 #end
    #end
#end
#tick //4
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick //5
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#end 
       
// (T11) Test reader attempt timeout while writer waiting (writer locking)
#begin
#test C74
#tick //1
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick  //2
    #thread
        #valueCheck m.writeLock().attempt(100) # false #end
        #valueCheck time() # 2 #end
    #end
#end
#tick  //3
    #thread
        #valueCheck m.readLock().attempt(1000) # true #end
        #valueCheck time() # 4 #end
    #end
#end
#tick //4
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick //5
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#end        


// (T11) Test reader attempt timeout while writer waiting (writer locking)
#begin
#test C75
#tick //1
    #thread
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick  //2
    #thread
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick  //3
    #thread
        #valueCheck m.readLock().attempt(100) # false #end
        #valueCheck time() # 3 #end
    #end
#end
#tick //4
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick //5
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#end 
       
// (T11) Test reader attempt timeout while writer waiting (reader locking)
#begin
#test C76
#tick //1
    #thread
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick  //2
    #thread
        #valueCheck m.writeLock().attempt(100) # false #end
        #valueCheck time() # 2 #end
    #end
#end
#tick  //3
    #thread
        #valueCheck m.readLock().attempt(100) # true #end
        #valueCheck time() # 3 #end
    #end
#end
#tick //4
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick //5
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#end        



// (T13) Test readers attempt timout while writer writing
#begin
#test C77
#tick //1
    #thread 
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick //2
    #thread <r1>
        #valueCheck m.readLock().attempt(100) # false #end
        #valueCheck time() # 2 #end
    #end
#end
#tick //3
    #thread <r2>
        #valueCheck m.readLock().attempt(1000) # true #end
        #valueCheck time() # 4 #end
    #end
#end
#tick //4
    #thread 
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick //5
    #thread <r2>
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#end     
  
// (T13) Test readers attempt timout while writer writing
#begin
#test C78
#tick //1
    #thread 
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick //2
    #thread <r1>
        #valueCheck m.writeLock().attempt(100) # false #end
        #valueCheck time() # 2 #end
    #end
#end
#tick //3
    #thread <r2>
        #valueCheck m.writeLock().attempt(1000) # true #end
        #valueCheck time() # 4 #end
    #end
#end
#tick //4
    #thread 
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#tick //5
    #thread <r2>
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#end       


// (T17) Test readers attempt timeout and writers waiting with writer locking
#begin
#test C79
#shared <s>
    ConanVector validTimes = new ConanVector();
    public void setup() {
        validTimes.add(6);
        validTimes.add(7);
    }
#end
#tick //1
    #thread 
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick //2
    #thread
        #valueCheck m.readLock().attempt(1000) # true #end
        #valueCheck time() # 8 #end
    #end
#end
#tick //3
    #thread
        #valueCheck m.readLock().attempt(100) # false #end
        #valueCheck time() # 3 #end
	#end
#end
#tick //4
    #thread
        #valueCheck m.writeLock().attempt(1000) # true #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick //5
    #thread
        #valueCheck m.writeLock().attempt(1000) # true #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick //6
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#tick //7
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 7 #end    
    #end                       
#end
#tick //8
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 8 #end
    #end
#end
#tick //9
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 9 #end
    #end
#end    
#end 

// (T17) Test readers attempt timeout and writers waiting with writer locking
#begin
#test C80
#tick //1
    #thread 
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick //2
    #thread
        #valueCheck m.readLock().attempt(1000) # true #end
        #valueCheck time() # 7 #end
    #end
#end
#tick //3
    #thread
        #valueCheck m.readLock().attempt(1000) # true #end
        #valueCheck time() # 7 #end
	#end
#end
#tick //4
    #thread
        #valueCheck m.writeLock().attempt(100) # false #end
        #valueCheck time() # 4 #end
    #end
#end
#tick //5
    #thread
        #valueCheck m.writeLock().attempt(1000) # true #end
        #valueCheck time() # 6 #end
    #end
#end
#tick //6
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#tick //7
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 7 #end    
    #end                       
#end
#tick //8
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 8 #end
    #end
 #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 8 #end
    #end
#end    
#end 


// (T15) Test many writers attempt timeout when multiple readers reading
#begin
#test C81
#shared <s>
    ConanVector validTimes = new ConanVector();
    public void setup() {
        validTimes.add(6);
        validTimes.add(7);
    }
#end
#tick //1
    #thread
        #valueCheck m.readLock().attempt(1000) # true #end
        #valueCheck time() # 1 #end
    #end
#end
#tick //2
    #thread
         #valueCheck m.writeLock().attempt(2000) # true #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick //3
    #thread
         #valueCheck m.writeLock().attempt(2000) # true #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick //4
    #thread
        #valueCheck m.readLock().attempt(100) # false #end
        #valueCheck time() # 4 #end
    #end
#end
#tick //5
    #thread
        #valueCheck m.readLock().attempt(3000) # true #end
        #valueCheck time() # 8 #end
    #end
#end
#tick //6
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#tick //7
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 7 #end
    #end
#end
#tick //8
    #thread
	#excMonitor m.writeLock().release(); #end
    	#valueCheck time() # 8 #end 
    #end                      
#end
#tick //9
    #thread
    	#excMonitor m.readLock().release(); #end
    	#valueCheck time() # 9 #end
    #end
#thread 
    	#excMonitor m.readLock().release(); #end
    	#valueCheck time() # 9 #end
    #end
#end    
#end


// (T15) Test many writers attempt timeout when multiple readers reading
#begin
#test C82
#tick //1
    #thread
        #valueCheck m.readLock().attempt(1000) # true #end
        #valueCheck time() # 1 #end
    #end
#end
#tick //2
    #thread
         #valueCheck m.writeLock().attempt(100) # false #end
        #valueCheck time() # 2 #end
    #end
#end
#tick //3
    #thread
         #valueCheck m.writeLock().attempt(3000) # true #end
        #valueCheck time() # 6 #end
    #end
#end
#tick //4
    #thread
        #valueCheck m.readLock().attempt(1000) # true #end
        #valueCheck time() # 7 #end
    #end
#end
#tick //5
    #thread
        #valueCheck m.readLock().attempt(1000) # true #end
        #valueCheck time() # 7 #end
    #end
#end
#tick //6
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#tick //7
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 7 #end
    #end
#end
#tick //8
    #thread
    	#excMonitor m.readLock().release(); #end
    	#valueCheck time() # 8 #end
    #end
#thread 
    	#excMonitor m.readLock().release(); #end
    	#valueCheck time() # 8 #end
    #end
#end    
#end