fmod CCOMMON is

including PROC .
including MODE .
including CONF .
including CMESSAGE .
including CONSTRAINTS .
including STATE .
including CAPI .

--------------------------------------------
--- local state of the configuration layer
--------------------------------------------

op network : ProcSet -> State .  --- processes in the network
op freshconf : Nat -> State .  --- fresh index to create new configurations

op reachable : Proc ProcSet -> State .  --- connectivity as observed from a process

op operational : Proc -> State .  --- state of regular operation

op failed : Proc -> State .  --- node failure

--- states of evs algorithm (see change.maude of comments)
--- invoked after configuration change

op evs-start : Proc ProcSet Bool -> State .
op evs-start' : Proc ProcSet ProcSet Bool -> State .
op evs-start'' : Proc ProcSet ProcSet Bool -> State .
op evs-start''' : Proc ProcSet Bool -> State .
op evs-collect : Proc ProcSet ProcSet Bool -> State .
op evs-collect' : Proc ProcSet ProcSet Bool -> State .
op evs-deliver : Proc ProcSet ProcSet Bool -> State .
op evs-trans : Proc ProcSet ProcSet Bool -> State .
op evs-trans' : Proc ProcSet ProcSet Bool -> State .
op evs-trans-deliver : Proc ProcSet ProcSet Bool -> State .
op evs-reg : Proc ProcSet Bool -> State .
op evs-reg' : Proc ProcSet Bool -> State .

--- broadcasts sent (i.e. in output buffer)
op sent : Proc BroadcastSet -> State .    
--- messages received (i.e. in input buffer)
op received : Proc MessageSet -> State .  

--- messages received and acknowledged by myself
op acked : Proc MessageSet -> State .

--- sequence numbers locally generated (essential for fifo constraints)
op localmsgs : Proc Conf NatSet -> State .  
--- sequence numbers known to process (essential for causality constraints)
op knownmsgs : Proc Conf NatSet -> State .  

--- sequence number shared by all members of a configuration
op freshseq : Nat -> State .  

--- causal order and total order constaints to be enforced
--- for the delivery of messages

op causalorder : Conf ConstraintSet -> State .
op totalorder : Conf EventList -> State .

--- the eventlist in total order is just a trace of all
--- delivery events in a configuration

endfm