fmod GROUP is

protecting BOOL .
protecting STRING .
protecting AGENT .

var agent agent' : Agent .

sort Group .   --- groups

var group group' : Group .

op group : String -> Group .
op privategroup : Agent -> Group .
op nogroup : -> Group . --- for msg-disconnect

var str : String .

op private : Group -> Bool . --- private group has single member
eq private(group(str)) = false .	
eq private(privategroup(agent)) = true .	

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

sort GroupSet .
op eGroupSet : -> GroupSet .
op sGroupSet : Group -> GroupSet .
op __ : GroupSet GroupSet -> GroupSet [assoc comm id: eGroupSet] .

var groupset groupset' : GroupSet .

op contains : GroupSet Group -> Bool .
eq contains(eGroupSet, group') = false .
eq contains((sGroupSet(group) groupset), group') = 
     (group' == group) or contains(groupset, group') .

op add : GroupSet Group -> GroupSet .
eq add(groupset,group) = (groupset sGroupSet(group)) .

op  add' : GroupSet Group -> GroupSet .
ceq add'(groupset,group) = groupset 
    if contains(groupset, group) .
ceq add'(groupset,group) = (groupset sGroupSet(group)) 
    if not(contains(groupset, group)) .

op  rm : GroupSet Group -> GroupSet .
eq  rm(eGroupSet,group) = eGroupSet .
ceq rm((sGroupSet(group) groupset),group') = rm(groupset,group')
    if (group' == group) .
ceq rm((sGroupSet(group) groupset),group') = (sGroupSet(group) rm(groupset,group'))
    if (group' =/= group) .

-----------------------
sort GroupList .
op eGroupList : -> GroupList .
op sGroupList : Group -> GroupList .
op __ : GroupList GroupList -> GroupList [assoc id: eGroupList] .

var grouplist grouplist' knowngroups : GroupList .

op contains : GroupList Group -> Bool .
eq contains(eGroupList, group') = false .
eq contains((sGroupList(group) grouplist), group') = 
     (group' == group) or contains(grouplist, group') .

op add : GroupList Group -> GroupList .
eq add(grouplist,group) = (grouplist sGroupList(group)) .

op  add' : GroupList Group -> GroupList .
ceq add'(grouplist,group) = grouplist 
    if contains(grouplist, group) .
ceq add'(grouplist,group) = (grouplist sGroupList(group)) 
    if not(contains(grouplist, group)) .

op  rm : GroupList Group -> GroupList .
eq  rm(eGroupList,group) = eGroupList .
ceq rm((sGroupList(group) grouplist),group') = rm(grouplist,group')
    if (group' == group) .
ceq rm((sGroupList(group) grouplist),group') = (sGroupList(group) rm(grouplist,group'))
    if (group' =/= group) .

op  rmdoubles : GroupList -> GroupList .
eq  rmdoubles(eGroupList) = eGroupList .
ceq rmdoubles(grouplist sGroupList(group)) = 
    rmdoubles(grouplist) 
    if contains(grouplist,group) .
ceq rmdoubles(grouplist sGroupList(group)) = 
    rmdoubles(grouplist) sGroupList(group) 
    if not(contains(grouplist,group)) .
   
endfm