#define PROZESSE 3
#define MAX 10
#define GESAMT ((MAX*(MAX+1))/2)
#define PUFFER 2
mtype={send,rec}
chan toV = [PUFFER] of {mtype,byte,byte};
chan toP[PROZESSE]= [PUFFER] of {mtype,byte,byte};

proctype Teilnehmer(byte id){
  byte i=1;
  int summe=0;
  byte wert;
  do
  :: atomic{
       i<=MAX && nfull(toV) ; /* 1 */
       toV!send,id,i;
       i=i+1
     }
  :: summe<GESAMT*(PROZESSE-1) 
             && toP[id]?[rec,_,_] ->
     toP[id]?rec,_,wert;
     summe=summe+wert
  :: i==MAX+1 && summe==GESAMT *(PROZESSE-1) ->
      break
  od;
}

proctype Verteiler(){
  byte name;
  byte wert;
  byte emp;
  do
  :: toV?send,name,wert ->
       emp=0;
       do
       :: emp<PROZESSE && emp!=name ->
          toP[emp]!rec, name, wert;
          emp=emp+1
       :: emp==name -> emp=emp+1
       :: emp==PROZESSE -> break
       od;
  od;
}   

init{
  atomic{
    byte i=0;
    do
    :: i<PROZESSE -> 
       run Teilnehmer(i);
       i=i+1
    :: else -> break
    od;
    run Verteiler()
  };
}

