#define N 10
#define K  5

mtype = {send,term,ack,termack};
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 && wert == (ackval+1) ->
		atomic {c12!send,wert; p1Sum = p1Sum + wert; wert = wert+1;}
	:: wert > K ->
		break;
	:: wert > N -> 
		break;
	:: c21?ack,ackval ->
		ackval = ackval;
	od;
	
	
	c12!term,0;
	
	do
	:: c21?termack,termackval ->
		termackval = termackval; break;
	od
}	

active proctype P2(){
	byte ein=0;
	byte ackval=0;
	byte termackval=0;
	
	do
	:: c12?send,ein ->
		c23!send,ein; p2Sum = p2Sum + ein; c21!ack,ein;
	:: c12?term,ein ->
		c23!term,ein;
	:: c32?ack,ackval ->
		ackval = ackval;
	:: c32?termack,termackval ->
		atomic {termackval = termackval; break;}
	od;
	
	
	c21!termack,ein; 
}

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

active proctype Invariante() {

assert(p1Sum < 55 && p2Sum < 55 && p3Sum < 55);
	
}