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

      TYPE
       
        StockDb = Ref -> Comp;
        Comp =  D : Des
	        Q : Qty
	        A : Alv
	        T : Typ;
        Ref = SYM;
        Des = SYM; 
        Qty = INT;
        Alv = INT;
        Typ = Ref-set;

        RefList = Ref-list;

        ProdPlan = Ref -> INT;
        ToBuy  = Ref -> INT;

      ENDTYPE

; ---------- STATE ----------------------------------------------------

; stk : StockDb


; ---------- EVENTS ---------------------------------------------------


    FUNC reset() : 
    STATE stk <- []; 

    FUNC insComp(r:Ref,i:Comp) : 
    PRE  not(r in dom(stk))  -> "ERROR: Reference Registered"
    STATE stk <- stk + [r -> i];

    FUNC remComp(r:Ref) : 
    PRE  r in dom(stk)  -> "ERROR: Reference Unknown"
    STATE stk <- stk + [r -> i];

    FUNC updateComp(r:Ref,q:Qty) : 
    PRE  r in dom(stk)  -> "ERROR: Reference Unknown"
    STATE  let  (c = stk[r])
           in   stk <- stk + [r -> Comp(D(c),q,A(c),T(c))];

    FUNC QueryRef(r:Ref) : Comp 
    PRE  r in dom(stk)  -> "ERROR: Reference Unknown"
    RETURN  stk[r];

    FUNC List() : Ref-set 
    RETURN  dom(stk);

    FUNC AlarmList() : Ref-set 
    RETURN  { r | r <- dom(stk) : Q(stk[r]) <= A(stk[r])};

    FUNC Explode(r:Ref) : Ref-set 
    PRE  r in dom(stk)  -> "ERROR: Reference Unknown"
    RETURN  explode(r,stk);

    FUNC UsedIn(r:Ref) : Ref-set 
    PRE  r in dom(stk)  -> "ERROR: Reference Unknown"
    RETURN  { x | x <- dom(stk) : r in T(stk[x]) };

    FUNC CanMake(r:Ref) : INT
    PRE  (r in dom(stk)) && consistent(stk)
    RETURN  CMk(r,stk);


; ---------- FUNCTIONS ------------------------------------------------  


    FUNC CMk(r:Ref,s:StockDb) : INT
    RETURN  let  (needs = T(s[r]))
            in   if needs=={}
                 then 0
                 else let ( hip = permutations(< c | c <- needs>),
                            imd = minimum({ Q(s[c]) | c <- needs}) )
                      in  maximum({minimum(Simulate(h,s)) | h <- hip} U
                                  {imd});
    FUNC Simulate(n:Ref-list,s:StockDb) : INT-set
    RETURN  if n==<> 
            then {}
            else let ( c = hd(n),
                       m = CMk(c,s),
                       ns = (s + [c -> NewQt(c,0,s)])
                               + [e -> NewQt(e,m,s) | e <- T(s[c])]) 
                 in  { add(Q(s[c]),m)} U Simulate(tl(n),ns);

    FUNC  NewQt(c:Ref,n:Qty,s:StockDb) : Comp
    RETURN  Comp(D(s[c]),n,A(s[c]),T(s[c]));

    FUNC  explode(r:Ref,s:StockDb) : Ref-set
    RETURN  {r} U UNION({explode(x,s) | x <- T(s[r])});

    FUNC  consistent(s:StockDb) : Bool
    RETURN  let (rfs = UNION ({T(s[x]) | x <- dom(s)}))
            in  subset(rfs,dom(s));

    FUNC minimum(v:INT-set) : INT
    RETURN  reduce(9999,smallest,v);

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

    FUNC maximum(v:INT-set) : INT
    RETURN  reduce(0,greatest,v);

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

    FUNC permutations(l:Ref-list) : RefList-set
    RETURN   { p | p <- perm(l,length(l)) : length(p)==length(l) };
            
    FUNC perm(l:Ref-list,n:INT) : RefList-set
    RETURN   if n==0 then {<>}
             else  let ( x = hd(l),
                         pr = permutations(rest(l,x)))
                   in  { <x:k> |  k <- pr } U perm(tail(l)^<x>,sub(n,1));

    rest(l,x) = if l==<> then <>
                else (if x==hd(l) then tail(l)
                      else <hd(l):rest(tail(l),x)>);