; ENROLLMENT CONTROL SYSTEM
; version 2       

MODEL ECS

; -------------------------------------------------------------------- 
; SORTS
; -------------------------------------------------------------------- 

TYPE
  DB = CId -> Course;
  Course = SId -> Inf;
  CId = STR;
  SId = STR;
  Inf = [Mark];
  Mark = INT;
ENDTYPE

STATE  C:DB;

; -------------------------------------------------------------------- 
; 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 = m-orio(999,ran(C[c])))
         in  {x | x <- dom(C[c]) : C[c][x] == mc};

m(a,b) = if (a<b) then a else b;

ENDMODEL
; -------------------------------------------------------------------- 
; TESTES
; -------------------------------------------------------------------- 
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);