#include PQUEUE.cam
;--------------------------------------------------------------------
; RSC-REPOSITORY                                          PQUEUEMK/96
;--------------------------------------------------------------------
;                         Copyright@1996 by F. Luis Neves
;
; Author(s):              FLN (F. Luis Neves)
; Revisions:              22.Fev.96 Rev: 
;                                   Rev:
;
;--------------------------------------------------------------------
;
;
; Comments: Prioritary Queue Component with Multiple Key
; 
; (a) Filiation: PQUEUEMK < PQUEUE
; (b) Interface:
;                        ------------
;                       |            |
;             INIT ---> |            | DEQ:B --->
;                       |            |
;                       |  PQUEUEMK  | FRONT:B --->
;                       |            |
;         ENQ(A,B) ---> |            | EMPTY:Bool --->
;                       |            |
;                        ------------
;
; (c) State: S = A -> B-list
;     Invariant: I(st) = all(a <- dom(st) : st(a) != <>)
; (d) Model:
;
;--------------------------------------------------------------------
;

TYPE

S = A -> B-list;
A = A1:ANY A2:ANY A_:ANY;
B = ANY;

ENDTYPE

;--------------------------------------------------------------------
; Total order on A

INF(s) = let (x = choice(s))
         in MIN(x,s-{x});
MIN(x,s) = if (s == {}) then x
           else let (y = choice(s))
                in if ((A1(x) <= A1(y)) &&
				       (A2(x) <= A2(y)) &&
					   (A_(x) <= A_(y))) then MIN(x,s-{y})
                   else MIN(y,s-{x});

;--------------------------------------------------------------------
;

FUNC INIT()
STATE st <- [];

FUNC ENQ(a:A,b:B)
STATE let (x = if (a in dom(st) -> st[a]) otherwise (<>))
      in st <- st + [a -> (x ^ <b>)];

FUNC FRONT():B
PRE st != []
RETURN let (m = INF(dom(st)))
       in hd(st[m]);

FUNC DEQ():B
PRE st != []
STATE let (m = INF(dom(st)), x = tl(st[m]), b = hd(st[m]))
      in progn(st <- if (x == <> -> st\{m}) otherwise (st + [m -> x]),b);

FUNC EMPTY(): Bool
RETURN st == [];