#ticktime 400
#monitor m WriterPreferenceReadWriteLock

#conditions 
	    C31	 at start of ReaderLock.attempt
            C32	 during Wait of ReaderLock.attempt
	    C33	 at start of ReaderLock.acquire
            C34	 during Wait of ReaderLock.acquire
	    C35	 at start of WriterLock.attempt
            C36	 during Wait of WriterLock.attempt
	    C37	 at start of WriterLock.acquire
            C38	 during Wait of WriterLock.acquire

	    // attempt

	    C39	1 reader waiting,
	    C40	1 writer waiting,
	    C41 1 writer and 1 reader waiting on a writer (interrupt reader),
	    C42 1 writer and 1 reader waiting on a writer (interrupt writer),
	    C43 1 writer and 1 reader waiting on a reader (interrupt reader),
            C44 1 writer and 1 reader waiting on a reader (interrupt writer),
	    C45 many readers waiting,
	    C46 many writers waiting,
	    C47 many writers and many readers waiting on a writer 
		//(interrupt reader), 
	    C48 many writers and many readers waiting on a writer 
		//(interrupt writer), 
	    C49 many writers and many readers waiting on a reader 
		//(interrupt reader)
	    C50 many writers and many readers waiting on a reader 
                //(interrupt writer)

            // acquire

	    C51 1 reader waiting,
	    C52 1 writer waiting,
	    C53 1 writer and 1 reader waiting on a writer (interrupt reader),
	    C54 1 writer and 1 reader waiting on a writer (interrupt writer),
	    C55 1 writer and 1 reader waiting on a reader (interrupt reader),
            C56 1 writer and 1 reader waiting on a reader (interrupt writer),
	    C57 many readers waiting,
	    C58 many writers waiting,
	    C59 many writers and many readers waiting on a writer 
		//(interrupt reader), 
	    C60 many writers and many readers waiting on a writer 
		//(interrupt writer), 
	    C61 many writers and many readers waiting on a reader 
		// (interrupt reader)
	    C62 many writers and many readers waiting on a reader 
		//(interrupt writer)
#end

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


//ATTEMPT
//(T21) Test interupt waiting reader attempt
#begin
#test C39
#tick
    #thread <t1>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread <t2>
        #excMonitor m.readLock().attempt(1000); # new InterruptedException() #end
        #valueCheck time() #  3 #end
    #end
#end
#tick
    #thread <t3>
        thread("t2").interrupt();
        #valueCheck time() #  3 #end
    #end
#end
#tick
    #thread <t1>
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#end  

//(T22) Test interrupt waiting reader attempt with 1 waiting reader
#begin
#test C45
#tick
    #thread <t1>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread <t2>
        #excMonitor m.readLock().attempt(1000); # new InterruptedException() #end
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t3>
        #excMonitor m.readLock().attempt(1000); #end
        #valueCheck time() #  5 #end
    #end
#end
#tick
    #thread <t4>
        thread("t2").interrupt();
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t1>
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#tick
    #thread <t3>
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#end 
 
//(T23) Test interrupt waiting reader attempt with 1 waiting writer
#begin
#test C41
#tick
    #thread <t1>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread <t2>
        #excMonitor m.readLock().attempt(1000); # new InterruptedException() #end
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t3>
        #excMonitor m.writeLock().attempt(1000); #end
        #valueCheck time() #  5 #end
    #end
#end
#tick
    #thread <t4>
        thread("t2").interrupt();
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t1>
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#tick
    #thread <t3>
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#end  


//(T24) Test interrupt waiting writer access with 1 waiting reader
#begin
#test C54
#tick
    #thread <t1>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread <t2>     
        #excMonitor m.readLock().attempt(1500);  #end
        #valueCheck time() #  5 #end
    #end
#end
#tick
    #thread <t3>
        #excMonitor m.writeLock().attempt(1000); # new InterruptedException() #end
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t4>
        thread("t3").interrupt();
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t1>
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#tick
    #thread <t2>
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#end  

//(T25) Test interrupt waiting writer attempt
#begin
#test C40
#tick
    #thread <t1>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread <t2>
        #excMonitor m.writeLock().attempt(1000); # new InterruptedException() #end
        #valueCheck time() #  3 #end
    #end
#end
#tick
    #thread <t3>
        thread("t2").interrupt();
        #valueCheck time() #  3 #end
    #end
#end
#tick
    #thread <t1>
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#end  

//(T26) Test interrupt waiting reader attempt with 1 waiting writer
#begin
#test C43
#tick
    #thread <t1>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread <t2>       
        #excMonitor m.writeLock().attempt(10000); #end
        #valueCheck time() #  5 #end
    #end
#end
#tick
    #thread <t3>
        #excMonitor m.readLock().attempt(10000); # new InterruptedException() #end
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t4>
        thread("t3").interrupt();
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t1>
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 5 #end
    #end
    #thread <t2>
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#end 

//(T27) Test interrupt waiting writer attempt with 1 waiting reader
#begin
#test C44
#tick
    #thread <t1>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread <t2>
        #excMonitor m.writeLock().attempt(10000); # new InterruptedException() #end
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t3>
        #excMonitor m.readLock().attempt(10000); #end
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t4>
        thread("t2").interrupt();
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t1>
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 5 #end
    #end
    #thread <t3>
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#end 
 
//(T28) Test interrupt waiting writer attempt with 1 waiting writer
#begin
#test C46
#tick
    #thread <t1>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread <t2>
        #excMonitor m.writeLock().attempt(10000); # new InterruptedException() #end
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t3>
        #excMonitor m.writeLock().attempt(10000); #end
        #valueCheck time() #  5 #end
    #end
#end
#tick
    #thread <t4>
        thread("t2").interrupt();
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t1>
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#tick
    #thread <t3>
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#end  

// (T29) Test 3 readers waiting and 3 writers waiting (interrupt reader)
#begin
#test C47
#shared <s>

    ConanVector validTimes = new ConanVector();
    public void setup() {
        validTimes.add(9);
        validTimes.add(10);
        validTimes.add(11);
    }
#end
#tick    //1
    #thread <t11>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick    //2
    #thread <t12>
        #excMonitor m.readLock().attempt(10000); # new InterruptedException() #end
        #valueCheck time() # 8 #end
    #end
#end
#tick    //3
    #thread <t13>
        #excMonitor m.writeLock().attempt(10000); #end
        #valueCheck time() # s.validTimes # CollectionRemove  #end
    #end
#end
#tick    //4
    #thread <t14>
        #excMonitor m.writeLock().attempt(10000); #end
        #valueCheck time() # s.validTimes # CollectionRemove  #end
    #end
#end
#tick     //5
    #thread <t15>
        #excMonitor m.readLock().attempt(10000); #end
	    #valueCheck time() # 12 #end
	#end
#end
#tick     //6
    #thread <t16>
        #excMonitor m.writeLock().attempt(10000); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick     //7
    #thread <t17>
        #excMonitor m.readLock().attempt(10000); #end
        #valueCheck time() # 12 #end
    #end
#end  
#tick     //8
    #thread <t18>
        thread("t12").interrupt();
        #valueCheck time() #  8 #end
    #end
#end
#tick     //9
    #thread <t11>
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 9 #end
    #end
#end
#tick     //10
    #thread 
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 10 #end
    #end
#end
#tick     //11
    #thread 
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 11 #end    
    #end                       
#end
#tick     //12
    #thread 
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 12 #end
    #end
#end
#tick      //13
    #thread 
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 13 #end
    #end   
    #thread 
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 13 #end
    #end
#end    
#end   
   
// (T30) Test 3 readers waiting and 3 writers waiting (interrupt writer)
#begin
#test C48
#shared <s>
    ConanVector validTimes = new ConanVector();
    public void setup() {
        validTimes.add(9);
        validTimes.add(10);
    }
#end
#tick  //1
    #thread <t21>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick   //2
    #thread <t22>
        #excMonitor m.readLock().attempt(10000); #end
        #valueCheck time() # 11 #end
    #end
#end
#tick   //3
    #thread <t23>
        #excMonitor m.writeLock().attempt(10000); # new InterruptedException() #end
        #valueCheck time() # 8 #end
    #end
#end
#tick   //4
    #thread <t24>
        #excMonitor m.writeLock().attempt(10000); #end
        #valueCheck time() # s.validTimes # CollectionRemove  #end
    #end
#end
#tick   //5
    #thread <t25>
        #excMonitor m.readLock().attempt(10000); #end
	    #valueCheck time() # 11 #end
	#end
#end
#tick   //6
    #thread <t26>
        #excMonitor m.writeLock().attempt(10000); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick 
    #thread <t27>
        #excMonitor m.readLock().attempt(10000); #end
        #valueCheck time() # 11 #end
    #end
#end  
#tick
    #thread <t28>
        thread("t23").interrupt();
        #valueCheck time() #  8 #end
    #end
#end
#tick 
    #thread <t21>
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 9 #end
    #end
#end
#tick 
    #thread 
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 10 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 11 #end    
    #end                       
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 12 #end
    #end   
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 12 #end
    #end
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 12 #end
    #end
#end    
#end      

// (T31) Test 3 readers waiting and 3 writers waiting (interrupt reader)
#begin
#test C49
#shared <s>

    ConanVector validTimes = new ConanVector();
    public void setup() {
        validTimes.add(9);
        validTimes.add(10);
        validTimes.add(11);
    }
#end
#tick 
    #thread <t31>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick 
    #thread <t32>
        #excMonitor m.writeLock().attempt(10000); #end
        #valueCheck time() # s.validTimes # CollectionRemove  #end
    #end
#end
#tick 
    #thread <t33>
        #excMonitor m.readLock().attempt(10000); # new InterruptedException() #end
        #valueCheck time() # 8 #end
    #end
#end
#tick 
    #thread <t44>
        #excMonitor m.writeLock().attempt(10000); #end
        #valueCheck time() # s.validTimes # CollectionRemove  #end
    #end
#end
#tick 
    #thread <t45>
        #excMonitor m.readLock().attempt(10000); #end
	    #valueCheck time() # 12 #end
	#end
#end
#tick 
    #thread <t46>
        #excMonitor m.writeLock().attempt(10000); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick 
    #thread <t47>
        #excMonitor m.readLock().attempt(10000); #end
        #valueCheck time() # 12 #end
    #end
#end  
#tick
    #thread <t48>
        thread("t33").interrupt();
        #valueCheck time() #  8 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 9 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 10 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 11 #end    
    #end                       
#end
#tick
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 12 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 13 #end
    #end   
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 13 #end
    #end
#end    
#end      

// (T32) Test 3 readers waiting and 3 writers waiting (interrupt writer)
#begin
#test C50
#shared <s>

    ConanVector validTimes = new ConanVector();
    public void setup() {
        validTimes.add(9);
        validTimes.add(10);
    }
#end
#tick 
    #thread <t51>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick 
    #thread <t52>
        #excMonitor m.writeLock().attempt(10000); # new InterruptedException() #end
        #valueCheck time() # 8  #end
    #end
#end
#tick 
    #thread <t53>
        #excMonitor m.readLock().attempt(10000); #end
        #valueCheck time() # 11 #end
    #end
#end
#tick 
    #thread <t54>
        #excMonitor m.writeLock().attempt(10000); #end
        #valueCheck time() # s.validTimes # CollectionRemove  #end
    #end
#end
#tick 
    #thread <t55>
        #excMonitor m.readLock().attempt(10000); #end
	    #valueCheck time() # 11 #end
	#end
#end
#tick 
    #thread <t56>
        #excMonitor m.writeLock().attempt(10000); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick 
    #thread <t57>
        #excMonitor m.readLock().attempt(10000); #end
        #valueCheck time() # 11 #end
    #end
#end  
#tick
    #thread <t58>
        thread("t52").interrupt();
        #valueCheck time() #  8 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 9 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 10 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 11 #end    
    #end                       
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 12 #end
    #end   
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 12 #end
    #end
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 12 #end
    #end
#end    
#end      


// ACCESS
//(T33) Test interupt waiting reader access
#begin
#test C51
#tick
    #thread <t1>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread <t2>
        #excMonitor m.readLock().acquire(); # new InterruptedException() #end
        #valueCheck time() #  3 #end
    #end
#end
#tick
    #thread <t3>
        thread("t2").interrupt();
        #valueCheck time() #  3 #end
    #end
#end
#tick
    #thread <t1>
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#end  

//(T34) Test interrupt waiting reader access with 1 waiting reader
#begin
#test C57
#tick
    #thread <t1>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread <t2>
        #excMonitor m.readLock().acquire(); # new InterruptedException() #end
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t3>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() #  5 #end
    #end
#end
#tick
    #thread <t4>
        thread("t2").interrupt();
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t1>
        #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 
 
//(T35) Test interrupt waiting reader access with 1 waiting writer
#begin
#test C53
#tick
    #thread <t1>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread <t2>
        #excMonitor m.readLock().acquire(); # new InterruptedException() #end
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t3>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() #  5 #end
    #end
#end
#tick
    #thread <t4>
        thread("t2").interrupt();
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t1>
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#tick
    #thread <t3>
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#end  


//(T36) Test interrupt waiting writer access with 1 waiting reader
#begin
#test C54
#tick
    #thread <t1>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread <t2>     
        #excMonitor m.readLock().acquire();  #end
        #valueCheck time() #  5 #end
    #end
#end
#tick
    #thread <t3>
        #excMonitor m.writeLock().acquire(); # new InterruptedException() #end
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t4>
        thread("t3").interrupt();
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t1>
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#tick
    #thread <t2>
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#end  

//(T37) Test interupt waiting writer access
#begin
#test C52
#tick
    #thread <t1>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread <t2>
        #excMonitor m.writeLock().acquire(); # new InterruptedException() #end
        #valueCheck time() #  3 #end
    #end
#end
#tick
    #thread <t3>
        thread("t2").interrupt();
        #valueCheck time() #  3 #end
    #end
#end
#tick
    #thread <t1>
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 4 #end
    #end
#end
#end  

//(T38) Test interrupt waiting reader access with 1 waiting writer
#begin
#test C55
#tick
    #thread <t1>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread <t2>       
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() #  5 #end
    #end
#end
#tick
    #thread <t3>
        #excMonitor m.readLock().acquire(); # new InterruptedException() #end
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t4>
        thread("t3").interrupt();
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t1>
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 5 #end
    #end
    #thread <t2>
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#end 

//(T39) Test interrupt waiting writer access with 1 waiting reader
#begin
#test C56
#tick
    #thread <t1>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread <t2>
        #excMonitor m.writeLock().acquire(); # new InterruptedException() #end
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t3>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t4>
        thread("t2").interrupt();
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t1>
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 5 #end
    #end
    #thread <t3>
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#end 
 
//(T40) Test interrupt waiting writer access with 1 waiting writer
#begin
#test C58
#tick
    #thread <t1>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick
    #thread <t2>
        #excMonitor m.writeLock().acquire(); # new InterruptedException() #end
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t3>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() #  5 #end
    #end
#end
#tick
    #thread <t4>
        thread("t2").interrupt();
        #valueCheck time() #  4 #end
    #end
#end
#tick
    #thread <t1>
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 5 #end
    #end
#end
#tick
    #thread <t3>
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 6 #end
    #end
#end
#end  

// (T41) Test 3 readers waiting and 3 writers waiting (interrupt reader)
#begin
#test C59
#shared <s>

    ConanVector validTimes = new ConanVector();
    public void setup() {
        validTimes.add(9);
        validTimes.add(10);
        validTimes.add(11);
    }
#end
#tick   //1
    #thread <t61>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick   //2
    #thread <t62>
        #excMonitor m.readLock().acquire(); # new InterruptedException() #end
        #valueCheck time() # 8 #end
    #end
#end
#tick   //3
    #thread <t63>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # s.validTimes # CollectionRemove  #end
    #end
#end
#tick   //4
    #thread <t64>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # s.validTimes # CollectionRemove  #end
    #end
#end
#tick   //5
    #thread <t65>
        #excMonitor m.readLock().acquire(); #end
	    #valueCheck time() # 12 #end
	#end
#end
#tick    //6
    #thread <t66>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick   //7
    #thread <t67>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 12 #end
    #end
#end  
#tick    //8
    #thread <t68>
        thread("t62").interrupt();
        #valueCheck time() #  8 #end
    #end
#end
#tick    //9
    #thread <t61>
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 9 #end
    #end
#end
#tick    //10
    #thread 
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 10 #end
    #end
#end
#tick    //11
    #thread 
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 11 #end    
    #end                       
#end
#tick    //12
    #thread 
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 12 #end
    #end
#end
#tick    //13
    #thread 
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 13 #end
    #end   
    #thread 
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 13 #end
    #end
#end    
#end   
   
// (T42) Test 3 readers waiting and 3 writers waiting (interrupt writer)
#begin
#test C60
#shared <s>

    ConanVector validTimes = new ConanVector();
    public void setup() {
        validTimes.add(9);
        validTimes.add(10);
    }
#end
#tick 
    #thread <t71>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick 
    #thread <t72>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 11 #end
    #end
#end
#tick 
    #thread <t73>
        #excMonitor m.writeLock().acquire(); # new InterruptedException() #end
        #valueCheck time() # 8 #end
    #end
#end
#tick 
    #thread <t74>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # s.validTimes # CollectionRemove  #end
    #end
#end
#tick 
    #thread <t75>
        #excMonitor m.readLock().acquire(); #end
	    #valueCheck time() # 11 #end
	#end
#end
#tick 
    #thread <t76>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick 
    #thread <t77>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 11 #end
    #end
#end  
#tick
    #thread <t78>
        thread("t73").interrupt();
        #valueCheck time() #  8 #end
    #end
#end
#tick 
    #thread <t71>
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 9 #end
    #end
#end
#tick 
    #thread 
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 10 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 11 #end    
    #end                       
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 12 #end
    #end   
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 12 #end
    #end
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 12 #end
    #end
#end    
#end      

// (T43) Test 3 readers waiting and 3 writers waiting (interrupt reader)
#begin
#test C61
#shared <s>

    ConanVector validTimes = new ConanVector();
    public void setup() {
        validTimes.add(9);
        validTimes.add(10);
        validTimes.add(11);
    }
#end
#tick 
    #thread <t81>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick 
    #thread <t82>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # s.validTimes # CollectionRemove  #end
    #end
#end
#tick 
    #thread <t83>
        #excMonitor m.readLock().acquire(); # new InterruptedException() #end
        #valueCheck time() # 8 #end
    #end
#end
#tick 
    #thread <t84>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # s.validTimes # CollectionRemove  #end
    #end
#end
#tick 
    #thread <t85>
        #excMonitor m.readLock().acquire(); #end
	    #valueCheck time() # 12 #end
	#end
#end
#tick 
    #thread <t86>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end
#tick 
    #thread <t87>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 12 #end
    #end
#end  
#tick
    #thread <t88>
        thread("t83").interrupt();
        #valueCheck time() #  8 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 9 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 10 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 11 #end    
    #end                       
#end
#tick
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 12 #end
    #end
#end
#tick 
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 13 #end
    #end   
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 13 #end
    #end
#end    
#end      

// (T44) Test 3 readers waiting and 3 writers waiting (interrupt writer)
#begin
#test C62
#shared <s>

    ConanVector validTimes = new ConanVector();
    public void setup() {
        validTimes.add(9);
        validTimes.add(10);
    }
#end
#tick //1
    #thread <t91>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 1 #end
    #end
#end
#tick //2
    #thread <t92>
        #excMonitor m.writeLock().acquire(); # new InterruptedException() #end
        #valueCheck time() # 8  #end
    #end
#end
#tick //3
    #thread <t93>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 11 #end
    #end
#end
#tick //4
    #thread <t94>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # s.validTimes # CollectionRemove  #end
    #end
#end
#tick //5
    #thread <t95>
        #excMonitor m.readLock().acquire(); #end
	    #valueCheck time() # 11 #end
	#end
#end
#tick //6
    #thread <t96>
        #excMonitor m.writeLock().acquire(); #end
        #valueCheck time() # s.validTimes # CollectionRemove #end
    #end
#end 
#tick //7 
    #thread <t97>
        #excMonitor m.readLock().acquire(); #end
        #valueCheck time() # 11 #end
    #end
#end  
#tick //8
    #thread <t98>
        thread("t92").interrupt();
        #valueCheck time() #  8 #end
    #end
#end
#tick //9
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 9 #end
    #end
#end
#tick //10
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 10 #end
    #end
#end
#tick //11
    #thread
        #excMonitor m.writeLock().release(); #end
        #valueCheck time() # 11 #end    
    #end                       
#end
#tick //12
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 12 #end
    #end   
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 12 #end
    #end
    #thread
        #excMonitor m.readLock().release(); #end
        #valueCheck time() # 12 #end
    #end
#end    
#end      

// INTERRUPT PRIOR CALL

//ATTEMPT
//(T63) Test prior interrupt reader attempt
#begin
#test C31
#tick
    #thread <t1>
        interrupt();
        #excMonitor m.readLock().attempt(1000); # new InterruptedException() #end
        #valueCheck time() #  1 #end
    #end
#end
#end  

//(T64) Test prior interrupt reader attempt
#begin
#test C35
#tick
    #thread <t1>
        interrupt();
        #excMonitor m.writeLock().attempt(1000); # new InterruptedException() #end
        #valueCheck time() #  1 #end
    #end
#end
#end  

// ACQUIRE
//(T65) Test prior interrupt reader attempt
#begin
#test C33
#tick
    #thread <t1>
        interrupt();
        #excMonitor m.writeLock().acquire(); # new InterruptedException() #end
        #valueCheck time() #  1 #end
    #end
#end
#end  

//(T66) Test prior interrupt reader attempt
#begin
#test C37
#tick
    #thread <t1>
        interrupt();
        #excMonitor m.readLock().acquire(); # new InterruptedException() #end
        #valueCheck time() #  1 #end
    #end
#end
#end