// ----------------------------------------------------------------------- // 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; } }