fmod GMESSAGE is

protecting BOOL .
protecting NAT .
protecting STRING .
protecting AGENT .
protecting GROUP .
protecting VIEW .
protecting CMESSAGE .

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

var client : Agent .
var proc : Proc .
var memb : Agent .
var sender : Agent .
var agent agent' : Agent .
var agentlist : AgentList .
var agentset : AgentSet .
var memblist translist : AgentList .
var clientlist : AgentList .
var group group' : Group .
var grouplist grouplist' : GroupList .
var view view' : View .
var viewset viewset' : ViewSet .
var index : Nat .

--------------------
--- contents of regular gmessages 

sort GData .  
op gdata : String -> GData .

var gdata : GData .

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

sort GroupAgents .

op groupagents : Group AgentList -> GroupAgents .

var groupagents groupagents' : GroupAgents .

------------------------
--- the following is needed for groups messages

sort GroupAgentsList .
op eGroupAgentsList : -> GroupAgentsList .
op sGroupAgentsList : GroupAgents -> GroupAgentsList .
op __ : GroupAgentsList GroupAgentsList -> GroupAgentsList [assoc id: eGroupAgentsList] .

var groupagentslist groupagentslist' : GroupAgentsList .

op  groups : GroupAgentsList -> GroupList .
eq  groups(eGroupAgentsList) = eGroupList .
eq  groups(sGroupAgentsList(groupagents(group,agentlist)) groupagentslist) = 
    sGroupList(group) groups(groupagentslist) .

op  agents : Group GroupAgentsList -> AgentList .
eq  agents(group,eGroupAgentsList) = eAgentList .
ceq agents(group,sGroupAgentsList(groupagents(group',agentlist)) groupagentslist) = 
    agentlist agents(group,groupagentslist) if group == group' .
ceq agents(group,sGroupAgentsList(groupagents(group',agentlist)) groupagentslist) = 
    agents(group,groupagentslist) if not(group == group') .

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

sort GMessage .

var gmessage gmessage' : GMessage .

subsort GMessage < Data . --- group messages become configuration level data

--- messages visible to the upper layer

op gdatamsg       --- regular message
    : Agent       --- sender
      Group       --- all receivers
      GData   --- contents
   -> GMessage .

op gtransmsg      --- transitional view message
    : Group       --- affected group
   -> GMessage .

op gjoinmsg       --- regular view message caused by join
    : Agent       --- joining agent
      Group       --- affected group
      View        --- new view
   -> GMessage .

op gleavemsg      --- regular view message caused by leave
    : Agent       --- joining agent
      Group       --- affected group
      View        --- new view
   -> GMessage .

op gdisconnectmsg --- regular view message caused by disconnect
    : Agent       --- disconnecting agent
      Group       --- affected group
      View        --- new view
   -> GMessage .

op gconfmsg    --- regular view message caused by network
    : Group       --- affected group
      View        --- new view
      AgentSet    --- transitional set of agents 
   -> GMessage .  --- (i.e. agents that came with client into the new view)

op gselfleavemsg --- selfleave message
    : Agent
      Group       --- affected group
   -> GMessage .

--- internal messages (not visible to the upper layer)

op ggroupmsg    --- internal groups message (used to bring views in sync after network changes)
    : Proc
      GroupAgentsList
   -> GMessage .

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

op isgdata : GMessage -> Bool .
eq isgdata(gdatamsg(agent,group,gdata)) = true .
eq isgdata(gtransmsg(group)) = false .
eq isgdata(gjoinmsg(agent,group,view)) = false .
eq isgdata(gleavemsg(agent,group,view)) = false .
eq isgdata(gdisconnectmsg(agent,group,view)) = false .
eq isgdata(gconfmsg(group,view,agentset)) = false .
eq isgdata(gselfleavemsg(agent,group)) = false .

op isgjoin : GMessage -> Bool .
eq isgjoin(gdatamsg(agent,group,gdata)) = false .
eq isgjoin(gtransmsg(group)) = false .
eq isgjoin(gjoinmsg(agent,group,view)) = true .
eq isgjoin(gleavemsg(agent,group,view)) = false .
eq isgjoin(gdisconnectmsg(agent,group,view)) = false .
eq isgjoin(gconfmsg(group,view,agentset)) = false .
eq isgjoin(gselfleavemsg(agent,group)) = false .
eq isgjoin(ggroupmsg(proc,groupagentslist)) = false .

op isgleave : GMessage -> Bool .
eq isgleave(gdatamsg(agent,group,gdata)) = false .
eq isgleave(gtransmsg(group)) = false .
eq isgleave(gjoinmsg(agent,group,view)) = false .
eq isgleave(gleavemsg(agent,group,view)) = true .
eq isgleave(gdisconnectmsg(agent,group,view)) = false .
eq isgleave(gconfmsg(group,view,agentset)) = false .
eq isgleave(gselfleavemsg(agent,group)) = false .
eq isgleave(ggroupmsg(proc,groupagentslist)) = false .

op isgdisconnect : GMessage -> Bool .
eq isgdisconnect(gdatamsg(agent,group,gdata)) = false .
eq isgdisconnect(gtransmsg(group)) = false .
eq isgdisconnect(gjoinmsg(agent,group,view)) = false .
eq isgdisconnect(gleavemsg(agent,group,view)) = false .
eq isgdisconnect(gdisconnectmsg(agent,group,view)) = true .
eq isgdisconnect(gconfmsg(group,view,agentset)) = false .
eq isgdisconnect(gselfleavemsg(agent,group)) = false .
eq isgdisconnect(ggroupmsg(proc,groupagentslist)) = false .

op isgconf : GMessage -> Bool .
eq isgconf(gdatamsg(agent,group,gdata)) = false .
eq isgconf(gtransmsg(group)) = false .
eq isgconf(gjoinmsg(agent,group,view)) = false .
eq isgconf(gleavemsg(agent,group,view)) = false .
eq isgconf(gdisconnectmsg(agent,group,view)) = false .
eq isgconf(gconfmsg(group,view,agentset)) = true .
eq isgconf(gselfleavemsg(agent,group)) = false .
eq isgconf(ggroupmsg(proc,groupagentslist)) = false .

op isgtrans : GMessage -> Bool .
eq isgtrans(gdatamsg(agent,group,gdata)) = false .
eq isgtrans(gtransmsg(group)) = true .
eq isgtrans(gjoinmsg(agent,group,view)) = false .
eq isgtrans(gleavemsg(agent,group,view)) = false .
eq isgtrans(gdisconnectmsg(agent,group,view)) = false .
eq isgtrans(gconfmsg(group,view,agentset)) = false .
eq isgtrans(gselfleavemsg(agent,group)) = false .
eq isgtrans(ggroupmsg(proc,groupagentslist)) = false .

op isgselfleave : GMessage -> Bool .
eq isgselfleave(gdatamsg(agent,group,gdata)) = false .
eq isgselfleave(gtransmsg(group)) = false .
eq isgselfleave(gjoinmsg(agent,group,view)) = false .
eq isgselfleave(gleavemsg(agent,group,view)) = false .
eq isgselfleave(gdisconnectmsg(agent,group,view)) = false .
eq isgselfleave(gconfmsg(group,view,agentset)) = false .
eq isgselfleave(gselfleavemsg(agent,group)) = true .
eq isgselfleave(ggroupmsg(proc,groupagentslist)) = false .

op group : GMessage ~> Group .
eq group(gdatamsg(agent,group,gdata)) = group .
eq group(gtransmsg(group)) = group .
eq group(gjoinmsg(agent,group,view)) = group .
eq group(gleavemsg(agent,group,view)) = group .
eq group(gdisconnectmsg(agent,group,view)) = group .
eq group(gconfmsg(group,view,agentset)) = group .
eq group(gselfleavemsg(agent,group)) = group .

op sender : GMessage ~> Agent .
eq sender(gdatamsg(agent,group,gdata)) = agent .
eq sender(gjoinmsg(agent,group,view)) = agent .
eq sender(gleavemsg(agent,group,view)) = agent .
eq sender(gdisconnectmsg(agent,group,view)) = agent .

op data : GMessage ~> GData .
eq data(gdatamsg(agent,group,gdata)) = gdata .

op view : GMessage ~> View .
eq view(gjoinmsg(agent,group,view)) = view .
eq view(gleavemsg(agent,group,view)) = view .
eq view(gdisconnectmsg(agent,group,view)) = view .
eq view(gconfmsg(group,view,agentset)) = view .

op transset : GMessage ~> AgentSet .
eq transset(gconfmsg(group,view,agentset)) = agentset .

op isggroup : GMessage -> Bool .
eq isggroup(gdatamsg(agent,group,gdata)) = false .
eq isggroup(gtransmsg(group)) = false .
eq isggroup(gjoinmsg(agent,group,view)) = false .
eq isggroup(gleavemsg(agent,group,view)) = false .
eq isggroup(gdisconnectmsg(agent,group,view)) = false .
eq isggroup(gconfmsg(group,view,agentset)) = false .
eq isggroup(gselfleavemsg(agent,group)) = false .
eq isggroup(ggroupmsg(proc,groupagentslist)) = true .

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

sort GMessageList .
op eGMessageList : -> GMessageList .
op sGMessageList : GMessage -> GMessageList .
op __ : GMessageList GMessageList -> GMessageList 
        [assoc id: eGMessageList] .

var gmessagelist gmessagelist' gmessagelist'' : GMessageList .

op  rm : GMessageList GMessage -> GMessageList .
eq  rm(eGMessageList,gmessage) = eGMessageList .
ceq rm((sGMessageList(gmessage) gmessagelist),gmessage') = rm(gmessagelist,gmessage')
    if (gmessage' == gmessage) .
ceq rm((sGMessageList(gmessage) gmessagelist),gmessage') = (sGMessageList(gmessage) rm(gmessagelist,gmessage'))
    if (gmessage' =/= gmessage) .

--- the following two function are only used for lists
--- of group messages

op  flatten : GMessageList ~> GroupAgentsList .
eq  flatten(eGMessageList) = eGroupAgentsList .
eq  flatten(sGMessageList(ggroupmsg(proc,groupagentslist)) gmessagelist) = 
    groupagentslist flatten(gmessagelist) .

op  groups : GMessageList ~> GroupList .
eq  groups(gmessagelist) = groups(flatten(gmessagelist)) .

endfm