fmod PROC is

protecting BOOL .
protecting STRING .
protecting NATUTIL .

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

sort Proc .
op proc : String -> Proc .

var proc proc' : Proc .
var member : Proc .

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

sort ProcSet .
op sProcSet : Proc -> ProcSet .
op eProcSet : -> ProcSet .
op __ : ProcSet ProcSet -> ProcSet [assoc comm id: eProcSet] .

var procset procset' : ProcSet .

op contains : ProcSet Proc -> Bool .
eq contains(eProcSet, proc') = false .
eq contains((sProcSet(proc) procset), proc') = 
     (proc' == proc) or contains(procset, proc') .

op add : ProcSet Proc -> ProcSet .
eq add(procset,proc) = (procset sProcSet(proc)) .

op  add' : ProcSet Proc -> ProcSet .
ceq add'(procset,proc) = procset 
    if contains(procset, proc) .
ceq add'(procset,proc) = (procset sProcSet(proc)) 
    if not(contains(procset, proc)) .

op  rm : ProcSet Proc -> ProcSet .
eq  rm(eProcSet,proc) = eProcSet .
ceq rm((sProcSet(proc) procset),proc') = rm(procset,proc')
    if (proc' == proc) .
ceq rm((sProcSet(proc) procset),proc') = (sProcSet(proc) rm(procset,proc'))
    if (proc' =/= proc) .

op subset : ProcSet ProcSet -> Bool .
eq subset(eProcSet,procset') = true .
eq subset((sProcSet(proc) procset), procset') = 
    contains(procset',proc) and subset(procset,procset') .

op  inter : ProcSet ProcSet -> ProcSet .
eq  inter(eProcSet,procset') = eProcSet .
ceq inter(sProcSet(proc) procset, procset') = 
    sProcSet(proc) inter(procset,procset')
    if contains(procset',proc) .
ceq inter(sProcSet(proc) procset, procset') = 
    inter(procset,procset')
    if not(contains(procset',proc)) .

op  union : ProcSet ProcSet -> ProcSet .
eq  union(eProcSet,procset') = procset' .
ceq union(sProcSet(proc) procset, procset') = 
    sProcSet(proc) union(procset,procset')
    if not(contains(procset,proc)) and not(contains(procset',proc)) .
ceq union(sProcSet(proc) procset, procset') = 
    union(procset,procset')
    if contains(procset,proc) or contains(procset',proc) .

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

sort ProcSetSet .

op eProcSetSet : -> ProcSetSet .
op __ : ProcSetSet ProcSetSet -> ProcSetSet [assoc comm id: eProcSetSet] .

op sProcSetSet : ProcSet -> ProcSetSet .

var comp : ProcSet .
var comps : ProcSetSet .

op connected : Proc Proc ProcSetSet -> Bool .

eq connected(proc,proc',eProcSetSet) = false .
eq connected(proc,proc',(sProcSetSet(comp) comps)) =
   (contains(comp,proc) and contains(comp,proc')) or
   connected(proc,proc',comps) .
	
endfm