#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) ->
		c12!send,wert; p1Sum = p1Sum + wert; wert = wert+1;
		// hier muss auf ack gewartet werden (gehoert zum Protokoll
                // und verhindert ihren Deadlock
		c21?ack,ackval; // Hier war quasi der Fehler!
	:: wert > K ->
		break;
	// in der folgende Zeile fehlte ein ::, wird aber nicht benoetigt,
	// da dies auch durch obigen Fall wert > K mit abgefangen wird
	// wert > N -> 
	//	break;
	//:: c21?ack,ackval ->
	//	ackval = ackval; // Hinweis, diese Zeile ohnehin unnoetig
	od;
	
	/* Warum wird dieser Code im Random-Mode nicht ausgeführt?! */
	c12!term,0;
	printf("Zeile durchlaufen\n");	
	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; atomic{ p2Sum = p2Sum + ein; c21!ack,ein;};
		// wie oben, Protocoll abschliessen
		c32?ack,ackval;
	:: c12?term,ein ->
		c23!term,ein;
		// naechste Zeile ergaenzt
		break
	//:: c32?ack,ackval ->
	//	ackval = ackval;
	:: c32?termack,termackval ->
		// termackval = termackval; Zeile ueberfluessig
		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() {
	// falsch: assert(p1Sum < 55 && p2Sum < 55 && p3Sum < 55);
	assert(p1Sum <= 55 && p2Sum <= 55 && p3Sum <= 55);
}