Messages

Processes multicast messages. Each message will have a content and a sender. Messages will also have a unique id, so that messages with the same content and sender can be distinguished. To model messages we introduce the type of message structures

If M MessageStruct, then its carrier |M| is the type of messages. The third component, which we write content $_{\mbox{\small {M}}}$ is a map from the messages |M|to their content |C|, which is the carrier of a decidable equivalence relation, cEQ $_{\mbox{\small {M}}}$, given by the second component of the message structure. This gives us a way to decide when the contents of two messages are ``the same''. The forth and fifth components, sender $_{\mbox{\small {M}}}$ and uid $_{\mbox{\small {M}}}$ are the operations that map messages to their sender and unique id. The two messages are equal if they have the same content, sender, and id, so we define