fmod GTEST is

protecting TEST .
protecting SPREAD .

var proc : Proc .
var procset procset' : ProcSet .

op  mkinitialgproc : Proc -> State .
eq  mkinitialgproc(proc) =
      glocalconf(proc,initialconf) 
      gview(proc,eViewSet)
      gjoined(proc,eGroupList) 
      gdelivered(proc,eGMessageList) .

op  mkinitialgproc' : Proc -> State .
eq  mkinitialgproc'(proc) =
      goperational(proc) .

op  mkinitialgprocs : ProcSet -> State .
eq  mkinitialgprocs(eProcSet) = eState .
eq  mkinitialgprocs(sProcSet(proc)) = mkinitialgproc(proc) .
ceq mkinitialgprocs(procset procset') = 
    mkinitialgprocs(procset) mkinitialgprocs(procset')
    if procset =/= eProcSet and procset' =/= eProcSet .

op  mkinitialgprocs' : ProcSet -> State .
eq  mkinitialgprocs'(eProcSet) = eState .
eq  mkinitialgprocs'(sProcSet(proc)) = mkinitialgproc'(proc) .
ceq mkinitialgprocs'(procset procset') = 
    mkinitialgprocs'(procset) mkinitialgprocs'(procset')
    if procset =/= eProcSet and procset' =/= eProcSet .

op mkinitialagents : ProcSet -> State .

eq mkinitialagents(procset) =
    gclients(eAgentList) --- all clients are disconnected
    gstate(mkinitialgprocs'(procset),eState,eState,eState) --- but the group layer is active on each process
    mkinitialgprocs(procset) .

endfm