#include RSC.cam
;--------------------------------------------------------------------
; RSC-REPOSITORY                                              FSET/96
;--------------------------------------------------------------------
;                         Copyright@1996 by F. Luis Neves
;
; Author(s):              JNO (Jose N. Oliveira), FLN (F. Luis Neves)
; Revisions:              21.Mar.96 Rev: 
;                                   Rev:
;
;--------------------------------------------------------------------
;
;
; Comments: Finite Set Component
; 
; (a) Filiation: FSET < RSC
; (b) Interface:
;                        ------------
;                       |            |
;             INIT ---> |            | TEST(A):Bool --->
;                       |            |
;           INS(A) ---> |    FSET    |
;                       |            |
;            <--- GET:A |            | <--- REM(A)
;                       |            |
;                        ------------
;
; (c) State:

STATE st: A-set;

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

FUNC INIT()
STATE st <- {};

FUNC EMPTY()
RETURN st == {};

FUNC INS(a:A)
STATE st <- st U {a};

FUNC TEST(a:A):Bool
RETURN a in st;

FUNC REM(a:A)
STATE st <- st - {a};

FUNC GET():A
PRE st != {}
let (a = choice(st))
in RETURN a
   STATE st <- st - {choice(st)};