; ***  ENROLLMENT CONTROL SYSTEM  ***
; Module: ENROLLSYS.CAM      92.10.27           jj 95.11.23

; -------------------------------------------------------------------- 
; 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
  DB = CId -> Course;
  Course = SId -> Inf;
  Inf = [Mark];
  WaitQ = Mess-list;
ENDTYPE

; STATE  C : Course

; -------------------------------------------------------------------- 
; Events
; -------------------------------------------------------------------- 

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

FUNC DefineCourse (c:CId) :
PRE  c notin dom(C)
STATE C <- C + [c -> []];


FUNC InsStu (n:SId,c:CId) :
PRE  (c in dom(C)) /\ (n notin dom(C[c]))
STATE  C <-  C + [c -> (C[c] + [n -> nil])];


FUNC InsMark (n:SId,c:CId,p:Mark) :
PRE  (c in dom(C)) /\ (n in dom(C[c]))
STATE  C <-  C + [c -> (C[c] + [n -> p])];


FUNC RemStu (n:SId,c:CId) :
PRE  (c in dom(C)) /\ (n in dom(C[c]))
STATE  C <-  C + [c -> C[c]\{n} ];


; -------------------------------------------------------------------- 
; Functions
; -------------------------------------------------------------------- 

FUNC Vacancies (c:CId) : INT
PRE  c in dom(C)
RETURNS  50 .- #(dom(C[c]));


FUNC PosMark (c:CId) : SId-set 
PRE  (c in dom(C)) /\ (all(x <- dom(C[c]) : is-Mark(C[c][x])))
RETURNS  { x | x <- dom(C[c]) : C[c][x] >= 10};


FUNC DidBetter (m:Mark,c:CId) : SId-set 
PRE  (c in dom(C)) /\ (all(x <- dom(C[c]) : is-Mark(C[c][x])))  
           -> "Sorry: Marks not yet available"   
RETURNS  { x | x <- dom(C[c]) : C[c][x] >= m};


FUNC MinMark (c:CId) : SId-set
PRE  (c in dom(C)) /\ (all(x <- dom(C[c]) : is-Mark(C[c][x])))   
RETURNS  let (mc = min-orio(999,ran(C[c])))
         in  {x | x <- dom(C[c]) : C[c][x] == mc};

; -------------------------------------------------------------------- 
; Communications Service
; -------------------------------------------------------------------- 

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

FUNC proc () : STR
RETURNS  let ( r = send(bf,Mess("ready","es"," ")))
         in   proc1(nil);

FUNC proc1 (rp:WaitQ) : STR
RETURNS  let ( x = receive(es) )
         in  if (T(x)=="end" -> SendReplies(rp),
                 is-iM(T(x)) -> let (y = InsStu(N(T(x)),Co(T(x))))
                                in proc1(rp),
                 is-CId(T(x))-> let (v = Vacancies(T(x)),
                                    y = <Mess(v,"es",O(x)):rp> )
                                in proc1(y)
                 else        -> proc1(rp);

FUNC SendReplies (rp:WaitQ) : SRT
RETURNS  if (rp == nil)
         then "No more messages"
         else  let  (x = send(bf,hd(rp)))
               in  SendReplies(tl(rp));

; -------------------------------------------------------------------- 
; Tests
; -------------------------------------------------------------------- 
Init();
DefineCourse("logic");
DefineCourse("specs");
InsStu("anne","logic");
InsStu("mary","specs");
InsStu("anne","specs");
InsStu("peter","specs");
InsStu("john","logic");
InsStu("john","specs");
InsStu("martha","logic");
InsStu("paul","logic");
InsMark("anne","logic",12);
InsMark("john","logic",7);
InsMark("martha","logic",10);
InsMark("paul","logic",17);