--- Formal Specification of Spread
---
--- Authors: Mark-Oliver Stehr (UIUC), Carolyn Talcott (SRI)
---  	     Sebastian Gutierrez-Nolasco (UCI)
--- Date: July, 2004
---
--- References: 
---
---   Yair Amir: Replication Using Group Communication Over a Partitioned 
---   Network, Ph.D. thesis, Hebrew University of Jerusalem, 1995. 
---
---   Louise E. Moser, Yair Amir, P. Michael Melliar-Smith and Deborah 
---   A. Agarwal: Extended Virtual Synchrony, 14th IEEE International 
---   Conference on Distributed Computing Systems (ICDCS), pages 56-65, 
---   June 1994
---
---   John Schultz: Partitionable Virtual Synchrony Using Extended Virtual
---   Synchrony, Masters Thesis, Johns Hopkins University, 2001. 
---
---   Yair Amir and Jonathan Stanton: The Spread Wide Area Group Communication 
---   System, Technical Report CNDS-98-4.  
---
---   Yair Amir and Jonathan Stanton: A Users Guide to Spread. October 21, 2002.
---
---   Spread Souce Code. Version 2.17.2rc3. Available at www.spread.org.
---
---   Personal Communication with Yair Amir and John Schultz. 2003/2004.
---
---
--- Notes:
--- - This specification uses a simplified mapping of agents to processes.
---   We assume that for each agent there is a running process with the same 
---   name, because a client should not rely on the knowledge that they are
---   using the same spread daemon.
--- - Join: The source code contains a more complex treatment of join, which 
---   seems to involve delivering trans messages under certain conditions. 
---   It remains unclear why this is needed.
--- - Group Messages: Group messages only need to be delivered to the affected 
---   groups, i.e. some optimizations are possible here which have been omitted
---   in this spec.
--- - The definitions of causal order delivery in Schultz' thesis is different 
---   from the one in Amir's thesis. We included specifications for both, but
---   we note that self-delivery can be violated with Amir's condition, more
---   precisely, if Amir's condition is generalized to include reliable and
---   fifo messages.
--- - With Schultz' condition there is still an issue with the description in 
---   messages. the User Manual, saying that fifo messages may need to wait 
---   for reliable 
--- - The actual implementation allows multicast to subgroups and multi group
---   multicasting, features that we omitted in the present specification, but 
---   it would be easy to add them. We do, however, provide a notion of private 
---   groups, which is needed for Secure Spread.
---   


mod SPREAD is

protecting BOOL .
protecting NAT .
protecting STRING .
protecting CSPREAD .
protecting AGENT .
protecting GROUP .
protecting VIEW .
protecting GMESSAGE .
protecting GAPI .


-----------------------
var memb : Agent .
var sender : Agent .
var agent agent' : Agent .
var agentlist : AgentList .
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 .
var gdata : GData .
var gmessage : GMessage .
var gmessagelist gmessagelist' gmessagelist'' : GMessageList .
var groupagentslist groupagentslist' : GroupAgentsList .
------------------------


var agentset agentset' : AgentSet .

op agentset : ProcSet ~> AgentSet .
eq agentset(eProcSet) = eAgentSet .
eq agentset(sProcSet(agent) procset) = sAgentSet(agent) agentset(procset) .


--- group layer local state

op gclients : AgentList -> State . 	--- all connected clients
op gjoined : Proc GroupList -> State . 	--- the groups the process has joined
op gview : Proc ViewSet -> State . 	--- the views the process has installed
op glocalconf : Proc Conf -> State . 	--- the configuration the process is in
op gdelivered : Proc GMessageList -> State .  --- client-side mailbox
					      --- (accessed using sp-receive)


--- each process is in one of the following states 
--- (wheater connected to a client or not)
op goperational : Proc -> State . 	      --- goperational mode 
op gtrans : Proc ProcSet -> State . 	      --- transitional mode
op ggather : Proc ProcSet ProcSet -> State .  --- groups message gathering mode
op ggather' : Proc ProcSet ProcSet GMessageList -> State .


--- for better type safety we could introduce a new sort of states for
--- each of these for constructors
var goperational gtrans ggather ggather' : State .

op gstate : State State State State -> State .

op contains : State Proc ~> Bool .
eq contains(eState,proc') = false .
eq contains(goperational(proc) goperational, proc') = 
   if proc == proc' then true 
   else contains(goperational,proc') fi .
eq contains(gtrans(proc,transprocs) gtrans, proc') = 
   if proc == proc' then true 
   else contains(gtrans,proc') fi .
eq contains(ggather(proc,transprocs,procset) ggather, proc') = 
   if proc == proc' then true 
   else contains(ggather,proc') fi .
eq contains(ggather'(proc, transprocs, procset, gmessagelist) ggather', proc') =
   if proc == proc' then true 
   else contains(ggather',proc') fi .
 
op rm : State Proc ~> State . 		      --- presently not used
eq rm(eState,proc') = eState .
eq rm(goperational(proc) goperational, proc') = 
   if proc == proc' then rm(goperational,proc') 
   else goperational(proc) rm(goperational,proc') fi .
eq rm(gtrans(proc,transprocs) gtrans, proc') = 
   if proc == proc' then rm(gtrans,proc') 
   else gtrans(proc,transprocs) rm(gtrans,proc') fi .
eq rm(ggather(proc,transprocs,procset) ggather, proc') = 
   if proc == proc' then rm(ggather,proc') 
   else ggather(proc,transprocs,procset) rm(ggather,proc') fi .
eq rm(ggather'(proc, transprocs, procset, gmessagelist) ggather', proc') = 
   if proc == proc' then rm(ggather',proc') 
   else ggather'(proc, transprocs, procset, gmessagelist) rm(ggather',proc') fi .


-----------------------
--- sp-connect
-----------------------

--- It is not necessary to change the goperational state or generate
--- process variables upon connect/disconnect, because we assume that
--- all processes of the group layer are always active even if they do
--- not have a connected client. This is needed because we collect
--- groups messages from each process, and a process needs to answer
--- even if not connected to a client.

crl gclients(clientlist)
    gjoined(proc, grouplist)
    gdelivered(proc,gmessagelist)
    sp-connect-req(proc) 
    =>
    gclients(add(clientlist,proc))
    gjoined(proc, eGroupList)
    gdelivered(proc,eGMessageList)
    sp-connect-ack(proc) 
    if not(contains(clientlist, proc)) .

crl gclients(clientlist)
    sp-connect-req(proc) 
    =>
    gclients(clientlist)
    sp-connect-err(proc,AgentNotUnique)
    if contains(clientlist, proc) .


-----------------------
--- sp-disconenct
-----------------------

op sp-disconnect         --- client has requested to disconnect from spread server
    : Agent              --- client
   -> State .

crl gclients(clientlist)
    sp-disconnect-req(proc) 
    ENABLED(DISCONNECT(proc)) 
    =>
    gclients(clientlist)
    sp-disconnect(proc) 
    multicast-req(proc, agreed, gdisconnectmsg(proc,nogroup,noview))
    PERFORMED(DISCONNECT(proc))
    if contains(clientlist, proc) .

rl  gclients(clientlist)
    gjoined(proc,grouplist)
    gdelivered(proc,gmessagelist)
    sp-disconnect(proc) 
    multicast-ack(proc) 
    =>
    gclients(rm(clientlist,proc))
    gjoined(proc,eGroupList)
    gdelivered(proc,eGMessageList)
    sp-disconnect-ack(proc) .

crl gclients(clientlist)
    sp-disconnect-req(proc) 
    =>
    gclients(clientlist)
    sp-disconnect-err(proc,IllegalAgent)
    if not(contains(clientlist, proc)) .


-----------------------
--- sp-join
-----------------------

op sp-join          	 --- client has requested to join a group
    : Agent              --- client
      Group              --- group to join
   -> State .

crl gclients(clientlist)
    sp-join-req(proc,group)
    ENABLED(JOIN(proc,group)) 
    =>
    gclients(clientlist)
    sp-join(proc,group)
    multicast-req(proc, agreed, gjoinmsg(proc,group,noview))
    PERFORMED(JOIN(proc,group))
    if contains(clientlist, proc) .

rl  sp-join(proc,group)
    multicast-ack(proc) 
    =>
    sp-join-ack(proc) .

crl gclients(clientlist)
    sp-join-req(proc,group) 
    =>
    gclients(clientlist)
    sp-join-err(proc,IllegalAgent)
    if not(contains(clientlist, proc)) .


-----------------------
--- sp-leave
-----------------------

op sp-leave         	 --- client has requested to leave a group
    : Agent              --- client
      Group              --- group to leave
   -> State .

crl gclients(clientlist)
    sp-leave-req(proc,group)
    ENABLED(LEAVE(proc,group)) 
    =>
    gclients(clientlist)
    sp-leave(proc,group)
    multicast-req(proc, agreed, gleavemsg(proc,group,noview))
    PERFORMED(LEAVE(proc,group)) 
    if contains(clientlist, proc) .

rl  sp-leave(proc,group)
    multicast-ack(proc) 
    =>
    sp-leave-ack(proc) .

crl gclients(clientlist)
    sp-leave-req(proc,group) 
    =>
    gclients(clientlist)
    sp-leave-err(proc,IllegalAgent)
    if not(contains(clientlist, proc)) .


-----------------------
--- sp-multicast
-----------------------

op sp-multicast     	 --- client has requested multicast to a group
    : Agent              --- client
      Mode               --- message type
      Group              --- destination
      GData	         --- contents
   -> State .

var mode : Mode .

crl gclients(clientlist)
    sp-multicast-req(proc,mode,group,gdata) 
    ENABLED(MULTICAST(proc,group)) 
    =>
    gclients(clientlist)
    sp-multicast(proc,mode,group,gdata)
    multicast-req(proc,mode,gdatamsg(proc,group,gdata)) 
    PERFORMED(MULTICAST(proc,group))
    if contains(clientlist,proc) .

rl  sp-multicast(proc,mode,group,gdata)
    multicast-ack(proc) 
    =>
    sp-multicast-ack(proc) .

crl gclients(clientlist)
    sp-multicast-req(proc,mode,group,gdata) 
    =>
    gclients(clientlist)
    sp-multicast-err(proc,IllegalAgent)
    if not(contains(clientlist, proc)) .


-----------------------
--- sp-receive
-----------------------

crl gclients(clientlist)
    gdelivered(proc, (sGMessageList(gmessage) gmessagelist))
    sp-receive-req(proc) 
    =>
    gclients(clientlist)
    gdelivered(proc, gmessagelist)
    sp-receive-ack(proc, gmessage)
    if contains(clientlist, proc) .

crl gclients(clientlist)
    sp-receive-req(proc) 
    =>
    gclients(clientlist)
    sp-receive-err(proc,IllegalAgent)
    if not(contains(clientlist, proc)) .


-----------------------
var message : Message .
var messagelist : MessageList .
var proc proc' proc'' : Proc .
var conf conf' conf'' newconf : Conf .
var seq : Nat .
var knownmsgs : NatSet .


--- processing data messages 
--- in operational, transitional, and gather state

crl gstate(goperational, gtrans, ggather, ggather')
    gjoined(proc,grouplist)
    delivered(proc, (sMessageList(message) messagelist))
    gdelivered(proc, gmessagelist') 
    =>
    gstate(goperational, gtrans, ggather, ggather')
    gjoined(proc,grouplist)
    delivered(proc, messagelist)
    gdelivered(proc, (gmessagelist' sGMessageList(gmessage)))
    if contains(goperational gtrans ggather', proc) /\
       datamsg(proc',mode,conf,seq,knownmsgs,gmessage) := message /\
       isgdata(gmessage) /\
       (contains(grouplist,group(gmessage)) or group(gmessage) == 
       privategroup(proc)) .

crl gstate(goperational, gtrans, ggather, ggather')
    gjoined(proc,grouplist)
    delivered(proc, (sMessageList(message) messagelist)) 
    =>
    gstate(goperational, gtrans, ggather, ggather')
    gjoined(proc,grouplist)
    delivered(proc, messagelist)
    if contains(goperational gtrans ggather', proc) /\
       datamsg(proc',mode,conf,seq,knownmsgs,gmessage) := message /\
       isgdata(gmessage) /\
       not(contains(grouplist,group(gmessage)) or group(gmessage) == 
       privategroup(proc)) .


--- We dont need the following anymore because mailbox is emptied 
--- when (dis)connecting.

--- Possibly discard data messages for disconnected clients.
--- crl gclients(clientlist)
---     delivered(proc, (sMessageList(message) messagelist)) =>
---     gclients(clientlist)
---     delivered(proc, messagelist)
---    if datamsg(proc',mode,conf,seq,knownmsgs,gmessage) := message /\
---       isgdata(gmessage) /\
---       not(contains(clientlist,proc)) 


--- aux functions for the following rules
--- (only used for join, leave, and disconnect messages with sender == client)

op  update : Proc GroupList GMessage ~> GroupList .
eq  update(proc,grouplist,gjoinmsg(sender,group,view)) =
    if sender == proc then add'(grouplist,group) else grouplist fi .
eq  update(proc,grouplist,gleavemsg(sender,group,view)) =
    if sender == proc then rm(grouplist,group) else grouplist fi .
eq  update(proc,grouplist,gdisconnectmsg(sender,group,view)) =
    if sender == proc then eGroupList else grouplist fi .

op  update : Proc Conf ViewSet GMessage ~> ViewSet .
ceq update(proc,conf,viewset,gjoinmsg(sender,group,noview)) =
    update(viewset,group,add(get(viewset,group),sender))
    if contains(viewset,group) .
ceq update(proc,conf,viewset,gjoinmsg(sender,group,noview)) =
    update(viewset,group,view(conf,group,sAgentList(sender),0)) --- conf used here
    if not(contains(viewset,group)) .
ceq update(proc,conf,viewset,gleavemsg(sender,group,noview)) =
    update(viewset,group,rm(get(viewset,group),sender))
    if contains(viewset,group) .
ceq update(proc,conf,viewset,gleavemsg(sender,group,noview)) =
    viewset
    if not(contains(viewset,group)) .
eq  update(proc,conf,viewset,gdisconnectmsg(sender,nogroup,noview)) =
    rm(viewset,sender) .


--- The following functions translates a view change message
--- without a view into a corresponding view change message
--- for each group equipped the the new view.

op  mkGMessages : Proc GroupList ViewSet GMessage ~> GMessageList .
eq  mkGMessages(proc,eGroupList,viewset',gmessage) = eGMessageList .
ceq mkGMessages(proc,sGroupList(group) grouplist',viewset',gmessage) = 
    sGMessageList(gjoinmsg(sender,group,get(viewset',group)))
    mkGMessages(proc,grouplist',viewset',gmessage)
    if gjoinmsg(sender,group,noview) := gmessage .
ceq mkGMessages(proc,sGroupList(group) grouplist',viewset',gmessage) = 
    mkGMessages(proc,grouplist',viewset',gmessage)
    if gjoinmsg(sender,group',noview) := gmessage /\ group' =/= group .
ceq mkGMessages(proc,sGroupList(group) grouplist',viewset',gmessage) = 
    sGMessageList(gleavemsg(sender,group,get(viewset',group)))
    mkGMessages(proc,grouplist',viewset',gmessage)
    if gleavemsg(sender,group,noview) := gmessage .
ceq mkGMessages(proc,sGroupList(group) grouplist',viewset',gmessage) = 
    mkGMessages(proc,grouplist',viewset',gmessage)
    if gleavemsg(sender,group',noview) := gmessage /\ group' =/= group .
ceq mkGMessages(proc,sGroupList(group) grouplist',viewset',gmessage) = 
    sGMessageList(gdisconnectmsg(sender,group,get(viewset',group)))
    mkGMessages(proc,grouplist',viewset',gmessage)
    if gdisconnectmsg(sender,nogroup,noview) := gmessage .


--- handle ordinary join, leave, disconnect
--- in operational, transitional, and gather state

crl gstate(goperational, gtrans, ggather, ggather')
    gjoined(proc,grouplist)
    gview(proc,viewset)
    glocalconf(proc,conf)
    delivered(proc, (sMessageList(message) messagelist))
    gdelivered(proc, gmessagelist') 
    =>
    gstate(goperational, gtrans, ggather, ggather')
    gjoined(proc,grouplist')
    gview(proc,viewset')
    glocalconf(proc,conf)
    delivered(proc, messagelist)
    gdelivered(proc, (gmessagelist' gmessagelist''))
    if contains(goperational gtrans ggather', proc) /\
       isdata(message) /\ gmessage := data(message) /\ 
       (isgjoin(gmessage) or 
        (isgleave(gmessage) and sender(gmessage) =/= proc) or 
        (isgdisconnect(gmessage) and sender(gmessage) =/= proc)) /\
       grouplist' := update(proc,grouplist,gmessage) /\
       viewset' := update(proc,conf,viewset,gmessage) /\
       gmessagelist'' := mkGMessages(proc,grouplist',viewset',gmessage) .


--- the following is not needed, because disconnected clients
--- can drop messages anyway (see earlier rule)

--- crl delivered(proc, (sMessageList(message) messagelist)) =>
---       delivered(proc, messagelist)
---       if isdata(message) /\ gmessage := data(message) /\
---          (isgdisconnect(gmessage) and sender(gmessage) == proc) 


--- special handling for self leave
--- in operational, transitional, and gather state

crl gstate(goperational, gtrans, ggather, ggather')
    gjoined(proc,grouplist)
    gview(proc,viewset)
    glocalconf(proc,conf)
    delivered(proc, (sMessageList(message) messagelist))
    gdelivered(proc, gmessagelist') 
    =>
    gstate(goperational, gtrans, ggather, ggather')
    gjoined(proc,grouplist')
    gview(proc,viewset')
    glocalconf(proc,conf)
    delivered(proc, messagelist)
    gdelivered(proc, (gmessagelist' gmessagelist''))
    if contains(goperational gtrans ggather', proc) /\
       isdata(message) /\ gmessage := data(message) /\ 
       (isgleave(gmessage) and sender(gmessage) == proc) /\
       grouplist' := update(proc,grouplist,gmessage) /\
       viewset' := update(proc,conf,viewset,gmessage) /\
       gmessagelist'' := sGMessageList(gselfleavemsg(sender(gmessage),group(gmessage))) .


--- handle transitional message
--- only for operational state here

op  gtransmsg : GroupList -> GMessageList .
eq  gtransmsg(eGroupList) = eGMessageList .
eq  gtransmsg(sGroupList(group) grouplist) = 
      sGMessageList(gtransmsg(group)) gtransmsg(grouplist) .

crl gstate(goperational(proc) goperational, gtrans, ggather, ggather')
    gjoined(proc,grouplist)
    glocalconf(proc,conf)
    delivered(proc, (sMessageList(message) messagelist))
    gdelivered(proc, gmessagelist') 
    =>
    gstate(goperational, gtrans(proc,members(conf)) gtrans, ggather, ggather')
    gjoined(proc,grouplist)
    glocalconf(proc,newconf)
    delivered(proc, messagelist) 
    gdelivered(proc, (gmessagelist' gtransmsg(grouplist)))
    if transmsg(newconf) := message .


--- the above could be optimized by sending gtransmsg only to groups
--- that are actually affected by the configuration change

var procset transprocs transprocs' : ProcSet .
var transagents transagents' : AgentSet .

op  mkGroupAgentsList : Proc GroupList -> GroupAgentsList .
eq  mkGroupAgentsList(proc,eGroupList) = eGroupAgentsList .
eq  mkGroupAgentsList(proc,sGroupList(group) grouplist) = 
    sGroupAgentsList(groupagents(group,sAgentList(proc)))
    mkGroupAgentsList(proc,grouplist) .


--- handle configuration change
--- only for transitional state here
--- broadcast groups message with all views

crl ENABLED(SENDGROUPMSG(proc))
    gstate(goperational, gtrans(proc,transprocs) gtrans, ggather, ggather')
    gjoined(proc,grouplist)
    glocalconf(proc,conf)
    delivered(proc, (sMessageList(message) messagelist)) 
    =>
    PERFORMED(SENDGROUPMSG(proc))
    gjoined(proc,grouplist)
    glocalconf(proc,newconf)
    delivered(proc, messagelist) 
    multicast-req(proc,agreed,ggroupmsg(proc,mkGroupAgentsList(proc,grouplist)))
    gstate(goperational, gtrans, ggather(proc,inter(transprocs,transprocs'),members(newconf)) ggather, ggather')
    if confmsg(newconf,transprocs') := message  .


--- handle configuration change messages without previous
--- transitional messages (can happen upon recovery)
--- only for operational state here

crl ENABLED(SENDGROUPMSG(proc))
    gstate(goperational(proc) goperational, gtrans, ggather, ggather')
    gjoined(proc,grouplist)
    glocalconf(proc,conf)
    delivered(proc, (sMessageList(message) messagelist)) 
    =>
    PERFORMED(SENDGROUPMSG(proc))
    gjoined(proc,grouplist)
    glocalconf(proc,newconf)
    delivered(proc, messagelist) 
    multicast-req(proc,agreed,ggroupmsg(proc,mkGroupAgentsList(proc,grouplist)))
    gstate(goperational, gtrans, ggather(proc,transprocs',members(newconf)) ggather, ggather')
    if confmsg(newconf,transprocs') := message .

rl  gstate(goperational, gtrans, ggather(proc,transprocs,procset) ggather, ggather')
    multicast-ack(proc) 
    =>
    gstate(goperational, gtrans, ggather, ggather'(proc,transprocs,procset,eGMessageList) ggather') .


--- gather all groups messages, i.e. one from each configuration member process

crl gstate(goperational, gtrans, ggather, ggather'(proc, transprocs, sProcSet(proc') procset, gmessagelist) ggather')
    delivered(proc, (sMessageList(message) messagelist)) 
    =>
    gstate(goperational, gtrans, ggather, ggather'(proc, transprocs, procset, gmessagelist sGMessageList(gmessage)) ggather')
    delivered(proc, messagelist) 
    if datamsg(proc'',mode,conf,seq,knownmsgs,gmessage) := message /\
       ggroupmsg(proc',groupagentslist') := gmessage .


--- the following rules deal with the case of transitional and
--- configuration change messages arriving before the groups messages
--- (in contrast to the rules for goperational state we take exisiting
--- transprocs into account)

crl gstate(goperational, gtrans, ggather, ggather'(proc,transprocs, sProcSet(proc') procset, gmessagelist) ggather')
    glocalconf(proc,conf)
    delivered(proc, (sMessageList(message) messagelist)) 
    =>
    gstate(goperational, gtrans(proc,transprocs) gtrans, ggather, ggather')
    delivered(proc, messagelist)
    glocalconf(proc,newconf)
    if transmsg(newconf) := message .

crl ENABLED(SENDGROUPMSG(proc))
    gstate(goperational, gtrans, ggather, ggather'(proc,transprocs, sProcSet(proc') procset, gmessagelist) ggather')
    gjoined(proc,grouplist)
    glocalconf(proc,conf)
    delivered(proc, (sMessageList(message) messagelist)) 
    =>
    PERFORMED(SENDGROUPMSG(proc))
    gjoined(proc,grouplist)
    glocalconf(proc,newconf)
    delivered(proc, messagelist) 
    multicast-req(proc,agreed,ggroupmsg(proc,mkGroupAgentsList(proc,grouplist)))
    gstate(goperational, gtrans, ggather(proc,inter(transprocs,transprocs'),members(newconf)) ggather, ggather')
    if confmsg(newconf,transprocs') := message .


--- aux functions for the following rules

--- the new viewset is computed from the union of the groups info
op  union : GroupList GroupAgentsList -> GroupAgentsList .
eq  union(eGroupList,groupagentslist) = eGroupAgentsList .
eq  union((sGroupList(group) grouplist),groupagentslist) = 
    sGroupAgentsList(groupagents(group,agents(group,groupagentslist))) 
    union(grouplist,groupagentslist) .

op  union : GroupList GMessageList -> GroupAgentsList .
eq  union(grouplist,gmessagelist) = union(grouplist,flatten(gmessagelist)) .


--- generate new viewset from the gathered groups info
op  mkViewSet : Conf GroupAgentsList Nat -> ViewSet .
eq  mkViewSet(conf, eGroupAgentsList, index) = eViewSet .
eq  mkViewSet(conf, sGroupAgentsList(groupagents(group,agentlist)) groupagentslist, index) =
    sViewSet(view(conf, group, agentlist, index))
    mkViewSet(conf, groupagentslist, index) . 


--- generate view change messages
op  mkConfGMessage : Group ViewSet AgentSet -> GMessage .
ceq mkConfGMessage(group,viewset,transagents) = 
    gconfmsg(group,view,inter(transagents,agentset(members(view)))) 
    if view := get(viewset,group) .

op  mkConfGMessages : GroupList ViewSet AgentSet -> GMessageList .
eq  mkConfGMessages(eGroupList,viewset,transagents) = eGMessageList .
eq  mkConfGMessages(sGroupList(group) grouplist,viewset,transagents) =
    sGMessageList(mkConfGMessage(group,viewset,transagents))
    mkConfGMessages(grouplist,viewset,transagents) .


--- find out which groups have changed from one view to another
op  groupchanged : Group ViewSet ViewSet -> Bool .
eq  groupchanged(group,viewset,viewset') = 
    members(get(viewset,group)) =/= members(get(viewset',group)) .

op  groupschanged : GroupList ViewSet ViewSet -> GroupList .
eq  groupschanged(eGroupList, viewset, viewset') = eGroupList .
ceq groupschanged(sGroupList(group) grouplist, viewset, viewset') = 
    sGroupList(group) groupschanged(grouplist,viewset,viewset')
    if groupchanged(group,viewset,viewset') .
ceq groupschanged(sGroupList(group) grouplist, viewset, viewset') = 
    groupschanged(grouplist,viewset,viewset')
    if not(groupchanged(group,viewset,viewset')) .

var groupschanged : GroupList .


--- process groups messages, update local viewset, and generate conf change messages

crl glocalconf(proc,conf)
    gjoined(proc,grouplist)
    gdelivered(proc, gmessagelist') 
    gstate(goperational, gtrans, ggather, ggather'(proc,transprocs,eProcSet,gmessagelist) ggather')
    gview(proc,viewset) 
    =>
    glocalconf(proc,conf)
    gjoined(proc,grouplist)
    gdelivered(proc, gmessagelist' mkConfGMessages(groupschanged,viewset',agentset(transprocs))) 
    gstate(goperational(proc) goperational, gtrans, ggather, ggather')
    gview(proc,viewset') 
    if grouplist' := rmdoubles(groups(gmessagelist)) /\
       viewset' := mkViewSet(conf,union(grouplist',gmessagelist),0) /\
       groupschanged := groupschanged(grouplist,viewset,viewset') .

endm