fmod CMESSAGE is

--- configuration level messages

including NATUTIL .
including PROC .
including MODE .
including CONF .

------------------------
--- message contents

sort Data .
op data : String -> Data .

var data : Data .

------------------------
--- messages
--- only data and conf change messages are delivered to the upper level
--- ack messages are used internally

sort Message .

--- regular message with data
op datamsg : Proc   --- sender
              Mode   --- mode of message
              Conf   --- configuration message was sent in
              Nat    --- sequence number (all sequence numbers are relative to the configuration)
              NatSet --- messages known to the sender of this message
              Data   --- contents 
           -> Message .

--- transitional configuration membership message
op transmsg : Conf
           -> Message .

--- regular configuration membership message
op confmsg : Conf 
              ProcSet   --- transitional set
           -> Message .

--- internal acknowledgement message (only used to ack safe messages)
op ackmsg :  Proc   --- sender
              Conf   --- configuration ack was sent in
              Nat    --- sequence number 
              Nat    --- sequence number of message being acknowledged
           -> Message .

--- note that membership refers to membership in processor configurations
--- and not to membership in groups (groups are not treated at this level)

var message message'  : Message .

------------------------

var src dest : Proc .
var mode : Mode .
var conf : Conf .
var ackedseq seq : Nat .
var transset : ProcSet .
var knownmsgs : NatSet .

op isdata : Message -> Bool .
eq isdata(datamsg(src,mode,conf,seq,knownmsgs,data)) = true .
eq isdata(ackmsg(src,conf,seq,ackedseq)) = false .
eq isdata(transmsg(conf)) = false .
eq isdata(confmsg(conf,transset)) = false .

op isack : Message -> Bool .
eq isack(datamsg(src,mode,conf,seq,knownmsgs,data)) = false .
eq isack(ackmsg(src,conf,seq,ackedseq)) = true .
eq isack(transmsg(conf)) = false .
eq isack(confmsg(conf,transset)) = false .

op src : Message -> Proc .
eq src(datamsg(src,mode,conf,seq,knownmsgs,data)) = src .
eq src(ackmsg(src,conf,seq,ackedseq)) = src .

op mode : Message -> Mode .
eq mode(datamsg(src,mode,conf,seq,knownmsgs,data)) = mode .

op conf : Message -> Conf .
eq conf(datamsg(src,mode,conf,seq,knownmsgs,data)) = conf .
eq conf(ackmsg(src,conf,seq,ackedseq)) = conf .

op seq : Message -> Nat .
eq seq(datamsg(src,mode,conf,seq,knownmsgs,data)) = seq .
eq seq(ackmsg(src,conf,seq,ackedseq)) = seq .

op knownmsgs : Message -> NatSet .
eq knownmsgs(datamsg(src,mode,conf,seq,knownmsgs,data)) = (sNatSet(seq) knownmsgs) .

op data : Message -> Data .
eq data(datamsg(src,mode,conf,seq,knownmsgs,data)) = data .

op ackedseq : Message -> Nat .
eq ackedseq(ackmsg(src,conf,seq,ackedseq)) = ackedseq .

-------------------------

sort MessageList .
op sMessageList : Message -> MessageList .
op eMessageList : -> MessageList .
op __ : MessageList MessageList -> MessageList [assoc id: eMessageList] .

var messagelist messagelist' : MessageList .

op contains : MessageList Message -> Bool .
eq contains(eMessageList, message') = false .
eq contains((sMessageList(message) messagelist), message') = 
     (message' == message) or contains(messagelist, message') .

op add : MessageList Message -> MessageList .
eq add(messagelist,message) = (messagelist sMessageList(message)) .

op  add' : MessageList Message -> MessageList .
ceq add'(messagelist,message) = messagelist 
    if contains(messagelist, message) .
ceq add'(messagelist,message) = (messagelist sMessageList(message)) 
    if not(contains(messagelist, message)) .

op  rm : MessageList Message -> MessageList .
eq  rm(eMessageList,message) = eMessageList .
ceq rm((sMessageList(message) messagelist),message') = rm(messagelist,message')
    if (message' == message) .
ceq rm((sMessageList(message) messagelist),message') = (sMessageList(message) rm(messagelist,message'))
    if (message' =/= message) .

op subset : MessageList MessageList -> Bool .
eq subset(eMessageList,messagelist') = true .
eq subset((sMessageList(message) messagelist), messagelist') = 
    contains(messagelist',message) and subset(messagelist,messagelist') .

-------------------------

sort MessageSet .
op sMessageSet : Message -> MessageSet .
op eMessageSet : -> MessageSet .
op __ : MessageSet MessageSet -> MessageSet [assoc comm id: eMessageSet] .

var messageset messageset' : MessageSet .

op contains : MessageSet Message -> Bool .
eq contains(eMessageSet, message') = false .
eq contains((sMessageSet(message) messageset), message') = 
     (message' == message) or contains(messageset, message') .

op add : MessageSet Message -> MessageSet .
eq add(messageset,message) = (messageset sMessageSet(message)) .

op  add' : MessageSet Message -> MessageSet .
ceq add'(messageset,message) = messageset 
    if contains(messageset, message) .
ceq add'(messageset,message) = (messageset sMessageSet(message)) 
    if not(contains(messageset, message)) .

op  rm : MessageSet Message -> MessageSet .
eq  rm(eMessageSet,message) = eMessageSet .
ceq rm((sMessageSet(message) messageset),message') = rm(messageset,message')
    if (message' == message) .
ceq rm((sMessageSet(message) messageset),message') = (sMessageSet(message) rm(messageset,message'))
    if (message' =/= message) .

op  rm : MessageSet MessageSet -> MessageSet .
eq  rm(messageset, eMessageSet) = messageset .
eq  rm(messageset, sMessageSet(message) messageset') = 
    rm(rm(messageset,message),messageset') .

op subset : MessageSet MessageSet -> Bool .
eq subset(eMessageSet,messageset') = true .
eq subset((sMessageSet(message) messageset), messageset') = 
    contains(messageset',message) and subset(messageset,messageset') .

op restrict : MessageSet Conf -> MessageSet .
eq restrict(eMessageSet,conf) = eMessageSet .
ceq restrict(sMessageSet(message) messageset,conf) =
    (sMessageSet(message) restrict(messageset,conf))
    if conf(message) == conf . 
ceq restrict(sMessageSet(message) messageset,conf) =
    restrict(messageset,conf)
    if conf(message) =/= conf . 

op restrict : MessageList Conf -> MessageList .
eq restrict(eMessageList,conf) = eMessageList .
ceq restrict(sMessageList(message) messagelist,conf) =
    (sMessageList(message) restrict(messagelist,conf))
    if conf(message) == conf . 
ceq restrict(sMessageList(message) messagelist,conf) =
    restrict(messagelist,conf)
    if conf(message) =/= conf . 

op acks : MessageSet Nat -> MessageSet .
eq acks(eMessageSet,seq) = eMessageSet .
ceq acks((sMessageSet(message) messageset), seq) =
    (sMessageSet(message) acks(messageset,seq))
    if isack(message) /\ ackedseq(message) == seq . 
ceq acks((sMessageSet(message) messageset), seq) =
    acks(messageset,seq)
    if isack(message) /\ ackedseq(message) =/= seq . 
ceq acks((sMessageSet(message) messageset), seq) =
    acks(messageset,seq)
    if not(isack(message)) . 

op srcs : MessageSet -> ProcSet .
eq srcs(eMessageSet) = eProcSet .
eq srcs(sMessageSet(message) messageset) =
   (sProcSet(src(message)) srcs(messageset)) . 
eq srcs(sMessageSet(message) messageset) =
   srcs(messageset) . 

op  seqs : MessageList -> NatSet .
eq  seqs(eMessageList) = eNatSet .
eq  seqs(sMessageList(message)) = sNatSet(seq(message))  .
ceq seqs(messagelist messagelist') =
    seqs(messagelist) seqs(messagelist')
    if messagelist =/= eMessageList and messagelist' =/= eMessageList .

op  knownmsgs : MessageList -> NatSet .
eq  knownmsgs(eMessageList) = eNatSet .
eq  knownmsgs(sMessageList(message)) = knownmsgs(message) .
ceq knownmsgs(messagelist messagelist') =
    knownmsgs(messagelist) knownmsgs(messagelist')
    if messagelist =/= eMessageList and messagelist' =/= eMessageList .

op  union : MessageSet MessageSet -> MessageSet .
eq  union(eMessageSet,messageset') = messageset' .
ceq union(sMessageSet(message) messageset, messageset') = 
    sMessageSet(message) union(messageset,messageset')
    if not(contains(messageset,message)) and not(contains(messageset',message)) .
ceq union(sMessageSet(message) messageset, messageset') = 
    union(messageset,messageset')
    if contains(messageset,message) or contains(messageset',message) .

op set : MessageList -> MessageSet .
eq set(eMessageList) = eMessageSet .
eq set(sMessageList(message) messagelist) = sMessageSet(message) set(messagelist) .

op data : MessageList -> MessageSet .
eq data(eMessageList) = eMessageSet .
ceq data(sMessageList(message) messagelist) = sMessageSet(message) data(messagelist) if isdata(message) .
ceq data(sMessageList(message) messagelist) = data(messagelist) if not(isdata(message)) .

---------------------------

sort Broadcast .

--- broadcast is a message to be sent to a set of processes

var broadcast broadcast' : Broadcast .

op broadcast : ProcSet Message -> Broadcast .  

sort BroadcastSet .
op sBroadcastSet : Broadcast -> BroadcastSet .
op eBroadcastSet : -> BroadcastSet .
op __ : BroadcastSet BroadcastSet -> BroadcastSet [assoc comm id: eBroadcastSet] .

var broadcastset broadcastset' : BroadcastSet .

op contains : BroadcastSet Broadcast -> Bool .
eq contains(eBroadcastSet, broadcast') = false .
eq contains((sBroadcastSet(broadcast) broadcastset), broadcast') = 
     (broadcast' == broadcast) or contains(broadcastset, broadcast') .

op add : BroadcastSet Broadcast -> BroadcastSet .
eq add(broadcastset,broadcast) = (broadcastset sBroadcastSet(broadcast)) .

op  add' : BroadcastSet Broadcast -> BroadcastSet .
ceq add'(broadcastset,broadcast) = broadcastset 
    if contains(broadcastset, broadcast) .
ceq add'(broadcastset,broadcast) = (broadcastset sBroadcastSet(broadcast)) 
    if not(contains(broadcastset, broadcast)) .

op  rm : BroadcastSet Broadcast -> BroadcastSet .
eq  rm(eBroadcastSet,broadcast) = eBroadcastSet .
ceq rm((sBroadcastSet(broadcast) broadcastset),broadcast') = rm(broadcastset,broadcast')
    if (broadcast' == broadcast) .
ceq rm((sBroadcastSet(broadcast) broadcastset),broadcast') = (sBroadcastSet(broadcast) rm(broadcastset,broadcast'))
    if (broadcast' =/= broadcast) .

op  rm : BroadcastSet BroadcastSet -> BroadcastSet .
eq  rm(broadcastset, eBroadcastSet) = broadcastset .
eq  rm(broadcastset, sBroadcastSet(broadcast) broadcastset') = 
    rm(rm(broadcastset,broadcast),broadcastset') .

endfm