mod TEST is

protecting CSPREAD .
protecting CONTROLLER .

var time : Nat .
var dseq seq' seq'' : Nat .
var index newindex oldindex oldindex' transindex : Nat .
var nat nat' : Nat .
var natlist natlist' : NatList .
var natset natset' : NatSet .
var localseqs : NatSet .
var dseqs seqs : NatSet .
var proc proc' : Proc .
var member : Proc .
var procset procset' : ProcSet .
var destset destset' : ProcSet .
var everybody : ProcSet .
var members members' newmembers transmembers transmembers' : ProcSet .
var oldmembers oldmembers' : ProcSet .
var othernewmembers : ProcSet .
var comp : ProcSet .
var comps : ProcSetSet .
var conf conf' oldconf newconf transconf regconf : Conf .
var mode : Mode .
var data : Data .
var message message'  : Message .
var src dest : Proc .
var knownseqs : NatSet .
var ackedseq seq : Nat .
var transset : ProcSet .
var ackflag : Bool .
var messagelist messagelist' : MessageList .
var delivered : MessageList .
var messageset messageset' : MessageSet .
var received : MessageSet .
var constraint constraint' : Constraint .
var constraintset constraintset' : ConstraintSet .
var constraints : ConstraintSet .
var event event' : Event .
var eventlist eventlist' : EventList .
var events events' : EventList .

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

--- all processes in the network (corresponds to processors if each
--- process runs one daemon)

op allprocs : -> ProcSet .

--- initial configuration contains all processes

op initialconf : -> Conf .
eq initialconf = regconf(allprocs,0) .

--- generate initial configuration and its attributes

op  mkinitialconf : ProcSet -> State .
eq  mkinitialconf(procset) = 
    freshconf(1)
    freshseq(0)
    causalorder(initialconf,eConstraintSet)
    totalorder(initialconf,eEventList) .

--- general initial process and its attributes

op  mkinitialproc : Proc -> State .
eq  mkinitialproc(proc) =
      operational(proc)
      reachable(proc,allprocs)
      sent(proc,eBroadcastSet)
      received(proc,eMessageSet)
      acked(proc,eMessageSet)
      delivered(proc,eMessageList)
      alldelivered(proc,eMessageList)
      localconf(proc,initialconf)
      localmsgs(proc,initialconf,eNatSet)
      knownmsgs(proc,initialconf,eNatSet) .

--- generate initial processes

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

endm