fmod VIEW is

protecting BOOL .
protecting NAT .
protecting STRING .
protecting CONF .
protecting AGENT .
protecting GROUP .

var client : Agent .
var memb : Agent .
var agent agent' : Agent .
var agentlist : AgentList .
var memblist : AgentList .
var group group' : Group .
var conf : Conf .

sort View .  --- views (order irrelevant)

var view view' : View .

op view : Conf Group AgentList Nat -> View .  
op noview : -> View .

var index : Nat .

op conf : View -> Conf .
eq conf(view(conf,group,agentlist,index)) = conf .

op group : View -> Group .
eq group(view(conf,group,agentlist,index)) = group .

op members : View -> AgentList .
eq members(view(conf,group,agentlist,index)) = agentlist .

op index : View -> Nat .
eq index(view(conf,group,agentlist,index)) = index .

op rm : View Agent -> View .
eq rm(view(conf, group, memblist, index),agent) = 
   view(conf, group, rm(memblist,agent), (s index)) .

op add : View Agent -> View .
eq add(view(conf,group,memblist,index),agent) = 
   view(conf,group,add'(memblist,agent),(s index)) .

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

sort ViewSet .
op sViewSet : View -> ViewSet .
op eViewSet : -> ViewSet .
op __ : ViewSet ViewSet -> ViewSet [assoc comm id: eViewSet] .

var viewset viewset' : ViewSet .

op  contains : ViewSet View -> Bool .
eq  contains(eViewSet, view') = false .
eq  contains((sViewSet(view) viewset), view') = 
     (view' == view) or contains(viewset, view') .

op  add : ViewSet View -> ViewSet .
eq  add(viewset,view) = (viewset sViewSet(view)) .

op  add' : ViewSet View -> ViewSet .
ceq add'(viewset,view) = viewset 
    if contains(viewset, view) .
ceq add'(viewset,view) = (viewset sViewSet(view)) 
    if not(contains(viewset, view)) .

op  rm : ViewSet View -> ViewSet .
eq  rm(eViewSet,view) = eViewSet .
ceq rm((sViewSet(view) viewset),view') = rm(viewset,view')
    if (view' == view) .
ceq rm((sViewSet(view) viewset),view') = (sViewSet(view) rm(viewset,view'))
    if (view' =/= view) .

op  subset : ViewSet ViewSet -> Bool .
eq  subset(eViewSet,viewset') = true .
eq  subset((sViewSet(view) viewset), viewset') = 
    contains(viewset',view) and subset(viewset,viewset') .

op  contains : ViewSet Group -> Bool .
eq  contains(eViewSet,group') = false .
ceq contains(sViewSet(view) viewset, group') = true
    if group(view) == group' .
ceq contains(sViewSet(view) viewset, group') = contains(viewset,group')
    if group(view) =/= group' .

--- special ops for views

op  get : ViewSet Group ~> View .
ceq get(sViewSet(view) viewset, group') = view
    if group(view) == group' .
ceq get(sViewSet(view) viewset, group') = get(viewset,group')
    if group(view) =/= group' .

op  update : ViewSet Group View -> ViewSet . 
eq  update(eViewSet, group', view') =
    sViewSet(view') .
ceq update(sViewSet(view) viewset, group', view') = 
    update(viewset,group',view')
    if group(view) == group' .
ceq update(sViewSet(view) viewset, group', view') = 
    sViewSet(view) update(viewset,group',view')
    if group(view) =/= group' .

--- second argument is redundant, because
--- update(vs,g,v) only used with g = group(v)

op  rm : ViewSet Agent -> ViewSet .
eq  rm(eViewSet,agent) = eViewSet .
eq  rm(sViewSet(view) viewset,agent) =
    sViewSet(rm(view,agent)) rm(viewset,agent) .

op  rm : ViewSet Group -> ViewSet .
eq  rm(eViewSet,group) = eViewSet .
ceq rm(sViewSet(view) viewset, group) =
    rm(viewset, group)  
    if group(view) == group .
ceq rm(sViewSet(view) viewset, group) =
    sViewSet(view) rm(viewset, group)  
    if group(view) =/= group .


endfm