fmod ASSOCMEMBSET is protecting SMESSAGE . --- AssocMembSet sort AssocMembSet . op assocmembset : AgentSet KeyId -> AssocMembSet . var assocmembset assocmembset' : AssocMembSet . var memberset memberset' : AgentSet . var keyid keyid' : KeyId . op memberset : AssocMembSet -> AgentSet . eq memberset(assocmembset(memberset,keyid)) = memberset . op keyid : AssocMembSet -> KeyId . eq keyid(assocmembset(memberset,keyid)) = keyid . --- AssocMembSetList sort AssocMembSetList . op eAssocMembSetList : -> AssocMembSetList . op sAssocMembSetList : AssocMembSet -> AssocMembSetList . op __ : AssocMembSetList AssocMembSetList -> AssocMembSetList [assoc id: eAssocMembSetList] . var assocmembsetlist assocmembsetlist' : AssocMembSetList . op contains : AssocMembSetList AssocMembSet -> Bool . eq contains(eAssocMembSetList, assocmembset') = false . eq contains((sAssocMembSetList(assocmembset) assocmembsetlist), assocmembset') = (assocmembset' == assocmembset) or contains(assocmembsetlist, assocmembset') . op contains : AssocMembSetList AssocMembSetList -> Bool . eq contains(assocmembsetlist, eAssocMembSetList) = false . eq contains(assocmembsetlist, (sAssocMembSetList(assocmembset') assocmembsetlist')) = contains(assocmembsetlist, assocmembset') or contains(assocmembsetlist, assocmembsetlist') . op add : AssocMembSetList AssocMembSet -> AssocMembSetList . eq add(assocmembsetlist,assocmembset) = (assocmembsetlist sAssocMembSetList(assocmembset)) . op add : AssocMembSetList AssocMembSetList -> AssocMembSetList . eq add(assocmembsetlist,assocmembsetlist') = (assocmembsetlist assocmembsetlist') . op add' : AssocMembSetList AssocMembSet -> AssocMembSetList . ceq add'(assocmembsetlist,assocmembset) = assocmembsetlist if contains(assocmembsetlist, assocmembset) . ceq add'(assocmembsetlist,assocmembset) = (assocmembsetlist sAssocMembSetList(assocmembset)) if not(contains(assocmembsetlist, assocmembset)) . op rm : AssocMembSetList AssocMembSet -> AssocMembSetList . eq rm(eAssocMembSetList, assocmembset) = eAssocMembSetList . ceq rm((sAssocMembSetList(assocmembset) assocmembsetlist), assocmembset') = rm(assocmembsetlist, assocmembset') if (assocmembset' == assocmembset) . ceq rm((sAssocMembSetList(assocmembset) assocmembsetlist), assocmembset') = (sAssocMembSetList(assocmembset) rm(assocmembsetlist, assocmembset')) if (assocmembset' =/= assocmembset) . op rm : AssocMembSetList AssocMembSetList -> AssocMembSetList . eq rm(assocmembsetlist, eAssocMembSetList) = assocmembsetlist . eq rm(assocmembsetlist, (sAssocMembSetList(assocmembset') assocmembsetlist')) = rm(rm(assocmembsetlist, assocmembset'), assocmembsetlist') . op subset : AssocMembSetList AssocMembSetList -> Bool . eq subset(eAssocMembSetList, assocmembsetlist') = true . eq subset((sAssocMembSetList(assocmembset) assocmembsetlist), assocmembsetlist') = contains(assocmembsetlist',assocmembset) and subset(assocmembsetlist,assocmembsetlist') . op len : AssocMembSetList -> Nat . eq len(eAssocMembSetList) = 0 . eq len(sAssocMembSetList(assocmembset) assocmembsetlist) = 1 + len(assocmembsetlist) . var i : Nat . op ith : AssocMembSetList Nat ~> AssocMembSet . eq ith((sAssocMembSetList(assocmembset) assocmembsetlist), 1) = assocmembset . eq ith((sAssocMembSetList(assocmembset) assocmembsetlist), (s i)) = ith(assocmembsetlist,i) . op index : AssocMembSetList AssocMembSet ~> Nat . ceq index((sAssocMembSetList(assocmembset) assocmembsetlist), assocmembset') = 1 if assocmembset == assocmembset' . ceq index((sAssocMembSetList(assocmembset) assocmembsetlist), assocmembset') = 1 + index(assocmembsetlist,assocmembset') if assocmembset =/= assocmembset' . op last : AssocMembSetList ~> AssocMembSet . eq last(assocmembsetlist sAssocMembSetList(assocmembset)) = assocmembset . op last : AssocMembSetList Nat ~> AssocMembSet . eq last(assocmembsetlist sAssocMembSetList(assocmembset), 1) = assocmembset . eq last(assocmembsetlist sAssocMembSetList(assocmembset), (s i)) = last(assocmembsetlist, i) . op first : AssocMembSetList ~> AssocMembSet . eq first(sAssocMembSetList(assocmembset) assocmembsetlist) = assocmembset . op next : AssocMembSetList AssocMembSet ~> AssocMembSet . ceq next(sAssocMembSetList(assocmembset) assocmembsetlist, assocmembset') = first(assocmembsetlist) if assocmembset == assocmembset' . ceq next(sAssocMembSetList(assocmembset) assocmembsetlist, assocmembset') = next(assocmembsetlist, assocmembset') if assocmembset =/= assocmembset' . op contains : AssocMembSetList KeyId -> Bool . eq contains(eAssocMembSetList, keyid') = false . eq contains((sAssocMembSetList(assocmembset) assocmembsetlist), keyid') = (keyid' == keyid(assocmembset)) or contains(assocmembsetlist, keyid') . op contains : AssocMembSetList AgentSet -> Bool . eq contains(eAssocMembSetList, memberset') = false . eq contains((sAssocMembSetList(assocmembset) assocmembsetlist), memberset') = (memberset' == memberset(assocmembset)) or contains(assocmembsetlist, memberset') . op lookup : AssocMembSetList KeyId ~> AssocMembSet . ceq lookup(sAssocMembSetList(assocmembset) assocmembsetlist, keyid') = assocmembset if keyid' == keyid(assocmembset) . ceq lookup(sAssocMembSetList(assocmembset) assocmembsetlist, keyid') = lookup(assocmembsetlist, keyid') if keyid' =/= keyid(assocmembset) . op lookup : AssocMembSetList AgentSet ~> AssocMembSet . ceq lookup(sAssocMembSetList(assocmembset) assocmembsetlist, memberset') = assocmembset if memberset' == memberset(assocmembset) . ceq lookup(sAssocMembSetList(assocmembset) assocmembsetlist, memberset') = lookup(assocmembsetlist, memberset') if memberset' =/= memberset(assocmembset) . --- GroupAssocMembSetList var group, group' : Group . sort GroupAssocMembSetList . op groupassocmembsetlist : Group AssocMembSetList -> GroupAssocMembSetList . op group : GroupAssocMembSetList -> Group . eq group(groupassocmembsetlist(group, assocmembsetlist)) = group . op assocmembsetlist : GroupAssocMembSetList -> AssocMembSetList . eq assocmembsetlist(groupassocmembsetlist(group, assocmembsetlist)) = assocmembsetlist . var groupassocmembsetlist groupassocmembsetlist' : GroupAssocMembSetList . --- GroupAssocMembSetListSet sort GroupAssocMembSetListSet . op eGroupAssocMembSetListSet : -> GroupAssocMembSetListSet . op sGroupAssocMembSetListSet : GroupAssocMembSetList -> GroupAssocMembSetListSet . op __ : GroupAssocMembSetListSet GroupAssocMembSetListSet -> GroupAssocMembSetListSet [assoc comm id: eGroupAssocMembSetListSet] . var groupassocmembsetlistset groupassocmembsetlistset' : GroupAssocMembSetListSet . op get : GroupAssocMembSetListSet Group ~> AssocMembSetList . ceq get(sGroupAssocMembSetListSet(groupassocmembsetlist) groupassocmembsetlistset, group') = assocmembsetlist(groupassocmembsetlist) if group(groupassocmembsetlist) == group' . ceq get(sGroupAssocMembSetListSet(groupassocmembsetlist) groupassocmembsetlistset, group') = get(groupassocmembsetlistset,group') if group(groupassocmembsetlist) =/= group' . op update : GroupAssocMembSetListSet Group AssocMembSetList -> GroupAssocMembSetListSet . eq update(eGroupAssocMembSetListSet, group', assocmembsetlist') = sGroupAssocMembSetListSet(groupassocmembsetlist(group', assocmembsetlist')) . ceq update(sGroupAssocMembSetListSet(groupassocmembsetlist(group,assocmembsetlist)) groupassocmembsetlistset, group', assocmembsetlist') = update(groupassocmembsetlistset,group',assocmembsetlist') if group == group' . ceq update(sGroupAssocMembSetListSet(groupassocmembsetlist(group,assocmembsetlist)) groupassocmembsetlistset, group', assocmembsetlist') = sGroupAssocMembSetListSet(groupassocmembsetlist(group,assocmembsetlist)) update(groupassocmembsetlistset,group',assocmembsetlist') if group =/= group' . op rm : GroupAssocMembSetListSet Group AssocMembSetList -> GroupAssocMembSetListSet . eq rm(eGroupAssocMembSetListSet, group', assocmembsetlist') = eGroupAssocMembSetListSet . ceq rm(sGroupAssocMembSetListSet(groupassocmembsetlist(group,assocmembsetlist)) groupassocmembsetlistset, group', assocmembsetlist') = rm(groupassocmembsetlistset,group',assocmembsetlist') if group == group' . ceq rm(sGroupAssocMembSetListSet(groupassocmembsetlist(group,assocmembsetlist)) groupassocmembsetlistset, group', assocmembsetlist') = sGroupAssocMembSetListSet(groupassocmembsetlist(group,assocmembsetlist)) rm(groupassocmembsetlistset,group',assocmembsetlist') if group =/= group' . op contains : GroupAssocMembSetListSet Group -> Bool . eq contains(eGroupAssocMembSetListSet, group') = false . eq contains((sGroupAssocMembSetListSet(groupassocmembsetlist(group,assocmembsetlist)) groupassocmembsetlistset), group') = (group' == group) or contains(groupassocmembsetlistset, group') . op add : GroupAssocMembSetListSet Group AssocMembSetList -> GroupAssocMembSetListSet . eq add(groupassocmembsetlistset, group', assocmembsetlist') = groupassocmembsetlistset sGroupAssocMembSetListSet(groupassocmembsetlist(group', assocmembsetlist')) . op add' : GroupAssocMembSetListSet Group AssocMembSetList -> GroupAssocMembSetListSet . ceq add'(groupassocmembsetlistset, group', assocmembsetlist') = groupassocmembsetlistset if contains(groupassocmembsetlistset, group') . ceq add'(groupassocmembsetlistset, group', assocmembsetlist') = add(groupassocmembsetlistset, group', assocmembsetlist') if not(contains(groupassocmembsetlistset, group')) . endfm