--- Formal Specification of Flush Spread
--- A layer providing Virtual Synchrony on Top of Spread
--- 
--- Authors: Mark-Oliver Stehr (UIUC), Carolyn Talcott (SRI)
--- Date: March 30, 2004
---
--- References:
---
---   John Schultz: Partitionable Virtual Synchrony Using Extended Virtual Synchrony, 
---     Masters Thesis, Masters Thesis, Johns Hopkins University, 2001. 
---
---   Spread Souce Code. Version 2.17.2rc3. Available at www.spread.org.
---
---   Personal Communication with Yair Amir and John Schultz. 2003/2004.
---
--- Notes:
---
--- Different from the Flush Spread implementation in C our specification
--- - does not have a special treatment for vulnerable messages
---   (leading to an optimization of message size for other messages)
--- - does not have the extra FLUSH_RECV messages after FLUSH_OK 
--- - does not drop unprocessed membership changes if they become 
---   too old (FLOK_AGE_LIMIT in the implementation)

--- It remains unclear where trans messages are delivered.  In this
--- specification they are delivered always and only before a network
--- conf change, but the flush spread documentation (see FL_receive)
--- seems to suggest that they can/must also be delivered when
--- voluntarily joining/leaving a group (actually this is more an
--- issue of the underlying spread layer, assuming that the semantics
--- regarding trans messages is the same).

mod FLUSHSPREAD is

protecting BOOL .
protecting NAT .
protecting STRING .
protecting SPREAD .
protecting FMESSAGE .
protecting FAPI .

var error : Error .
var client agent : Agent .
var agentset : AgentSet .
var agentlist : AgentList .
var group group' : Group .
var view view' : View .
var gdata : GData .
var fdata : FData .
var message : FMessage .
var gmessage : GMessage .
var gmessagelist : GMessageList .
var viewset viewset' viewset'' viewset''' : ViewSet .
var grouplist : GroupList .
var transset : AgentSet .
var groupset groupset' : GroupSet .
var fmessage : FMessage .
var fmessagelist fmessagelist' : FMessageList .

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

op isfreq : GMessage -> Bool .
eq isfreq(gmessage) = isgdata(gmessage) and isfreq(data(gmessage)) .

op  isfok : GMessage -> Bool .
ceq isfok(gmessage) = isfok(data(gmessage)) if isgdata(gmessage) .
ceq isfok(gmessage) = false if not(isgdata(gmessage)) .

op isfdata : GMessage -> Bool .
eq isfdata(gmessage) = isgdata(gmessage) and isfdata(data(gmessage)) .

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

op conv : GMessage -> FMessage .
eq conv(gdatamsg(agent,group,gdata)) = gdata .
eq conv(gtransmsg(group)) = ftransmsg(group) .
eq conv(gjoinmsg(agent,group,view)) = fjoinmsg(agent,group,view) .
eq conv(gleavemsg(agent,group,view)) = fleavemsg(agent,group,view) .
eq conv(gdisconnectmsg(agent,group,view)) = fdisconnectmsg(agent,group,view) .
eq conv(gconfmsg(group,view,agentset)) = fconfmsg(group,view,agentset) .
eq conv(gselfleavemsg(agent,group)) = fselfleavemsg(agent,group) .

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

sort GroupOp .

op joining : Agent Group -> GroupOp .
op leaving : Agent Group -> GroupOp .
op disconnecting : Agent Group -> GroupOp .
op changing : Group -> GroupOp .

var groupop groupop' : GroupOp .

op group : GroupOp ~> Group .
eq group(joining(agent,group)) = group .
eq group(leaving(agent,group)) = group .
eq group(disconnecting(agent,group)) = group .
eq group(changing(group)) = group .

op joining : GroupOp ~> Bool .
eq joining(joining(agent,group)) = true .
eq joining(leaving(agent,group)) = false .
eq joining(disconnecting(agent,group)) = false .
eq joining(changing(group)) = false .

op leaving : GroupOp ~> Bool .
eq leaving(joining(agent,group)) = false .
eq leaving(leaving(agent,group)) = true .
eq leaving(disconnecting(agent,group)) = false .
eq leaving(changing(group)) = false .

op changing : GroupOp ~> Bool .
eq changing(joining(agent,group)) = false .
eq changing(leaving(agent,group)) = false .
eq changing(disconnecting(agent,group)) = false .
eq changing(changing(group)) = true .

op disconnecting : GroupOp ~> Bool .
eq disconnecting(joining(agent,group)) = false .
eq disconnecting(leaving(agent,group)) = false .
eq disconnecting(disconnecting(agent,group)) = true .
eq disconnecting(changing(group)) = false .

op sender : GroupOp ~> Agent .
eq sender(joining(agent,group)) = agent .
eq sender(leaving(agent,group)) = agent .
eq sender(disconnecting(agent,group)) = agent .

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

sort GroupOpSet .
op eGroupOpSet : -> GroupOpSet .
op sGroupOpSet : GroupOp -> GroupOpSet .
op __ : GroupOpSet GroupOpSet -> GroupOpSet [assoc comm id: eGroupOpSet] .

var groupopset groupopset' : GroupOpSet .

op contains : GroupOpSet GroupOp -> Bool .
eq contains(eGroupOpSet, groupop') = false .
eq contains((sGroupOpSet(groupop) groupopset), groupop') = 
     (groupop' == groupop) or contains(groupopset, groupop') .

op contains : GroupOpSet Group -> Bool .
eq contains(eGroupOpSet, group') = false .
eq contains((sGroupOpSet(groupop) groupopset), group') = 
     (group(groupop) == group') or contains(groupopset, group') .

op joining : GroupOpSet Group -> Bool .
eq joining(eGroupOpSet, group') = false .
eq joining((sGroupOpSet(groupop) groupopset), group') = 
     (joining(groupop) and group(groupop) == group') or joining(groupopset, group') .

op leaving : GroupOpSet Group -> Bool .
eq leaving(eGroupOpSet, group') = false .
eq leaving((sGroupOpSet(groupop) groupopset), group') = 
     (leaving(groupop) and group(groupop) == group') or leaving(groupopset, group') .

op disconnecting : GroupOpSet Group -> Bool .
eq disconnecting(eGroupOpSet, group') = false .
eq disconnecting((sGroupOpSet(groupop) groupopset), group') = 
     (disconnecting(groupop) and group(groupop) == group') or disconnecting(groupopset, group') .

op changing : GroupOpSet Group -> Bool .
eq changing(eGroupOpSet, group') = false .
eq changing((sGroupOpSet(groupop) groupopset), group') = 
     (changing(groupop) and group(groupop) == group') or changing(groupopset, group') .

op add : GroupOpSet GroupOp -> GroupOpSet .
eq add(groupopset,groupop) = (groupopset sGroupOpSet(groupop)) .

op  add' : GroupOpSet GroupOp -> GroupOpSet .
ceq add'(groupopset,groupop) = groupopset 
    if contains(groupopset, groupop) .
ceq add'(groupopset,groupop) = (groupopset sGroupOpSet(groupop)) 
    if not(contains(groupopset, groupop)) .

op  rm : GroupOpSet GroupOp -> GroupOpSet .
eq  rm(eGroupOpSet,groupop) = eGroupOpSet .
ceq rm((sGroupOpSet(groupop) groupopset),groupop') = rm(groupopset,groupop')
    if (groupop' == groupop) .
ceq rm((sGroupOpSet(groupop) groupopset),groupop') = (sGroupOpSet(groupop) rm(groupopset,groupop'))
    if (groupop' =/= groupop) .

op  rm : GroupOpSet Group -> GroupOpSet .
eq  rm(eGroupOpSet,group) = eGroupOpSet .
ceq rm((sGroupOpSet(groupop) groupopset),group') = rm(groupopset,group')
    if (group' == group(groupop)) .
ceq rm((sGroupOpSet(groupop) groupopset),group') = (sGroupOpSet(groupop) rm(groupopset,group'))
    if (group' =/= group(groupop)) .

op group : GroupOpSet -> GroupSet .
eq group(eGroupOpSet) = eGroupSet .
eq group(sGroupOpSet(groupop) groupopset) = sGroupSet(group(groupop)) group(groupopset) .

op  get : GroupOpSet Group ~> GroupOp .
ceq get(sGroupOpSet(groupop) groupopset, group) =
    groupop
    if group(groupop) == group .
ceq get(sGroupOpSet(groupop) groupopset, group) =
    get(groupopset, group)
    if group(groupop) =/= group .

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

sort GroupAgentsAgents .
op groupagentsagents : Group AgentSet AgentSet -> GroupAgentsAgents .

var groupagentsagents groupagentsagents' : GroupAgentsAgents .
var transmembers orgmembers transmembers' orgmembers' : AgentSet .

op group : GroupAgentsAgents -> Group .
eq group(groupagentsagents(group,orgmembers,transmembers)) = group .

op orgmembers : GroupAgentsAgents -> AgentSet .
eq orgmembers(groupagentsagents(group,orgmembers,transmembers)) = orgmembers .

op transmembers : GroupAgentsAgents -> AgentSet .
eq transmembers(groupagentsagents(group,orgmembers,transmembers)) = transmembers .

op  update : GroupAgentsAgents Group AgentSet AgentSet -> GroupAgentsAgents .
ceq update(groupagentsagents(group,orgmembers,transmembers),group',orgmembers',transmembers') = 
    groupagentsagents(group,orgmembers',transmembers') if group == group' .
ceq update(groupagentsagents(group,orgmembers,transmembers),group',orgmembers',transmembers') = 
    groupagentsagents(group,orgmembers,transmembers) if group =/= group' .

op  update : GroupAgentsAgents Group AgentSet -> GroupAgentsAgents .
ceq update(groupagentsagents(group,orgmembers,transmembers),group',transmembers') = 
    groupagentsagents(group,orgmembers,transmembers') if group == group' .
ceq update(groupagentsagents(group,orgmembers,transmembers),group',transmembers') = 
    groupagentsagents(group,orgmembers,transmembers) if group =/= group' .

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

sort GroupAgentsAgentsSet .
op eGroupAgentsAgentsSet : -> GroupAgentsAgentsSet .
op sGroupAgentsAgentsSet : GroupAgentsAgents -> GroupAgentsAgentsSet .
op __ : GroupAgentsAgentsSet GroupAgentsAgentsSet -> GroupAgentsAgentsSet [assoc comm id: eGroupAgentsAgentsSet] .

var groupagentsagentsset groupagentsagentsset' : GroupAgentsAgentsSet .

op contains : GroupAgentsAgentsSet GroupAgentsAgents -> Bool .
eq contains(eGroupAgentsAgentsSet, groupagentsagents') = false .
eq contains((sGroupAgentsAgentsSet(groupagentsagents) groupagentsagentsset), groupagentsagents') = 
     (groupagentsagents' == groupagentsagents) or contains(groupagentsagentsset, groupagentsagents') .

op  rm : GroupAgentsAgentsSet Group -> GroupAgentsAgentsSet .
eq  rm(eGroupAgentsAgentsSet,group') = eGroupAgentsAgentsSet .
ceq rm((sGroupAgentsAgentsSet(groupagentsagents) groupagentsagentsset),group') = 
    rm(groupagentsagentsset,group')
    if (group(groupagentsagents) == group') .
ceq rm((sGroupAgentsAgentsSet(groupagentsagents) groupagentsagentsset),group') = 
    (sGroupAgentsAgentsSet(groupagentsagents) rm(groupagentsagentsset,group'))
    if (group(groupagentsagents) =/= group') .

op  update : GroupAgentsAgentsSet Group AgentSet AgentSet -> GroupAgentsAgentsSet .
eq  update(eGroupAgentsAgentsSet,group,orgmembers,transmembers) = 
    sGroupAgentsAgentsSet(groupagentsagents(group,orgmembers,transmembers)) .
ceq update(sGroupAgentsAgentsSet(groupagentsagents) groupagentsagentsset, group,orgmembers,transmembers) =
    sGroupAgentsAgentsSet(groupagentsagents)
    update(groupagentsagentsset,group,orgmembers,transmembers) 
    if group(groupagentsagents) =/= group .
ceq update(sGroupAgentsAgentsSet(groupagentsagents) groupagentsagentsset, group,orgmembers,transmembers) =
    update(groupagentsagentsset,group,orgmembers,transmembers)  
    if group(groupagentsagents) == group .

op  update' : GroupAgentsAgentsSet Group AgentSet -> GroupAgentsAgentsSet .
eq  update'(eGroupAgentsAgentsSet,group,transmembers) = eGroupAgentsAgentsSet .
ceq update'(sGroupAgentsAgentsSet(groupagentsagents) groupagentsagentsset, group,transmembers) =
    sGroupAgentsAgentsSet(update(groupagentsagents,group,transmembers))
    update'(groupagentsagentsset,group,transmembers)
    if group(groupagentsagents) == group .
ceq update'(sGroupAgentsAgentsSet(groupagentsagents) groupagentsagentsset, group,transmembers) =
    sGroupAgentsAgentsSet(groupagentsagents)
    update'(groupagentsagentsset,group,transmembers) 
    if group(groupagentsagents) =/= group .

op  get : GroupAgentsAgentsSet Group ~> GroupAgentsAgents .
ceq get(sGroupAgentsAgentsSet(groupagentsagents) groupagentsagentsset, group) =
    groupagentsagents
    if group(groupagentsagents) == group .
ceq get(sGroupAgentsAgentsSet(groupagentsagents) groupagentsagentsset, group) =
    get(groupagentsagentsset, group)
    if group(groupagentsagents) =/= group .

op  transmembers : GroupAgentsAgentsSet Group ~> AgentSet .
eq  transmembers(groupagentsagentsset,group) = transmembers(get(groupagentsagentsset,group)) .

-------------------------------
---- flush spread local state

op fstate : Agent GroupSet GroupSet GroupSet -> State .

op fmembers : Agent GroupAgentsAgentsSet -> State .

op fpending : Agent GroupOpSet -> State .

var pending : GroupOpSet .

var membinfoset membinfoset' : GroupAgentsAgentsSet .

op ftrans : Agent GroupSet -> State .

var transgroups transgroups' : GroupSet . 

var steady authorize agree : GroupSet .

op fiview : Agent ViewSet -> State . --- the views the agent has installed
op fpview : Agent ViewSet -> State . --- the pending views the agent has not yet installed

op fbuffer : Agent GMessageList -> State . --- messages are buffered here

-----------------------
--- f-connect
-----------------------

op f-connect-req' : Agent -> State .

rl  f-connect-req(client) =>
    f-connect-req'(client)
    sp-connect-req(client) .

rl  f-connect-req'(client)
    sp-connect-ack(client) =>
    fpview(client,eViewSet)
    fiview(client,eViewSet)
    fstate(client,eGroupSet,eGroupSet,eGroupSet)
    fbuffer(client,eGMessageList)
    fmembers(client,eGroupAgentsAgentsSet)
    ftrans(client,eGroupSet)
    fpending(client,eGroupOpSet)
    f-connect-ack(client) .

rl  f-connect-req'(client)
    sp-connect-err(client,error) =>
    f-connect-err(client,error) .

-----------------------
--- f-disconnect
-----------------------

op f-disconnect-req' : Agent -> State .

rl  f-disconnect-req(client) =>
    f-disconnect-req'(client)
    sp-disconnect-req(client) .

rl  f-disconnect-req'(client)
    fpview(client,viewset)
    fiview(client,viewset')
    fstate(client,steady,authorize,agree)
    fbuffer(client,gmessagelist)
    fmembers(client,membinfoset)
    ftrans(client,transgroups)
    fpending(client,pending)
    sp-disconnect-ack(client) =>
    f-disconnect-ack(client) .

rl  f-disconnect-req'(client)
    sp-disconnect-err(client,error) =>
    f-disconnect-err(client,error) .

-----------------------
--- f-join
-----------------------

op f-join-req' : Agent Group -> State .

rl  f-join-req(client,group) =>
    f-join-req'(client,group)
    sp-join-req(client,group) .

rl  f-join-req'(client,group)
    sp-join-ack(client) =>
    f-join-ack(client) .

rl  f-join-req'(client,group)
    sp-join-err(client,error) =>
    f-join-err(client,error) .

-----------------------
--- f-leave
-----------------------

op f-leave-req' : Agent Group -> State .

rl  f-leave-req(client,group) =>
    f-leave-req'(client,group)
    sp-leave-req(client,group) .

rl  f-leave-req'(client,group)
    sp-leave-ack(client) =>
    f-leave-ack(client) .

rl  f-leave-req'(client,group)
    sp-leave-err(client,error) =>
    f-leave-err(client,error) .

-----------------------
--- f-multicast
-----------------------

var mode : Mode .

op f-multicast-req' : Agent Mode Group FData -> State .

crl fiview(client,viewset)
    fstate(client,steady,authorize,agree)
    f-multicast-req(client,mode,group,fdata) =>
    fiview(client,viewset)
    fstate(client,steady,authorize,agree)
    f-multicast-req'(client,mode,group,fdata)
    sp-multicast-req(client,mode,group,fdatamsg(client,group,fdata,view))
    if view := get(viewset,group) /\
       not(contains(agree,group)) .

crl fiview(client,viewset)
    fstate(client,steady,authorize,agree)
    f-multicast-req(client,mode,group,fdata) =>
    fiview(client,viewset)
    fstate(client,steady,authorize,agree)
    f-multicast-req'(client,mode,group,fdata)
    sp-multicast-req(client,mode,group,fdatamsg(client,group,fdata,noview))
    if private(group) /\
       not(contains(agree,group)) .

crl fstate(client,steady,authorize,agree)
    f-multicast-req(client,mode,group,fdata) =>
    fstate(client,steady,authorize,agree)
    f-multicast-err(client,IllegalState)
    if contains(agree,group) .

rl  sp-multicast-ack(client)
    f-multicast-req'(client,mode,group,fdata) =>
    f-multicast-ack(client) .

rl  f-multicast-req'(client,mode,group,fdata)
    sp-multicast-err(client,error) =>
    f-multicast-err(client,error) .

-----------------------
--- f-receive
-----------------------

op  f-receive-req' : Agent -> State .
op  f-receive-req'' : Agent -> State .

--- aux functions for the following rules

op  receivedfok : Agent Group Agent GMessage -> Bool .
eq  receivedfok(client,group,agent,gmessage) = 
    isfok(gmessage) and sender(data(gmessage)) == agent and group(data(gmessage)) == group  .

op  receivedfok : Agent Group Agent GMessageList -> Bool .
eq  receivedfok(client,group,agent,eGMessageList) = false . 
eq  receivedfok(client,group,agent,sGMessageList(gmessage) gmessagelist) = 
    receivedfok(client,group,agent,gmessage) or
    receivedfok(client,group,agent,gmessagelist) .

op  receivedallfoks : Agent Group AgentList GMessageList -> Bool .
eq  receivedallfoks(client,group,eAgentList,gmessagelist) = true .
eq  receivedallfoks(client,group,(sAgentList(agent) agentlist),gmessagelist) =
    receivedfok(client,group,agent,gmessagelist) and
    receivedallfoks(client,group,agentlist,gmessagelist) .

op  receivedallfoks : Agent GroupSet ViewSet GMessageList -> GroupSet .
eq  receivedallfoks(agent,eGroupSet,viewset,gmessagelist) = eGroupSet .
eq  receivedallfoks(agent,sGroupSet(group) groupset,viewset,gmessagelist) = 
    (if receivedallfoks(agent,group,members(get(viewset,group)),gmessagelist) then sGroupSet(group) else eGroupSet fi)
    receivedallfoks(agent,groupset,viewset,gmessagelist) .

op  removefok : Agent Group Agent GMessageList -> GMessageList .
eq  removefok(client,group,agent,eGMessageList) = eGMessageList . 
ceq removefok(client,group,agent,sGMessageList(gmessage) gmessagelist) = 
    removefok(client,group,agent,gmessagelist) 
    if receivedfok(client,group,agent,gmessage) .
ceq removefok(client,group,agent,sGMessageList(gmessage) gmessagelist) = 
    sGMessageList(gmessage) 
    removefok(client,group,agent,gmessagelist) 
    if not(receivedfok(client,group,agent,gmessage)) .

op  removeallfoks : Agent Group AgentList GMessageList -> GMessageList .
eq  removeallfoks(client,group,eAgentList,gmessagelist) = gmessagelist .
eq  removeallfoks(client,group,(sAgentList(agent) agentlist),gmessagelist) =    
    removeallfoks(client,group,agentlist,removefok(client,group,agent,gmessagelist)) .

op  receivednextchange : GMessageList ~> GMessage .
ceq receivednextchange(sGMessageList(gmessage) gmessagelist) = gmessage
    if isgtrans(gmessage) or isgconf(gmessage) or isgjoin(gmessage) or 
       isgleave(gmessage) or isgselfleave(gmessage) or isgdisconnect(gmessage) .
ceq receivednextchange(sGMessageList(gmessage) gmessagelist) = receivednextchange(gmessagelist) 
    if isgdata(gmessage) .

op  receiveddeliverablefdata : GMessageList ViewSet ~> GMessage .
ceq receiveddeliverablefdata(sGMessageList(gmessage) gmessagelist, viewset) = 
    receiveddeliverablefdata(gmessagelist,viewset)
    if isgtrans(gmessage) or isgconf(gmessage) or isgjoin(gmessage) or 
       isgleave(gmessage) or isgselfleave(gmessage) or
       isgdisconnect(gmessage) or isfok(gmessage) .
ceq receiveddeliverablefdata(sGMessageList(gmessage) gmessagelist, viewset) = 
    gmessage 
    if isfdata(gmessage) /\ view(data(gmessage)) =/= noview /\ 
       view(data(gmessage)) == get(viewset,group(data(gmessage))) .
ceq receiveddeliverablefdata(sGMessageList(gmessage) gmessagelist, viewset) = 
    receiveddeliverablefdata(gmessagelist,viewset)
    if isfdata(gmessage) /\ view(data(gmessage)) =/= noview /\
       view(data(gmessage)) =/= get(viewset,group(data(gmessage))) .
ceq receiveddeliverablefdata(sGMessageList(gmessage) gmessagelist, viewset) = 
    gmessage 
    if isfdata(gmessage) /\ view(data(gmessage)) == noview .

--- check if any work to do, if not wait for next message

crl fstate(client, steady, authorize, agree)
    fpview(client,viewset)
    fiview(client,viewset')
    f-receive-req(client)
    fbuffer(client,gmessagelist) =>
    fstate(client, steady, authorize, agree)
    fpview(client,viewset)
    fiview(client,viewset')
    f-receive-req'(client)
    sp-receive-req(client)
    fbuffer(client,gmessagelist)
    if not(receiveddeliverablefdata(gmessagelist,viewset') :: GMessage) and
       not(receivednextchange(gmessagelist) :: GMessage) and
       receivedallfoks(client,agree,viewset,gmessagelist) == eGroupSet .

rl  f-receive-req'(client)
    sp-receive-err(client,error) =>
    f-receive-err(client,error) .

--- check if any deliverable data received, if yes pass it on to app

crl fstate(client, steady, authorize, agree)
    fiview(client,viewset')
    fbuffer(client,gmessagelist)
    f-receive-req(client) =>
    fstate(client, steady, authorize, agree)
    fiview(client,viewset')
    fbuffer(client,rm(gmessagelist,gmessage))
    f-receive-ack(client,data(gmessage))
    if gmessage := receiveddeliverablefdata(gmessagelist,viewset') .

--- check if any change message received, if yes send flush req

crl fstate(client, steady, authorize, agree)
    fbuffer(client,gmessagelist)
    ftrans(client,transgroups)
    f-receive-req(client) =>
    fstate(client, steady, authorize, agree)
    fbuffer(client,rm(gmessagelist,gmessage))
    ftrans(client,add'(transgroups,group))
    f-receive-ack(client,ftransmsg(group))
    if gmessage := receivednextchange(gmessagelist) /\ 
       isgtrans(gmessage) /\ group := group(gmessage) /\
       not(contains(transgroups,group)) .

crl fstate(client, steady, authorize, agree)
    fbuffer(client,gmessagelist)
    ftrans(client,transgroups)
    f-receive-req(client) =>
    fstate(client, steady, authorize, agree)
    fbuffer(client,rm(gmessagelist,gmessage))
    ftrans(client,transgroups)
    f-receive-req(client)
    if gmessage := receivednextchange(gmessagelist) /\ 
       isgtrans(gmessage) /\ group := group(gmessage) /\
       contains(transgroups,group) .

crl fstate(client, steady, authorize, agree)
    fpending(client, pending)
    fpview(client,viewset)
    fmembers(client,membinfoset)
    fbuffer(client,gmessagelist)
    f-receive-req(client) =>
    fstate(client, rm(steady, group), add(authorize,group), agree)
    fpending(client, add'(pending, changing(group)))
    fpview(client,viewset')
    fmembers(client,membinfoset')
    fbuffer(client,rm(gmessagelist,gmessage))
    f-receive-ack(client,freqmsg(client,group))
    if gmessage := receivednextchange(gmessagelist) /\ 
       isgconf(gmessage) /\ group := group(gmessage) /\
       not(contains(authorize agree, group)) /\
       viewset' := update(viewset,group,view(gmessage)) /\
       transmembers := transset(gmessage) /\
       orgmembers := agentset(members(view(gmessage))) /\
       membinfoset' := update(membinfoset,group,orgmembers,transmembers) .

crl fstate(client, steady, authorize, agree)
    fpview(client,viewset)
    fmembers(client,membinfoset)
    fbuffer(client,gmessagelist)
    f-receive-req(client) =>
    fstate(client, steady, authorize, agree)
    fpview(client,viewset')
    fmembers(client,membinfoset')
    fbuffer(client,rm(gmessagelist,gmessage))
    f-receive-req(client)
    if gmessage := receivednextchange(gmessagelist) /\ 
       isgconf(gmessage) /\ group := group(gmessage) /\
       contains(authorize agree, group) /\
       viewset' := update(viewset,group,view(gmessage)) /\
       transmembers := inter(transmembers(membinfoset,group),transset(gmessage)) /\
       membinfoset' := update'(membinfoset,group,transmembers) .

crl fstate(client, steady, authorize, agree)
    fpending(client, pending)
    fpview(client,viewset)
    fmembers(client,membinfoset)
    fbuffer(client,gmessagelist)
    f-receive-req(client) =>
    fstate(client, rm(steady, group), add(authorize,group), agree)
    fpending(client, add'(pending,joining(sender(gmessage),group)))
    fpview(client,viewset')
    fmembers(client,membinfoset')
    fbuffer(client,rm(gmessagelist,gmessage))
    f-receive-ack(client,freqmsg(client,group))
    if gmessage := receivednextchange(gmessagelist) /\ 
       isgjoin(gmessage) /\ group := group(gmessage) /\ 
       not(contains(authorize agree, group)) /\
       viewset' := update(viewset,group,view(gmessage)) /\
       orgmembers := agentset(members(view(gmessage))) /\
       membinfoset' := update(membinfoset,group,orgmembers,orgmembers) .

crl fstate(client, steady, authorize, agree)
    fpview(client,viewset)
    fmembers(client,membinfoset)
    fpending(client, pending)
    fbuffer(client,gmessagelist)
    f-receive-req(client) =>
    fstate(client, rm(steady, group), add(authorize,group), agree)
    fpview(client,viewset')
    fmembers(client,membinfoset')
    fpending(client, add'(pending,leaving(sender(gmessage),group)))
    fbuffer(client,rm(gmessagelist,gmessage))
    f-receive-ack(client,freqmsg(client,group))
    if gmessage := receivednextchange(gmessagelist) /\ 
       isgleave(gmessage) /\ group := group(gmessage) /\ 
       not(contains(authorize agree, group)) /\
       viewset' := update(viewset,group,view(gmessage)) /\
       orgmembers := agentset(members(view(gmessage))) /\
       membinfoset' := update(membinfoset,group,orgmembers,orgmembers) .

crl fstate(client, steady, authorize, agree)
    fpview(client,viewset)
    fmembers(client,membinfoset)
    fpending(client, pending)
    fbuffer(client,gmessagelist)
    f-receive-req(client) =>
    fstate(client, rm(steady, group), add(authorize,group), agree)
    fpview(client,viewset')
    fmembers(client,membinfoset')
    fpending(client, add'(pending,disconnecting(sender(gmessage),group)))
    fbuffer(client,rm(gmessagelist,gmessage))
    f-receive-ack(client,freqmsg(client,group))
    if gmessage := receivednextchange(gmessagelist) /\ 
       isgdisconnect(gmessage) /\ group := group(gmessage) /\ 
       not(contains(authorize agree, group)) /\
       viewset' := update(viewset,group,view(gmessage)) /\
       orgmembers := agentset(members(view(gmessage))) /\
       membinfoset' := update(membinfoset,group,orgmembers,orgmembers) .

crl fstate(client, steady, authorize, agree)
    fpview(client,viewset)
    fiview(client,viewset')
    fmembers(client,membinfoset)
    fbuffer(client,gmessagelist)
    f-receive-req(client) =>
    fstate(client, steady, authorize, agree)
    fpview(client,viewset''')
    fiview(client,viewset'')
    fmembers(client,membinfoset')
    fbuffer(client,rm(gmessagelist,gmessage))
    f-receive-ack(client,fselfleavemsg(client,group))
    if gmessage := receivednextchange(gmessagelist) /\ 
       isgselfleave(gmessage) /\ group := group(gmessage) /\ 
       viewset'' := rm(viewset',group) /\
       viewset''' := rm(viewset,group) /\
       membinfoset' := rm(membinfoset,group) .

--- check if floks arrived then deliver join to app

crl fstate(client, steady, authorize, agree)
    fpending(client, pending)
    fpview(client,viewset)
    fiview(client,viewset')
    f-receive-req(client)
    fbuffer(client,gmessagelist) =>
    fstate(client, add(steady,group), authorize, rm(agree,group))
    fpending(client, rm(pending,group))
    fpview(client,viewset''')
    fiview(client,viewset'')
    fbuffer(client,removeallfoks(client,group,members(view),gmessagelist))
    f-receive-ack(client,fjoinmsg(sender(get(pending,group)),group,view))
    if sGroupSet(group) groupset := receivedallfoks(client,agree,viewset,gmessagelist) /\
       joining(pending,group) /\ view := get(viewset,group) /\
       viewset'' := update(viewset',group,view) /\
       viewset''' := rm(viewset,group) .

crl fstate(client, steady, authorize, agree)
    fpending(client, pending)
    fpview(client,viewset)
    fiview(client,viewset')
    f-receive-req(client)
    fbuffer(client,gmessagelist) =>
    fstate(client, add(steady,group), authorize, rm(agree,group))
    fpending(client, rm(pending,group))
    fpview(client,viewset''')
    fiview(client,viewset'')
    fbuffer(client,removeallfoks(client,group,members(view),gmessagelist))
    f-receive-ack(client,fleavemsg(sender(get(pending,group)),group,view))
    if sGroupSet(group) groupset := receivedallfoks(client,agree,viewset,gmessagelist) /\
       leaving(pending,group) /\ view := get(viewset,group) /\
       viewset'' := update(viewset',group,view) /\
       viewset''' := rm(viewset,group) .

crl fstate(client, steady, authorize, agree)
    fpending(client, pending)
    fpview(client,viewset)
    fiview(client,viewset')
    f-receive-req(client)
    fbuffer(client,gmessagelist) =>
    fstate(client, add(steady,group), authorize, rm(agree,group))
    fpending(client, rm(pending,group))
    fpview(client,viewset''')
    fiview(client,viewset'')
    fbuffer(client,removeallfoks(client,group,members(view),gmessagelist))
    f-receive-ack(client,fdisconnectmsg(sender(get(pending,group)),group,view))
    if sGroupSet(group) groupset := receivedallfoks(client,agree,viewset,gmessagelist) /\
       disconnecting(pending,group) /\ view := get(viewset,group) /\
       viewset'' := update(viewset',group,view) /\
       viewset''' := rm(viewset,group) .

crl fstate(client, steady, authorize, agree)
    fpending(client, pending)
    fpview(client,viewset)
    fiview(client,viewset')
    fmembers(client,membinfoset)
    ftrans(client,transgroups)
    f-receive-req(client)
    fbuffer(client,gmessagelist) =>
    fstate(client, add(steady,group), authorize, rm(agree,group))
    fpending(client, rm(pending,group))
    fpview(client,viewset''')
    fiview(client,viewset'')
    fmembers(client,membinfoset)
    ftrans(client,rm(transgroups,group))
    fbuffer(client,removeallfoks(client,group,members(view),gmessagelist))
    f-receive-ack(client,fconfmsg(group,view,transmembers(membinfoset,group)))
    if sGroupSet(group) groupset := receivedallfoks(client,agree,viewset,gmessagelist) /\
       changing(pending,group) /\ view := get(viewset,group) /\
       viewset'' := update(viewset',group,view) /\
       viewset''' := rm(viewset,group) .

--- pass message to app or buffer message

crl fiview(client,viewset)
    f-receive-req'(client)
    sp-receive-ack(client,gmessage) =>
    fiview(client,viewset)
    f-receive-ack(client,data(gmessage))
    if isfdata(gmessage) /\ view(data(gmessage)) == noview or 
                            view(data(gmessage)) == get(viewset,group(data(gmessage))) .

crl fiview(client,viewset)
    f-receive-req'(client)
    fbuffer(client,gmessagelist)
    sp-receive-ack(client,gmessage) =>
    fiview(client,viewset)
    f-receive-req(client)
    fbuffer(client,gmessagelist sGMessageList(gmessage))
    if isfdata(gmessage) /\ view(data(gmessage)) =/= noview /\ 
                            view(data(gmessage)) =/= get(viewset,group(data(gmessage)))  .

crl f-receive-req'(client)
    fbuffer(client,gmessagelist)
    sp-receive-ack(client,gmessage) =>
    f-receive-req(client)
    fbuffer(client,gmessagelist sGMessageList(gmessage)) 
    if isgtrans(gmessage) or isgconf(gmessage) or 
       isgjoin(gmessage) or isgleave(gmessage) or isgselfleave(gmessage) or
       isgdisconnect(gmessage) or
       isfok(gmessage) .

-----------------------
--- f-flushok
-----------------------

op  f-flushok-req' : Agent Group -> State .

crl fstate(client, steady, authorize, agree)
    f-flushok-req(client,group) =>
    fstate(client, steady, rm(authorize,group), add(agree,group))
    sp-multicast-req(client,fifo,group,fokmsg(client,group)) 
    f-flushok-req'(client,group)
    if contains(authorize,group) .

crl fstate(client, steady, authorize, agree)
    f-flushok-req(client,group) =>
    fstate(client, steady, authorize, agree)
    f-flushok-err(client,IllegalState)
    if not(contains(authorize,group)) .

rl  f-flushok-req'(client,group)
    sp-multicast-ack(client) => 
    f-flushok-ack(client) .

rl  f-flushok-req'(client,group)
    sp-multicast-err(client,error) =>
    f-flushok-err(client,error) .

endm