MODEL CoursePlan


TYPE
  Plan = Course-set

  inv(p) = let  ( coll = lambda(x) . if (is-Mandatory(x) -> Ym(x),
                                         is-Optional(x)  -> Yo(x) ) )
           in exist( x <- {1,2,3,4,5,6} : coll-set(p) == inseg(x) );

  Course = Mandatory | Optional;

  Mandatory = Ym : Year  
              Am : Area
              Nm : Name;
              
  Optional = Yo : Year
             Io : Idf
             Ops : Option-set;

  Option =  Ao : Area
            No : Name;

  Year = INT;
  Area = STR;
  Name = STR;
  Idf = INT;

ENDTYPE

STATE P:Plan;
 invariant() = inv_Plan(P);

FUNC f()
RETURN if (x is-<> -> true,
           x is-<a:b> -> <a>);

FUNC InsMC (y:Year, a:Area, n:Name) :
; inserts a new (mandatory) course
STATE  P <- P U {Mandatory(y,a,n)};

FUNC InsOC (y:Year, i:Idf, o:Option-set) :
; inserts a new (optional) course
STATE  P <- P U {Optional(y,i,o)};

FUNC Courses () : Name-set
; computes the set of courses offered (either optional or mandatory)
RETURNS  let ( m = {c | c <- P : is-Mandatory(c)},
               o = P-m )
         in  Nm-set(m) U UNION({No-set(Ops(c)) | c <- o});

FUNC OptionalAreas () : Area-set
; computes the curricular areas only involved in optional areas
RETURNS  let ( m = {c | c <- P : is-Mandatory(c)},
               o = P-m )
         in UNION({Ao-set(Ops(c)) | c <- o}) - Am-set(m);


ENDMODEL

; test
c1 <- Mandatory(1,"Logic","Set Theory");
c2 <- Mandatory(2,"Logic","Categorial Logic");
c3 <- Mandatory(1,"Computation","Functional Programming");

o1 <- Optional(2,1,{Option("Hardware","Digital Design I"), Option("Logic","Proof Theory")});
o2 <- Optional(3,2,{Option("Hardware","Digital Design II"), Option("Logic","Graph Theory"),
                    Option("Computation","Data Minning")});

P <- {c1,c2,c3,o1,o2};