fmod GROUPVAR is

protecting SMESSAGE .

var client agent : Agent .
var group group' : Group .
var agentset agentset' : AgentSet .
var context context' : Context .
var token : Token .
var viewset viewset' : ViewSet .
var view : View .
var fmessage : FMessage .
var fmessagelist : FMessageList .
var transset transset' : AgentSet .
var fdata : FData .
var error : Error .
var smessage smessage' : SMessage .
var sdata : SData .
var smessagelist smessagelist' : SMessageList .

--- various types to store group specific information

sort GroupAgentSet .

op groupagentset : Group AgentSet -> GroupAgentSet .

op group : GroupAgentSet -> Group .
eq group(groupagentset(group,agentset)) = group .

op agents : GroupAgentSet -> AgentSet .
eq agents(groupagentset(group,agentset)) = agentset .

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

var groupagentset groupagentsset' : GroupAgentSet .

sort GroupAgentSetSet .
op eGroupAgentSetSet : -> GroupAgentSetSet .
op sGroupAgentSetSet : GroupAgentSet -> GroupAgentSetSet .
op __ : GroupAgentSetSet GroupAgentSetSet -> GroupAgentSetSet [assoc comm id: eGroupAgentSetSet] .

var groupagentsetset groupagentsetset' : GroupAgentSetSet .

op  get : GroupAgentSetSet Group ~> AgentSet .
ceq get(sGroupAgentSetSet(groupagentset) groupagentsetset, group') = agents(groupagentset)
    if group(groupagentset) == group' .
ceq get(sGroupAgentSetSet(groupagentset) groupagentsetset, group') = get(groupagentsetset,group')
    if group(groupagentset) =/= group' .

op  update : GroupAgentSetSet Group AgentSet -> GroupAgentSetSet .
eq  update(eGroupAgentSetSet, group', agentset') =
    sGroupAgentSetSet(groupagentset(group', agentset')) .
ceq update(sGroupAgentSetSet(groupagentset(group,agentset)) groupagentsetset, group', agentset') = 
    update(groupagentsetset,group',agentset')
    if group == group' .
ceq update(sGroupAgentSetSet(groupagentset(group,agentset)) groupagentsetset, group', agentset') = 
    sGroupAgentSetSet(groupagentset(group,agentset)) update(groupagentsetset,group',agentset')
    if group =/= group' .

op  rm : GroupAgentSetSet Group AgentSet -> GroupAgentSetSet .
eq  rm(eGroupAgentSetSet, group', agentset') =
    eGroupAgentSetSet .
ceq rm(sGroupAgentSetSet(groupagentset(group,agentset)) groupagentsetset, group', agentset') = 
    rm(groupagentsetset,group',agentset')
    if group == group' .
ceq rm(sGroupAgentSetSet(groupagentset(group,agentset)) groupagentsetset, group', agentset') = 
    sGroupAgentSetSet(groupagentset(group,agentset)) rm(groupagentsetset,group',agentset')
    if group =/= group' .

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

sort GroupContext .

op groupcontext : Group Context -> GroupContext .

op group : GroupContext -> Group .
eq group(groupcontext(group,context)) = group .

op context : GroupContext -> Context .
eq context(groupcontext(group,context)) = context .

var groupcontext groupcontext' : GroupContext .

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

sort GroupContextSet .
op eGroupContextSet : -> GroupContextSet .
op sGroupContextSet : GroupContext -> GroupContextSet .
op __ : GroupContextSet GroupContextSet -> GroupContextSet [assoc comm id: eGroupContextSet] .

var groupcontextset groupcontextset' : GroupContextSet .

op  get : GroupContextSet Group ~> Context .
ceq get(sGroupContextSet(groupcontext) groupcontextset, group') = context(groupcontext)
    if group(groupcontext) == group' .
ceq get(sGroupContextSet(groupcontext) groupcontextset, group') = get(groupcontextset,group')
    if group(groupcontext) =/= group' .

op  update : GroupContextSet Group Context -> GroupContextSet .
eq  update(eGroupContextSet, group', context') =
    sGroupContextSet(groupcontext(group', context')) .
ceq update(sGroupContextSet(groupcontext(group,context)) groupcontextset, group', context') = 
    update(groupcontextset,group',context')
    if group == group' .
ceq update(sGroupContextSet(groupcontext(group,context)) groupcontextset, group', context') = 
    sGroupContextSet(groupcontext(group,context)) update(groupcontextset,group',context')
    if group =/= group' .

op  rm : GroupContextSet Group Context -> GroupContextSet .
eq  rm(eGroupContextSet, group', context') =
    eGroupContextSet .
ceq rm(sGroupContextSet(groupcontext(group,context)) groupcontextset, group', context') = 
    rm(groupcontextset,group',context')
    if group == group' .
ceq rm(sGroupContextSet(groupcontext(group,context)) groupcontextset, group', context') = 
    sGroupContextSet(groupcontext(group,context)) rm(groupcontextset,group',context')
    if group =/= group' .

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

sort GroupSMessage .

op groupsmessage : Group SMessage -> GroupSMessage .

op group : GroupSMessage -> Group .
eq group(groupsmessage(group,smessage)) = group .

op smessage : GroupSMessage -> SMessage .
eq smessage(groupsmessage(group,smessage)) = smessage .

var groupsmessage groupsmessage' : GroupSMessage .

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

sort GroupSMessageSet .
op eGroupSMessageSet : -> GroupSMessageSet .
op sGroupSMessageSet : GroupSMessage -> GroupSMessageSet .
op __ : GroupSMessageSet GroupSMessageSet -> GroupSMessageSet [assoc comm id: eGroupSMessageSet] .

var groupsmessageset groupsmessageset' : GroupSMessageSet .

op  get : GroupSMessageSet Group ~> SMessage .
ceq get(sGroupSMessageSet(groupsmessage) groupsmessageset, group') = smessage(groupsmessage)
    if group(groupsmessage) == group' .
ceq get(sGroupSMessageSet(groupsmessage) groupsmessageset, group') = get(groupsmessageset,group')
    if group(groupsmessage) =/= group' .

op  update : GroupSMessageSet Group SMessage -> GroupSMessageSet .
eq  update(eGroupSMessageSet, group', smessage') =
    sGroupSMessageSet(groupsmessage(group', smessage')) .
ceq update(sGroupSMessageSet(groupsmessage(group,smessage)) groupsmessageset, group', smessage') = 
    update(groupsmessageset,group',smessage')
    if group == group' .
ceq update(sGroupSMessageSet(groupsmessage(group,smessage)) groupsmessageset, group', smessage') = 
    sGroupSMessageSet(groupsmessage(group,smessage)) update(groupsmessageset,group',smessage')
    if group =/= group' .

op  rm : GroupSMessageSet Group SMessage -> GroupSMessageSet .
eq  rm(eGroupSMessageSet, group', smessage') =
    eGroupSMessageSet .
ceq rm(sGroupSMessageSet(groupsmessage(group,smessage)) groupsmessageset, group', smessage') = 
    rm(groupsmessageset,group',smessage')
    if group == group' .
ceq rm(sGroupSMessageSet(groupsmessage(group,smessage)) groupsmessageset, group', smessage') = 
    sGroupSMessageSet(groupsmessage(group,smessage)) rm(groupsmessageset,group',smessage')
    if group =/= group' .

op  update-transset : GroupSMessageSet Group AgentSet -> GroupSMessageSet .
eq  update-transset(groupsmessageset, group', transset') =
    update(groupsmessageset,group',update-transset(get(groupsmessageset,group'),transset')) .

endfm