blessuren pastebin

Untitled

From Gray Madrill, 12 Years ago, written in Plain Text, viewed 3 times.
URL https://paste.blessuren.de/view/1c6ba432 Embed
Download Paste or View Raw
  1. #define N 10
  2. #define K  5
  3.  
  4. mtype = {send,term,ack,termack};
  5. chan c12 = [0] of {mtype,byte};
  6. chan c23 = [0] of {mtype,byte};
  7. chan c32 = [0] of {mtype,byte};
  8. chan c21 = [0] of {mtype,byte};
  9.  
  10. byte p1Sum = 0;
  11. byte p2Sum = 0;
  12. byte p3Sum = 0;
  13.  
  14. active proctype P1(){
  15.         byte termackval=0;
  16.         byte ackval=0;
  17.         byte wert=1;
  18.         byte antwort;
  19.         do
  20.         :: wert<=N && wert == (ackval+1) ->
  21.                 atomic {c12!send,wert; p1Sum = p1Sum + wert; wert = wert+1;}
  22.         :: wert > K ->
  23.                 break;
  24.         :: wert > N ->
  25.                 break;
  26.         :: c21?ack,ackval ->
  27.                 ackval = ackval;
  28.         od;
  29.        
  30.        
  31.         c12!term,0;
  32.        
  33.         do
  34.         :: c21?termack,termackval ->
  35.                 termackval = termackval; break;
  36.         od
  37. }      
  38.  
  39. active proctype P2(){
  40.         byte ein=0;
  41.         byte ackval=0;
  42.         byte termackval=0;
  43.        
  44.         do
  45.         :: c12?send,ein ->
  46.                 c23!send,ein; p2Sum = p2Sum + ein; c21!ack,ein;
  47.         :: c12?term,ein ->
  48.                 c23!term,ein;
  49.         :: c32?ack,ackval ->
  50.                 ackval = ackval;
  51.         :: c32?termack,termackval ->
  52.                 atomic {termackval = termackval; break;}
  53.         od;
  54.        
  55.        
  56.         c21!termack,ein;
  57. }
  58.  
  59. active proctype P3(){
  60.         byte ein=0;
  61.         do
  62.         :: c23?send,ein ->
  63.                 atomic {p3Sum = p3Sum + ein; c32!ack,ein;}
  64.         :: c23?term,ein ->
  65.                 c32!termack,ein; break;
  66.         od;
  67. }
  68.  
  69. active proctype Invariante() {
  70.  
  71. assert(p1Sum < 55 && p2Sum < 55 && p3Sum < 55);
  72.        
  73. }
  74.  

Reply to "Untitled"

Here you can reply to the paste above

Powered by Stikked