#define N 10
#define K  5

mtype = {send,term,ack,termack,repeat,termrepeat};
chan c12 = [0] of {mtype,byte}; 
chan c23 = [0] of {mtype,byte}; 
chan c32 = [0] of {mtype,byte}; 
chan c21 = [0] of {mtype,byte}; 

byte p1Sum = 0;
byte p2Sum = 0;
byte p3Sum = 0;

active proctype P1(){
	byte termackval=0;
	byte ackval=0;
	byte wert=1;
	byte antwort;
	
	do
	:: wert<=N -> atomic{c12!send,wert; p1Sum = p1Sum + wert; wert = wert+1;}
		if
		/* auf ack warten */
		::c21?ack,ackval -> printf("ack von P2 erhalten")
		/* ist nicht angekommen */
    		::c21?repeat,wert -> c12!send,wert;	
		fi
	:: wert > K -> break;
	od;
	
	c12!term,0;
	
	do
	:: c21?termrepeat,wert -> c12!term,0;
	:: c21?termack,termackval -> break;
	od
}	

active proctype P2(){
	byte ein=0;
	byte ackval=0;
	byte termackval=0;
	do
	:: c12?send,ein -> atomic {p2Sum = p2Sum + ein; c21!ack,ein};c23!send,ein;
	    		if
	               	:: c32?ack,ackval -> printf("ack von P3 erhalten")
			:: c32?repeat,ein -> c23!send,ein;
			fi
	:: c12?send,ein -> c21!repeat,ein; skip
	:: c12?term,ein -> atomic {c21!termack,ein; c23!term,ein;} 
			if
			:: c32?termack,termackval -> break;
			:: c32?termrepeat,ein -> c23!term,ein;
			fi		   
	:: c12?term,ein -> c21!termrepeat,ein;
	od;
}

active proctype P3(){
	byte ein=0;
	do
	:: c23?send,ein ->
		atomic {p3Sum = p3Sum + ein; c32!ack,ein;}
	:: c23?send,ein -> 
		c32!repeat,ein;
	:: c23?term,ein ->
		atomic {c32!termack,ein; break;}
	:: c23?term,ein ->
		c32!termrepeat,ein; skip
	od;
}

active proctype Invariante() {
	assert(p1Sum <= 55 && p2Sum <= 55 && p3Sum <= 55);
}