; ***  ENROLLMENT CONTROL SYSTEM ***
; Module: SERVER.CAM        92.10.27

; -------------------------------------------------------------------- 
; Sorts
; -------------------------------------------------------------------- 

TYPE
; Shared Types
  Mess = T:Mtype O:PId D:PId;
  Mtype = STR | INT | iM | mM | CId | pM;
  iM = N:SId Co:CId;
  mM = N:SId Co:CId M:Mark;
  pM = M:Mark Co:CId;
  PId = STR;
  CId = STR;
  SId = STR;
  Mark = INT;
; Private Types
  Buffers = PId -> Mess-list;
ENDTYPE

; STATE  B:Buffers


; -------------------------------------------------------------------- 
; Communication Service
; -------------------------------------------------------------------- 


FUNC Init () :
STATE B <- [];

FUNC EndSession () : STR
STATE let (x = rmchannel(ip1),
           x = rmchannel(ip2),
           x = rmchannel(es),
           x = rmchannel(bf) )
       in B <- []
RETURNS "Session is over. (Uff!)";

FUNC DefineModule (p:PId) :
PRE  p notin dom(P)
STATE B <- B + [p -> nil];


FUNC serv() : 
STATE let ( m = receive(bf) )
      in  if (T(m) == "ready")
          then  B <- reply(O(m),B)
          else  B <- update(B,m,D(m))
RETURNS serv();

FUNC update(b:Buffers,m:Mess,d:PId) : Buffers
PRE  d in dom(b)
RETURNS  b + [d -> b[d] ^ <m>];

FUNC reply(p:PId,b:Buffers) : Buffers
PRE  p in dom(b)
RETURNS  if (b[p] == nil)
         then  (let  (x = send(conv(p),Mess("end"," "," ")))
               in b)
         else (let  (x = send(conv(p),hd(b[p])))
               in  reply(p,b + [p -> tl(b[p])]));

FUNC conv (p:STR) : CHAN
; This function becomes necessary as a value of type CHAN cannot be
; part of a message processed by the send or receive primitives.
RETURNS  if (p == "es") then es
         else if (p == "ip1") then ip1 else ip2;



; Initialization

bf <- channel("bf");
ip1 <- channel("ip1");
ip2 <- channel("ip2");
es <- channel("es");

Init();
DefineModule("es");
DefineModule("ip1");
DefineModule("ip2");