package rwvsn;
public class RWVSNDriver {
	static RWPrinter rwp;
	static IntWrapper iw;

	public static void main(String argv[]) {
		rwp = new RWPrinter();
		iw = new IntWrapper();

		for (int i = 0; i < 2; i++) {
			new Writer(rwp).start();
			new Reader(rwp).start();
		}
	}
}

class IntWrapper {
	public int x = 0;
}

final class Reader extends Thread {
	protected RWPrinter rwp;
	public Reader(RWPrinter r) {
		rwp = r;
	}
	public void run() {
		while (true)
			rwp.read();
	}
}

final class Writer extends Thread {
	protected RWPrinter rwp;
	public Writer(RWPrinter r) {
		rwp = r;
	}
	public void run() {
		while (true)
			rwp.write();
	}
}

class RWPrinter extends RWVSN {
	protected void doRead() {
		if (RWVSNDriver.iw.x < 10)
			RWVSNDriver.iw.x++;
	}
	protected void doWrite() {
		if (RWVSNDriver.iw.x > 0)
			RWVSNDriver.iw.x--;
	}
}

abstract class RWVSN {
	
	//@ invariant !(activeReaders > 0 && activeWriters > 0);
	//@ invariant !(activeWriters > 1);
	
	protected int activeReaders = 0;  // threads executing read
	protected int activeWriters = 0;  // always zero or one

	protected int waitingReaders = 0; // threads not yet in read
	protected int waitingWriters = 0; // same for write

	protected abstract void doRead(); // implement in subclasses
	protected abstract void doWrite(); 

	/**
	 * This method is not atomic. Furthermore, it's
	 * behavior can only be accurately expressed using
	 * temporal logics... something else to add to JML?
	 */
	public void read() /*throws InterruptedException*/ {
	  beforeRead(); 
	  try     { doRead(); }
	  finally { afterRead(); }
	}

	/**
	 * This method is not atomic. Furthermore, it's
	 * behavior can only be accurately expressed using
	 * temporal logics... something else to add to JML?
	 */
	public void write() /*throws InterruptedException*/ { 
	  beforeWrite(); 
	  try     { doWrite(); }
	  finally { afterWrite(); }
	}
	
	/*@ behavior
	   @   requires \lockset.has(this);
	   @   ensures \result <==> (waitingWriters == 0 && activeWriters == 0) &&
	   @                    \independent; 
	   @*/
	protected /*@ atomic pure @*/ boolean allowReader() {
	  return waitingWriters == 0 && activeWriters == 0;
	}

	/*@ behavior
	   @   requires \lockset.has(this);
	   @   ensures \result <==> (activeWriters == 0 && activeReaders == 0) &&
	   @                   \independent; 
	   @*/
	protected /*@ atomic pure @*/ boolean allowWriter() {
	  return activeReaders == 0 && activeWriters == 0;
	}


	/*@ behavior
	   @   when allowReader();
	   @    assignable waitingReaders, activeReaders;
	   @    ensures activeReaders >= 1 &&
	   @             \old(activeReaders) + 1 == activeReaders;
	   @*/
	protected /*@ atomic @*/ void beforeRead() 
	 /*throws InterruptedException*/ {
	 	synchronized(this) {
		  ++waitingReaders;
		  while (!allowReader()) {
			try { wait(); } 
			catch (InterruptedException ie) {
			  --waitingReaders; // roll back state 
	//		  throw ie;
			}
		  }
		  //@ commit:
		  --waitingReaders;
		  ++activeReaders;
	 	}
	}

	/*@ behavior
	   @    locks this;
	   @    assignable activeReaders;
	   @    ensures \old(activeReaders) - 1 == activeReaders;
	   @*/
	protected /*@ atomic @*/ void afterRead()  {
		synchronized(this) { 
		  --activeReaders;
		  notifyAll();
		}
	}

	/*@ behavior
	   @   requires allowWriter();
	   @   assignable waitingWriters, activeWriters;
	   @   ensures activeWriters == 1 &&
	   @          \old(activeWriters) + 1 == activeWriters;
	   @*/
	protected /*@ atomic @*/ void beforeWrite()
	 /*throws InterruptedException*/ {
		synchronized(this) {
		  ++waitingWriters;
		  while (!allowWriter()) {
			try { wait(); } 
			catch (InterruptedException ie) {
			  --waitingWriters;
	//		  throw ie;
			}
		  }
		  //@ commit:
		  --waitingWriters;
		  ++activeWriters;
		}
	}

	/*@ behavior
	   @    locks this;
	   @    assignable activeWriters;
	   @    ensures \old(activeWriters) - 1 == activeWriters;
	   @*/
	protected /*@ atomic @*/ void afterWrite() {
		synchronized(this) { 
		  --activeWriters;
		  notifyAll();
		}
	}
}