#define N 4			/* liczba zwykłych stacji + 1 (Master) */
#define ENQ N			/* zapytanie od stacji Master */
#define INVALID_ID 7            /* niepoprawny identyfikator adresata */

/* stacje zwykłe i ich sekretarze mają identyfikator 1..N-1,
   a Master ma identyfikator 0 */

/* wszelka komunikacja jest synchroniczna (zerowa pojemność kanałów) */

/* format pakietu w sieci: nadawca, adresat, dane */
chan to_medium = [0] of {byte, byte, byte};
chan from_medium[N] = [0] of {byte, byte, byte}; /* rozgłaszanie */

/* sekretarz przekazuje otrzymane dane swojej stacji */
chan out[N] = [0] of {byte};	/* powinno być N-1, ale składnia nie pozwala */

/* sekretarz odbiera od swojej stacji adresata i dane do wysłania */
chan in[N] = [0] of {byte, byte}; /* j.w. */

active proctype master()
{
        byte sender;
        byte receiver;
        byte data;
        byte next;
        next=1;
        to_medium!0,next,ENQ;      
        do
        :: from_medium[0]?sender,receiver,data
        :: timeout -> next=next%(N-1)+1;to_medium!0,next,ENQ
        od
}

active proctype medium()
{
        byte sender;
        byte receiver;
        byte data;
        byte i;
        do
        :: to_medium?sender,receiver,data ->
           i=0;
           if
           :: (1) -> do
                     :: i<=N-1 ->
                           if
                           :: i==sender -> skip
                           :: i!=sender -> from_medium[i]!sender,receiver,data
                           fi;
                           i=i+1
                     :: i>N-1 -> break
                     od
           :: to_medium?sender,receiver,data -> goto accept_collision
           fi
        od;
accept_collision: do
                  :: (1) -> skip
                  od               
}

proctype slave(byte id)
{
        byte sender;
        byte receiver;
        byte data;
        byte ny_receiver;
        byte ny_data;
        do
        :: from_medium[id]?sender,receiver,data ->
           if
           :: data!=ENQ ->
                 if
                 :: receiver==id -> out[id]!data
                 :: receiver!=id -> skip
                 fi
           :: data==ENQ && receiver==id ->
                 in[id]?ny_receiver,ny_data;
                 to_medium!id,ny_receiver,ny_data
           :: data==ENQ && receiver!=id -> skip
           fi
        :: from_medium[id]?sender,receiver,data          /* gubienie pakietu */
        od
}

proctype user(byte id; chan cin,cout)
{
        byte data;
	byte succ = id%(N-1)+1;	/* następnik */
        do
        :: cout?data ->
           if
           :: data!=id -> goto accept_wrong_data
           :: data==id -> skip
           fi
        :: cin!INVALID_ID,0     /* nie zainteresowany */
        :: cin!succ,succ	/* adresat = treść (dla weryfikacji) */
        od;
accept_wrong_data:
        do
        :: (1) -> skip                          
        od
}

init {
	byte proc;
	atomic {
		proc = 1;
		do
		:: proc < N ->
			run slave (proc);
			run user(proc, in[proc], out[proc]);
			proc++
		:: proc >= N ->
			break
		od
	}
}