/* What does the following code do? More precisely, what */
/* is the relationship between the contents of the array 'str' */
/* and the value 'result' upon termination? */

#define	MAX		6
#define MAXINDEX 	MAX-1

bool result; 
byte str[MAX]; 

proctype producer( chan out )
{	int i;
	do 
	:: (i <= MAXINDEX) -> out!str[i]; i++;
	:: (i > MAXINDEX) -> break;
	od;
} 

proctype mystery( chan in; chan out )
{	bit x,y;
	bool r;
	chan child = [1] of { bit };
	chan c = [1] of { bool };

	out!1;
	if 
	:: in?x -> out!1;
		   run mystery( child, c );
		   do
		   :: in?y -> child!y; c?r; out!(r && (x==y));
		   :: timeout -> break; 
		   od 
	:: timeout -> skip
	fi
}

proctype consumer ( chan in )
{ 	bool r;
	int i=0;
	do
	:: (i <= MAX) -> in?r; i++;
	:: (i > MAX) -> break;
	od;
	result = r;
}
	
init 
{ 	
	/* initialize the array str here */
	str[0] = 1;
	str[1] = 1;
	str[2] = 0;
	str[3] = 0;
	str[4] = 1;
	str[5] = 0;

	chan child = [1] of { bit };
	chan c = [1] of { bool };

	run producer(child);
	run mystery(child, c);
	run consumer(c);
}