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 */

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

		assert writers_active == 0;

		do
		::	readers_waiting == readers_count ->
			break;
		od;
		
		writers_active = 1;
		assert readers_active == 0;
		writers_active = 0;
		writers_count = 0;
	od;
}

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

		if
		::	writers_count > 0 -> 
			atomic { readers_waiting++; }
			do
			::	writers_count == 0 ->
				break;
			od;
			atomic { readers_waiting--; }
		fi;

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

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