#include FFUN.cam
;--------------------------------------------------------------------
; RSC-REPOSITORY                                            PQUEUE/96
;--------------------------------------------------------------------
;                         Copyright@1996 by F. Luis Neves
;
; Author(s):              JNO (Jose N. Oliveira), FLN (F. Luis Neves)
; Revisions:              22.Fev.96 Rev: 
;                                   Rev:
;
;--------------------------------------------------------------------
;
;
; Comments: Prioritary Queue Component
; 
; (a) Filiation: PQUEUE < FFUN
; (b) Interface:
;                        ------------
;                       |            |
;             INIT ---> |            | DEQ:B --->
;                       |            |
;                       |   PQUEUE   | FRONT:B --->
;                       |            |
;         ENQ(A,B) ---> |            | EMPTY:Bool --->
;                       |            |
;                        ------------
;
; (c) State:

STATE st: NAT->B-seq;

;     Invariant: I(S) = all(a <- dom(S) : S(a) != <>)

; (d) Model:
;
;--------------------------------------------------------------------
;

INF(s)=min-orio(32767,s);

FUNC ENQ(a:NAT,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 != []
let (m = INF(dom(st)), x = tl(st[m]), b = hd(st[m]))
in RETURN b
   STATE st <- if (x == <> -> st\{m}) otherwise (st + [m -> x]);