fmod FMESSAGE is protecting BOOL . protecting NAT . protecting STRING . protecting SPREAD . 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 grouplist : GroupList . var transset : AgentSet . --- Group Type sort GroupType . op group-vs : -> GroupType . op group-evs : -> GroupType . var grouptype : GroupType . op isvs : GroupType -> Bool . eq isvs(group-vs) = true . eq isvs(group-evs) = false . op isevs : GroupType -> Bool . eq isevs(group-vs) = false . eq isevs(group-evs) = true . --- Flush Type sort FlushType . op force : -> FlushType . var flushtype : FlushType . op isforce : FlushType -> Bool . eq isforce(force) = true . --- FData sort FData . op fdata : String -> FData . sort FMessage . subsort FMessage < GData . --- some flush layer messages are group layer data --- messages visible to the upper layer op fdatamsg --- regular message : Agent --- sender Group --- all receivers FData --- contents View --- sending view -> FMessage . op freqmsg --- flush request message : Agent Group --- affected group -> FMessage . op freqmsg --- flush request message : Agent Group --- affected group FlushType --- force freq -> FMessage . op ftransmsg --- transitional view message : Group --- affected group -> FMessage . op fjoinmsg --- regular view message caused by join : Agent --- joining agent Group --- affected group View --- new view -> FMessage . op fleavemsg --- regular view message caused by leave : Agent --- joining agent Group --- affected group View --- new view -> FMessage . op fdisconnectmsg --- regular view message caused by disconnect : Agent --- disconnecting agent Group --- affected group View --- new view -> FMessage . op fconfmsg --- regular view message caused by network : Group --- affected group View --- new view AgentSet --- transitional set of agents -> FMessage . --- (i.e. agents that came with client into the new view) op fselfleavemsg --- selfleavemsg message : Agent --- leaving agent Group --- affected group -> FMessage . --- internal messages (not visible to the upper layer) op fokmsg --- internal flush ok message : Agent Group --- affected group -> FMessage . ----------------------- op isfreq : FMessage -> Bool . eq isfreq(fdatamsg(client,group,fdata,view)) = false . eq isfreq(freqmsg(client,group)) = true . eq isfreq(freqmsg(client,group,flushtype)) = true . eq isfreq(fokmsg(client,group)) = false . eq isfreq(fjoinmsg(client,group,view)) = false . eq isfreq(fleavemsg(client,group,view)) = false . eq isfreq(ftransmsg(group)) = false . eq isfreq(fconfmsg(group,view,transset)) = false . eq isfreq(fselfleavemsg(client,group)) = false . eq isfreq(fdisconnectmsg(client,group,view)) = false . op isfok : FMessage -> Bool . eq isfok(fdatamsg(client,group,fdata,view)) = false . eq isfok(freqmsg(client,group)) = false . eq isfok(freqmsg(client,group,flushtype)) = false . eq isfok(fokmsg(client,group)) = true . op isfdata : FMessage -> Bool . eq isfdata(fdatamsg(client,group,fdata,view)) = true . eq isfdata(freqmsg(client,group)) = false . eq isfdata(freqmsg(client,group,flushtype)) = false . eq isfdata(fokmsg(client,group)) = false . eq isfdata(fjoinmsg(client,group,view)) = false . eq isfdata(fleavemsg(client,group,view)) = false . eq isfdata(ftransmsg(group)) = false . eq isfdata(fconfmsg(group,view,transset)) = false . eq isfdata(fselfleavemsg(client,group)) = false . eq isfdata(fdisconnectmsg(client,group,view)) = false . op isfjoin : FMessage -> Bool . eq isfjoin(fdatamsg(client,group,fdata,view)) = false . eq isfjoin(freqmsg(client,group)) = false . eq isfjoin(freqmsg(client,group,flushtype)) = false . eq isfjoin(fokmsg(client,group)) = false . eq isfjoin(fjoinmsg(client,group,view)) = true . eq isfjoin(fleavemsg(client,group,view)) = false . eq isfjoin(ftransmsg(group)) = false . eq isfjoin(fconfmsg(group,view,transset)) = false . eq isfjoin(fselfleavemsg(client,group)) = false . eq isfjoin(fdisconnectmsg(client,group,view)) = false . op isfleave : FMessage -> Bool . eq isfleave(fdatamsg(client,group,fdata,view)) = false . eq isfleave(freqmsg(client,group)) = false . eq isfleave(freqmsg(client,group,flushtype)) = false . eq isfleave(fokmsg(client,group)) = false . eq isfleave(fjoinmsg(client,group,view)) = false . eq isfleave(fleavemsg(client,group,view)) = true . eq isfleave(ftransmsg(group)) = false . eq isfleave(fconfmsg(group,view,transset)) = false . eq isfleave(fselfleavemsg(client,group)) = false . eq isfleave(fdisconnectmsg(client,group,view)) = false . op isfselfleave : FMessage -> Bool . eq isfselfleave(fdatamsg(client,group,fdata,view)) = false . eq isfselfleave(freqmsg(client,group)) = false . eq isfselfleave(freqmsg(client,group,flushtype)) = false . eq isfselfleave(fokmsg(client,group)) = false . eq isfselfleave(fjoinmsg(client,group,view)) = false . eq isfselfleave(fleavemsg(client,group,view)) = false . eq isfselfleave(ftransmsg(group)) = false . eq isfselfleave(fconfmsg(group,view,transset)) = false . eq isfselfleave(fselfleavemsg(client,group)) = true . eq isfselfleave(fdisconnectmsg(client,group,view)) = false . op isftrans : FMessage -> Bool . eq isftrans(fdatamsg(client,group,fdata,view)) = false . eq isftrans(freqmsg(client,group)) = false . eq isftrans(freqmsg(client,group,flushtype)) = false . eq isftrans(fokmsg(client,group)) = false . eq isftrans(fjoinmsg(client,group,view)) = false . eq isftrans(fleavemsg(client,group,view)) = false . eq isftrans(ftransmsg(group)) = true . eq isftrans(fconfmsg(group,view,transset)) = false . eq isftrans(fselfleavemsg(client,group)) = false . eq isftrans(fdisconnectmsg(client,group,view)) = false . op isfconf : FMessage -> Bool . eq isfconf(fdatamsg(client,group,fdata,view)) = false . eq isfconf(freqmsg(client,group)) = false . eq isfconf(freqmsg(client,group,flushtype)) = false . eq isfconf(fokmsg(client,group)) = false . eq isfconf(fjoinmsg(client,group,view)) = false . eq isfconf(fleavemsg(client,group,view)) = false . eq isfconf(ftransmsg(group)) = false . eq isfconf(fconfmsg(group,view,transset)) = true . eq isfconf(fselfleavemsg(client,group)) = false . eq isfconf(fdisconnectmsg(client,group,view)) = false . op isfdisconnect : FMessage -> Bool . eq isfdisconnect(fdatamsg(client,group,fdata,view)) = false . eq isfdisconnect(freqmsg(client,group)) = false . eq isfdisconnect(freqmsg(client,group,flushtype)) = false . eq isfdisconnect(fokmsg(client,group)) = false . eq isfdisconnect(fjoinmsg(client,group,view)) = false . eq isfdisconnect(fleavemsg(client,group,view)) = false . eq isfdisconnect(ftransmsg(group)) = false . eq isfdisconnect(fconfmsg(group,view,transset)) = false . eq isfdisconnect(fselfleavemsg(client,group)) = false . eq isfdisconnect(fdisconnectmsg(client,group,view)) = true . op isviewmsg : FMessage ~> Bool . eq isviewmsg(fdatamsg(client,group,fdata,view)) = false . eq isviewmsg(freqmsg(client,group)) = false . eq isviewmsg(freqmsg(client,group,flushtype)) = false . eq isviewmsg(fokmsg(client,group)) = false . eq isviewmsg(fjoinmsg(agent,group,view)) = true . eq isviewmsg(fleavemsg(agent,group,view)) = true . eq isviewmsg(fconfmsg(group,view,agentset)) = true . eq isviewmsg(fdisconnectmsg(agent,group,view)) = true . eq isviewmsg(fselfleavemsg(client,group)) = false . op view : FMessage ~> View . eq view(fdatamsg(client,group,fdata,view)) = view . eq view(fjoinmsg(client,group,view)) = view . eq view(fleavemsg(client,group,view)) = view . eq view(fdisconnectmsg(client,group,view)) = view . eq view(fconfmsg(group,view,agentset)) = view . op group : FMessage ~> Group . eq group(fdatamsg(client,group,fdata,view)) = group . eq group(freqmsg(client,group)) = group . eq group(freqmsg(client,group,flushtype)) = group . eq group(fokmsg(client,group)) = group . eq group(fjoinmsg(client,group,view)) = group . eq group(fleavemsg(client,group,view)) = group . eq group(ftransmsg(group)) = group . eq group(fconfmsg(group,view,transset)) = group . eq group(fselfleavemsg(client,group)) = group . eq group(fdisconnectmsg(client,group,view)) = group . op sender : FMessage ~> Agent . eq sender(fdatamsg(client,group,fdata,view)) = client . eq sender(freqmsg(client,group)) = client . eq sender(freqmsg(client,group,flushtype)) = client . eq sender(fokmsg(client,group)) = client . eq sender(fjoinmsg(client,group,view)) = client . op flushtype : FMessage ~> FlushType . eq flushtype(freqmsg(client,group,flushtype)) = flushtype . op data : FMessage ~> FData . eq data(fdatamsg(client,group,fdata,view)) = fdata . ----------------------- sort FMessageList . op eFMessageList : -> FMessageList . op sFMessageList : FMessage -> FMessageList . op __ : FMessageList FMessageList -> FMessageList [assoc id: eFMessageList] . var fmessagelist fmessagelist' : FMessageList . var fmessage, fmessage' : FMessage . op contains : FMessageList FMessage -> Bool . eq contains(eFMessageList, fmessage') = false . eq contains((sFMessageList(fmessage) fmessagelist), fmessage') = (fmessage' == fmessage) or contains(fmessagelist, fmessage') . op contains : FMessageList FMessageList -> Bool . eq contains(fmessagelist, eFMessageList) = false . eq contains(fmessagelist, (sFMessageList(fmessage') fmessagelist')) = contains(fmessagelist, fmessage') or contains(fmessagelist, fmessagelist') . op add : FMessageList FMessage -> FMessageList . eq add(fmessagelist,fmessage) = (fmessagelist sFMessageList(fmessage)) . op add : FMessageList FMessageList -> FMessageList . eq add(fmessagelist,fmessagelist') = (fmessagelist fmessagelist') . op add' : FMessageList FMessage -> FMessageList . ceq add'(fmessagelist,fmessage) = fmessagelist if contains(fmessagelist, fmessage) . ceq add'(fmessagelist,fmessage) = (fmessagelist sFMessageList(fmessage)) if not(contains(fmessagelist, fmessage)) . op rm : FMessageList FMessage -> FMessageList . eq rm(eFMessageList, fmessage) = eFMessageList . ceq rm((sFMessageList(fmessage) fmessagelist), fmessage') = rm(fmessagelist, fmessage') if (fmessage' == fmessage) . ceq rm((sFMessageList(fmessage) fmessagelist), fmessage') = (sFMessageList(fmessage) rm(fmessagelist, fmessage')) if (fmessage' =/= fmessage) . op rm : FMessageList FMessageList -> FMessageList . eq rm(fmessagelist, eFMessageList) = fmessagelist . eq rm(fmessagelist, (sFMessageList(fmessage') fmessagelist')) = rm(rm(fmessagelist, fmessage'), fmessagelist') . op subset : FMessageList FMessageList -> Bool . eq subset(eFMessageList, fmessagelist') = true . eq subset((sFMessageList(fmessage) fmessagelist), fmessagelist') = contains(fmessagelist',fmessage) and subset(fmessagelist,fmessagelist') . op len : FMessageList -> Nat . eq len(eFMessageList) = 0 . eq len(sFMessageList(fmessage) fmessagelist) = 1 + len(fmessagelist) . var i : Nat . op ith : FMessageList Nat ~> FMessage . eq ith((sFMessageList(fmessage) fmessagelist), 1) = fmessage . eq ith((sFMessageList(fmessage) fmessagelist), (s i)) = ith(fmessagelist,i) . op index : FMessageList FMessage ~> Nat . ceq index((sFMessageList(fmessage) fmessagelist), fmessage') = 1 if fmessage == fmessage' . ceq index((sFMessageList(fmessage) fmessagelist), fmessage') = 1 + index(fmessagelist,fmessage') if fmessage =/= fmessage' . op last : FMessageList ~> FMessage . eq last(fmessagelist sFMessageList(fmessage)) = fmessage . op last : FMessageList Nat ~> FMessage . eq last(fmessagelist sFMessageList(fmessage), 1) = fmessage . eq last(fmessagelist sFMessageList(fmessage), (s i)) = last(fmessagelist, i) . op first : FMessageList ~> FMessage . eq first(sFMessageList(fmessage) fmessagelist) = fmessage . op next : FMessageList FMessage ~> FMessage . ceq next(sFMessageList(fmessage) fmessagelist, fmessage') = first(fmessagelist) if fmessage == fmessage' . ceq next(sFMessageList(fmessage) fmessagelist, fmessage') = next(fmessagelist, fmessage') if fmessage =/= fmessage' . endfm