// -----------------------------------------------------------------------
// The following module implements a lossy channel. Each time the input
// event "receive_message" holds, the channel receives a new message with
// tag "in_tag". The inputs "duplicate" and "loose" instruct the
// lossy channel to duplicate the message that is currently sent or to
// loose that message. Since the Channel may receive more messages than
// it can send, it will have to store messages. As we only deal with
// message tags, it is sufficient to model the storage of the channel by
// holding the "min_tag" and "max_tag", respectively.
// -----------------------------------------------------------------------

module Channel(
   event ?receive_message,	// holds if channel receives a new message
   int   ?in_tag,		// the content of receive message (only tag)
   event ?duplicate,		// instructs to (erroneously) duplicate a message
   event ?loose,		// instructs to (erroneously) send a message !=min_message
   int   min_tag,	// minimal message in buffer
         max_tag,	// maximal message in buffer
   event !send_message,	// indicates that a message is sent
   int   !out_tag)	// the sent message (between min_message and max_message)
{
  nat tag;
  event error;
   loop{
      if(receive_message) 
	 next(max_tag) = max_tag + 1;
      if(in_tag != (max_tag+1))
	 emit(error);

      // -------------------------------------------------------------
      // send a message that is contained in the buffer; since the
      // channel is faulty, it might duplicate and loose messages
      // -------------------------------------------------------------
      if(min_tag < max_tag)
         if(loose)
            next(min_tag) = (min_tag + 1);
         else {
            emit(send_message);
            out_tag = min_tag;
	    if(not(duplicate))
               next(tag) = min_tag +1;
         }
      pause;
   }
}