- #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);
- }