fmod CAPI is

--- Spread configuration layer API (internal API)
--- used by group layer

protecting CMESSAGE .
including STATE .

------------------------------------------------------
---  configuration layer interface towards upper layer
------------------------------------------------------

--- this is the general format of a procedure call

op multicast-req : Proc Mode Data -> State . --- multicast request from upper layer
op multicast-ack : Proc -> State .  --- multicast ack to upper layer

--- the following state components are accessed directly by the upper layer
--- and therefore we include them as part of the API:

--- each process is part of a configuration
op localconf : Proc Conf -> State . 

--- messages delivered to upper layer (order essential)
op delivered : Proc MessageList -> State .  

--- history of all delivered messages
op alldelivered : Proc MessageList -> State .  

--- "delivered" is part of local state and simulataneously 
--- part of the API (the upper layer can simply take
--- messages out of the "delivered" buffer).
--- It would be more uniform to have a receive-req/receive-ack
--- pair of procedure calls, but this seems less convenient.

----------------------------------------------------
--- configuration layer interface towards controller
----------------------------------------------------

--- the following state compoments are only used to have a fine
--- control over the execution and to generate specific scenarios

--- some rules are controlled by action tokens

op SEND : Proc Nat -> Action . --- send token
op RECEIVE : Proc Nat -> Action . --- receive token
op LOSE : Proc Nat -> Action . --- loss token
op CHANGE : Proc ProcSet -> Action .     --- configuration change token
op EVS-START : Proc Bool -> Action .     --- evs algorithm trigger token (active)
op EVS-START' : Proc Bool -> Action .     --- evs algorithm trigger token (passive)
op CFAIL : Proc -> Action . --- process failure (only configuration layer)
op CRECOVER : Proc -> Action . --- process recovery (only configuration layer)

endfm