fmod AGENT is

protecting BOOL .
protecting STRING .
protecting NATUTIL .

--- the following sort and op declarations are common to spread and cliques

sort Agent .   --- agents (we identify an agent with its private group)
op agent : String -> Agent . 

var agent agent' : Agent .

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

sort AgentList .
op eAgentList : -> AgentList .
op sAgentList : Agent -> AgentList .
op __ : AgentList AgentList -> AgentList [assoc id: eAgentList] .

var agentlist agentlist' : AgentList .

op contains : AgentList Agent -> Bool .
eq contains(eAgentList, agent') = false .
eq contains((sAgentList(agent) agentlist), agent') = 
     (agent' == agent) or contains(agentlist, agent') .
     
op  contains : AgentList AgentList -> Bool .
eq  contains(agentlist, eAgentList) = false .
eq  contains(agentlist, (sAgentList(agent') agentlist')) = 
      contains(agentlist, agent') or contains(agentlist, agentlist') .     
 
op add : AgentList Agent -> AgentList .
eq add(agentlist,agent) = (agentlist sAgentList(agent)) .

op  add : AgentList AgentList -> AgentList .
eq  add(agentlist,agentlist') = (agentlist agentlist') .

op  add' : AgentList Agent -> AgentList .
ceq add'(agentlist,agent) = agentlist 
    if contains(agentlist, agent) .
ceq add'(agentlist,agent) = (agentlist sAgentList(agent)) 
    if not(contains(agentlist, agent)) .  
     
op  rm : AgentList Agent -> AgentList .
eq  rm(eAgentList,agent) = eAgentList .
ceq rm((sAgentList(agent) agentlist),agent') = rm(agentlist,agent')
    if (agent' == agent) .
ceq rm((sAgentList(agent) agentlist),agent') = (sAgentList(agent) rm(agentlist,agent'))
    if (agent' =/= agent) .

op  rm : AgentList AgentList -> AgentList .
eq  rm(agentlist, eAgentList) = agentlist .
eq  rm(agentlist, (sAgentList(agent') agentlist')) = 
    rm(rm(agentlist, agent'), agentlist') .
    
op  subset : AgentList AgentList -> Bool .
eq  subset(eAgentList,agentlist') = true .
eq  subset((sAgentList(agent) agentlist), agentlist') = 
     contains(agentlist',agent) and subset(agentlist,agentlist') .

op  len : AgentList -> Nat .
eq  len(eAgentList) = 0 .
eq  len(sAgentList(agent) agentlist) = 1 + len(agentlist) .

var i : Nat .
op  ith : AgentList Nat ~> Agent .
eq  ith((sAgentList(agent) agentlist), 1) = agent .
eq  ith((sAgentList(agent) agentlist), (s i)) = ith(agentlist,i) .

op  index : AgentList Agent ~> Nat .
ceq index((sAgentList(agent) agentlist), agent') = 1 
    if agent == agent' .
ceq index((sAgentList(agent) agentlist), agent') = 1 + index(agentlist,agent') 
    if agent =/= agent' .

op  last : AgentList ~> Agent .
eq  last(agentlist sAgentList(agent)) = agent .

op  last : AgentList Nat ~> Agent .
eq  last(agentlist sAgentList(agent), 1) = agent .
eq  last(agentlist sAgentList(agent), (s i)) = last(agentlist, i) .

op  first : AgentList ~> Agent .
eq  first(sAgentList(agent) agentlist) = agent .

op  next : AgentList Agent ~> Agent .
ceq next(sAgentList(agent) agentlist, agent') = first(agentlist)
    if agent == agent' .
ceq next(sAgentList(agent) agentlist, agent') = next(agentlist, agent')
    if agent =/= agent' .

---------------------------    
    
sort AgentSet .
op eAgentSet : -> AgentSet .
op sAgentSet : Agent -> AgentSet .
op __ : AgentSet AgentSet -> AgentSet [assoc comm id: eAgentSet] .
    
var agentset agentset' : AgentSet .

op contains : AgentSet Agent -> Bool .
eq contains(eAgentSet, agent') = false .
eq contains((sAgentSet(agent) agentset), agent') = 
     (agent' == agent) or contains(agentset, agent') .

op  inter : AgentSet AgentSet -> AgentSet .
eq  inter(eAgentSet,agentset') = eAgentSet .
ceq inter(sAgentSet(agent) agentset, agentset') = 
    sAgentSet(agent) inter(agentset,agentset')
    if contains(agentset',agent) .
ceq inter(sAgentSet(agent) agentset, agentset') = 
    inter(agentset,agentset')
    if not(contains(agentset',agent)) .

op  add : AgentSet Agent -> AgentSet .
eq  add(agentset,agent) = (agentset sAgentSet(agent)) .

op  add : AgentSet AgentSet -> AgentSet .
eq  add(agentset,agentset') = (agentset agentset') .

op  add' : AgentSet Agent -> AgentSet .
ceq add'(agentset,agent) = agentset 
    if contains(agentset, agent) .
ceq add'(agentset,agent) = (agentset sAgentSet(agent)) 
    if not(contains(agentset, agent)) .

op  rm : AgentSet Agent -> AgentSet .
eq  rm(eAgentSet,agent) = eAgentSet .
ceq rm((sAgentSet(agent) agentset),agent') = rm(agentset,agent')
    if (agent' == agent) .
ceq rm((sAgentSet(agent) agentset),agent') = (sAgentSet(agent) rm(agentset,agent'))
    if (agent' =/= agent) .

op  rm : AgentSet AgentSet -> AgentSet .
eq  rm(agentset, eAgentSet) = agentset .
eq  rm(agentset, (sAgentSet(agent') agentset')) = 
    rm(rm(agentset, agent'), agentset') .

op  subset : AgentSet AgentSet -> Bool .
eq  subset(eAgentSet,agentset') = true .
eq  subset((sAgentSet(agent) agentset), agentset') = 
    contains(agentset',agent) and subset(agentset,agentset') .
   
op agentset : AgentList -> AgentSet .
eq agentset(eAgentList) = eAgentSet .
eq agentset(sAgentList(agent) agentlist) = sAgentSet(agent) agentset(agentlist) .

op card : AgentSet -> Nat .
eq card(eAgentSet) = 0 .
eq card(sAgentSet(agent) agentset) = card(agentset) + 1 .
   
endfm