Untitled

From Whipped Duck, 12 Years ago, written in Plain Text, viewed 6 times.
URL https://paste.blessuren.de/view/d8fe32f6 Embed
Download Paste or View Raw
  1. #define N 10
  2. #define K  5
  3. mtype = {send,term,ack,termack};
  4. chan c12 = [0] of {mtype,byte};
  5. chan c23 = [0] of {mtype,byte};
  6. chan c32 = [0] of {mtype,byte};
  7. chan c21 = [0] of {mtype,byte};
  8. byte p1Sum = 0;
  9. byte p2Sum = 0;
  10. byte p3Sum = 0;
  11. active proctype P1(){
  12.         byte termackval=0;
  13.         byte ackval=0;
  14.         byte wert=1;
  15.         byte antwort;
  16.         do
  17.         :: wert<=N && wert == (ackval+1) ->
  18.                 c12!send,wert; p1Sum = p1Sum + wert; wert = wert+1;
  19.                 // hier muss auf ack gewartet werden (gehoert zum Protokoll
  20.                 // und verhindert ihren Deadlock
  21.                 c21?ack,ackval; // Hier war quasi der Fehler!
  22.         :: wert > K ->
  23.                 break;
  24.         // in der folgende Zeile fehlte ein ::, wird aber nicht benoetigt,
  25.         // da dies auch durch obigen Fall wert > K mit abgefangen wird
  26.         // wert > N ->
  27.         //      break;
  28.         //:: c21?ack,ackval ->
  29.         //      ackval = ackval; // Hinweis, diese Zeile ohnehin unnoetig
  30.         od;
  31.        
  32.         /* Warum wird dieser Code im Random-Mode nicht ausgeführt?! */
  33.         c12!term,0;
  34.         printf("Zeile durchlaufen\n"); 
  35.         do
  36.         :: c21?termack,termackval ->
  37.                 termackval = termackval; break;
  38.         od
  39. }      
  40. active proctype P2(){
  41.         byte ein=0;
  42.         byte ackval=0;
  43.         byte termackval=0;
  44.        
  45.         do
  46.         :: c12?send,ein ->
  47.                 c23!send,ein; atomic{ p2Sum = p2Sum + ein; c21!ack,ein;};
  48.                 // wie oben, Protocoll abschliessen
  49.                 c32?ack,ackval;
  50.         :: c12?term,ein ->
  51.                 c23!term,ein;
  52.                 // naechste Zeile ergaenzt
  53.                 break
  54.         //:: c32?ack,ackval ->
  55.         //      ackval = ackval;
  56.         :: c32?termack,termackval ->
  57.                 // termackval = termackval; Zeile ueberfluessig
  58.                 break;
  59.         od;
  60.        
  61.        
  62.         c21!termack,ein;
  63. }
  64. active proctype P3(){
  65.         byte ein=0;
  66.         do
  67.         :: c23?send,ein ->
  68.                 atomic {p3Sum = p3Sum + ein; c32!ack,ein;}
  69.         :: c23?term,ein ->
  70.                 c32!termack,ein; break;
  71.         od;
  72. }
  73. active proctype Invariante() {
  74.         // falsch: assert(p1Sum < 55 && p2Sum < 55 && p3Sum < 55);
  75.         assert(p1Sum <= 55 && p2Sum <= 55 && p3Sum <= 55);
  76. }
  77.  
  78.  
  79.  

Reply to "Untitled"

Here you can reply to the paste above