#define NBUFS 2
#define READMAX 2
#define BUFSIZ 2*READMAX
#define EOF 255
#define TIMEOUT 254
#define FILEMAXLEN 20

byte	n[NBUFS];
byte ntotal[NBUFS];
byte putnext[NBUFS];
byte getnext[NBUFS];
bool eof[NBUFS];
bool roomwait[NBUFS];
bool datawait[NBUFS];
byte rwant;

/* use one big data array to simulate 2-d array */
#define bufstart(slot) (slot*BUFSIZ)
#define bufend(slot) ((slot+1)*BUFSIZ)
/* bit data[BUFSIZ*NBUFS]; */

bool selwait;
/* bool hastimeout; */

#define get 0
#define release 1

chan lock = [0] of { bit };
chan lockkill = [0] of { bit };
chan sel = [0] of { byte };
chan selcall = [0] of { byte };
chan selans = [0] of { byte, byte };
chan selkill = [0] of { bit };
chan readcall = [0] of { byte, byte };
chan readans = [0] of { byte };
chan readkill = [0] of { bit };
chan croom[NBUFS] = [0] of { bit };
chan cdata[NBUFS] = [0] of { bit };

proctype Lockrendez()
{
	do
	:: lock!get -> lock?release
	:: lockkill?release -> break
	od
}

proctype Copy(byte fd)
{
	byte num;
	bit b;

	do  :: 1 ->
		/* make sure there's room */
		lock?get;
		if
		:: (BUFSIZ-putnext[fd]) < READMAX ->
			if
			:: getnext[fd] == putnext[fd] ->
				getnext[fd] = 0;
				putnext[fd] = 0;
				lock!release
			:: getnext[fd] != putnext[fd] ->
				roomwait[fd] = 1;
				lock!release;
				croom[fd]?b
			fi
		:: (BUFSIZ-putnext[fd]) >= READMAX ->
			lock!release
		fi;
		/* simulate read into data buf at putnext */
		if
		:: ntotal[fd] > FILEMAXLEN ->
			num = EOF
		:: ntotal[fd] <= FILEMAXLEN ->
			if
			:: num = 1
			:: num = READMAX
			:: num = EOF
			fi
		fi;
		/* here is where data transfer would happen */
		lock?get;
		if
		:: num == EOF ->
			eof[fd] = 1;
/* printf("Copy %d got eof\n", fd);/**/
			if
			:: datawait[fd] ->
				datawait[fd] = 0;
				lock!release;
				cdata[fd]!1
			:: !datawait[fd] && (rwant & (1<<fd)) && selwait ->
				selwait = 0;
				lock!release;
				sel!fd
			:: !datawait[fd] && !((rwant & (1<<fd)) && selwait) ->
				lock!release
			fi;
			break
		:: num != EOF ->
/* printf("Copy %d putting %d in; old putnext=%d, old n=%d\n", fd, num, putnext[fd], n[fd]); /* */
			putnext[fd] = putnext[fd] + num;
			n[fd] = n[fd] + num;
			ntotal[fd] = ntotal[fd] + num;
			assert(n[fd] > 0);
			if
			:: datawait[fd] ->
				datawait[fd] = 0;
				lock!release;
				cdata[fd]!1
			:: !datawait[fd] && (rwant & (1<<fd)) && selwait ->
				selwait = 0;
				lock!release;
				sel!fd
			:: !datawait[fd] && !((rwant & (1<<fd)) && selwait) ->
				lock!release
			fi
		fi;
	od
}

proctype Read()
{
	byte ngot;
	byte fd;
	byte nwant;
	bit b;

    do
    :: readcall?fd,nwant ->
	if
	:: eof[fd] && n[fd] == 0 ->
		readans!EOF
	:: !(eof[fd] && n[fd] == 0) ->
		lock?get;
		ngot = putnext[fd] - getnext[fd];
/* printf("Reading %d, want %d: ngot = %d - %d, n = %d\n", fd, nwant, putnext[fd], getnext[fd], n[fd]); /* */
		if
		:: ngot == 0 ->
			if
			:: eof[fd] ->
				skip
			:: !eof[fd] ->
				/* sleep until there's data */
				datawait[fd] = 1;
/* printf("Read sleeping\n"); /* */
				lock!release;
				cdata[fd]?b;
				lock?get;
				ngot = putnext[fd] - getnext[fd];
/* printf("Read awoke, ngot = %d\n", ngot); /**/
			fi
		:: ngot != 0 -> skip
		fi;
		if
		:: ngot > nwant -> ngot = nwant
		:: ngot <= nwant -> skip
		fi;
		/* here would take ngot elements from data, from getnext[fd] ... */
		getnext[fd] = getnext[fd] + ngot;
		assert(n[fd] >= ngot);
		n[fd] = n[fd] - ngot;
		if
		:: ngot == 0 ->
			assert(eof[fd]);
			ngot = EOF
		:: ngot != 0 -> skip
		fi;
		if
		:: getnext[fd] == putnext[fd] && roomwait[fd] ->
			getnext[fd] = 0;
			putnext[fd] = 0;
			roomwait[fd] = 0;
			lock!release;
			croom[fd]!0
		:: getnext[fd] != putnext[fd] || !roomwait[fd] ->
			lock!release
		fi;
		readans!ngot
	fi
    :: readkill?b -> break
    od
}

proctype Select()
{
	byte num;
	byte i;
	byte fd;
	byte r;
	bit b;

    do
    :: selcall?r ->
/* printf("Select called, r=%d\n", r); /**/
	i = 0;
	do
	:: i < NBUFS ->
		if
		:: r & (1<<i) ->
			if
			:: eof[i] && n[i] == 0 ->
/* printf("Select got eof on %d\n", i);/**/
				num = EOF;
				r = i;
				goto donesel
			:: !eof[i] || n[i] != 0 -> skip
			fi
		:: !(r & (1<<i)) -> skip
		fi;
		i = i+1
	:: i >= NBUFS -> break
	od;
	num = 0;
	lock?get;
	rwant = 0;
	i = 0;
	do
	:: i < NBUFS ->
		if
		:: r & (1<<i) ->
			if
			:: n[i] > 0 || eof[i] ->
/* printf("Select found %d has n==%d\n", i, n[i]); /**/
				num = num+1
			:: n[i] == 0 && !eof[i] ->
/* printf("Select asks to wait for %d\n", i); /**/
				r = r &(~(1<<i));
				rwant = rwant | (1<<i)
			fi
		:: !(r & (1<<i)) -> skip
		fi;
		i = i+1
	:: i >= NBUFS -> break
	od;
	if
	:: num > 0 || rwant == 0 ->
		rwant = 0;
		lock!release;
	:: num == 0 && rwant != 0 ->
		selwait = 1;
		lock!release;
/* printf("Select sleeps\n"); /**/
		sel?fd;
/* printf("Select wakes up, fd=%d\n", fd); /**/
		if
		:: fd != TIMEOUT ->
			if
			:: (rwant & (1<<fd)) && (n[fd] > 0) ->
				r = r | (1<<fd);
				num = 1
			:: !(rwant & (1<<fd)) || (n[fd] == 0) ->
				num = 0
			fi
		:: fd == TIMEOUT -> skip
		fi;
		rwant = 0
	fi;
  donesel:
	selans!num,r
    :: selkill?b -> break
    od
}

/* This routine is written knowing NBUFS == 2 in several places */
proctype User()
{
	byte ndone;
	byte i;
	byte rw;
	byte num;
	byte nwant;
	byte fd;
	bool goteof[NBUFS];

	ndone = 0;
	do
	:: ndone == NBUFS -> break
	:: ndone < NBUFS ->
		if
		:: 1->
			/* maybe use Read */
/* printf("User trying to read.  Current goteofs: %d %d\n", goteof[0], goteof[1]); /**/
			/* randomly pick fd 0 or 1 from non-eof ones */
			if
			:: !goteof[0] -> fd = 0
			:: !goteof[1] -> fd = 1
			fi;
			if
			:: nwant = 1
			:: nwant = READMAX
			fi;
			readcall!fd,nwant;
			readans?num;
			if
			:: num == EOF ->
				goteof[fd] = 1;
				ndone = ndone + 1
			:: num != EOF -> assert(num != 0)
			fi
		:: 1->
/* printf("User trying to select.  Current goteofs: %d %d\n", goteof[0], goteof[1]); /**/
			/* maybe use Select, then Read */
			/* randomly set the "i want" bit for non-eof fds */
			if
			:: !goteof[0] && !goteof[1] -> rw = (1<<0) | (1<<1)
			:: !goteof[0] -> rw = (1<<0)
			:: !goteof[1] -> rw = (1<<1)
			fi;
			selcall!rw;
			selans?i,rw;
			if
			:: i == EOF ->
				goteof[rw] = 1;
				ndone = ndone + 1
			:: i != EOF ->
				/* this next statement knows NBUFS == 2 ! */
				if
				:: rw & (1<<0) -> fd = 0
				:: rw & (1<<1) -> fd = 1
				:: rw == 0 -> fd = EOF
				fi;
				if
				:: nwant = 1
				:: nwant = READMAX
				fi;
				if
				:: fd != EOF ->
					readcall!fd,nwant;
					readans?num;
					assert(num != 0)
				:: fd == EOF -> skip
				fi
			fi
		fi
	od;
	lockkill!release;
	selkill!release;
	readkill!release
}

init
{
	byte i;

	atomic {
		run Lockrendez();
		i = 0;
		do
		:: i < NBUFS ->
			run Copy(i);
			i = i+1
		:: i >= NBUFS -> break
		od;
		run Select();
		run Read();
		run User()
	}
}