int writers_count = 0;
int writers_waiting = 0;
int readers_count = 0;
int readers_waiting = 0;

int readers_active = 0;	/* used for assertions */
int writers_active = 0; /* used for assertions */

int readers_active_total = 0;
int writers_active_total = 0;

proctype writer()
{
	do
	::  do
		::	atomic {
				if 
				::	writers_count == 0 -> writers_count = 1;
					break;
				fi;
			}
		od;

		assert writers_active == 0;

		do
		::	readers_waiting < readers_count -> 
			writers_waiting = 1;
			/* yield */
			writers_waiting = 0;
		::	readers_waiting == readers_count ->
			break;
		od;
		
		writers_active = 1;
		writers_active_total++;
		assert readers_active == 0;
		writers_active = 0;
		writers_count = 0;
	od;
}

proctype reader()
{
	do
	::	atomic { readers_count++; };

		do
		::	writers_waiting < writers_count -> 
			atomic { readers_waiting++; }
			/* yield */
			atomic { readers_waiting--; }
		::	writers_waiting == writers_count ->
			break;
		od;

		atomic { readers_active++; readers_active_total++; }
		assert writers_active == 0;
		atomic { readers_active--; }
		atomic { readers_count--; }
	od;
}

init
{
	run reader();
	run writer();
}