#include FSET.cam
;--------------------------------------------------------------------
; RSC-REPOSITORY                                              BREL/96
;--------------------------------------------------------------------
;                         Copyright@1996 by F. Luis Neves
;
; Author(s):              JNO (Jose N. Oliveira), FLN (F. Luis Neves)
; Revisions:              21.Mar.96 Rev: 
;                                   Rev:
;
;--------------------------------------------------------------------
;
;
; Comments: Binary Relation Component
; 
; (a) Filiation: BREL < FSET
; (b) Interface:
;                        ------------
;             INIT ---> |            |
;                       |            | GET:AxB --->     
;          REMR(A) ---> |            |
;                       |    BREL    | SELR(A):B-set --->
;          REML(B) ---> |            |
;                       |            | SELL(B):A-set --->
;         INS(A,B) ---> |            |
;                        ------------
;
; (c) State:

STATE st: A <-> B;

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

FUNC SELR(a:A)
RETURN { p2(t) | t <- st : p1(t)==a };

FUNC SELL(b:B)
RETURN { p1(t) | t <- st : p2(t)==b };

FUNC REMR(a:A)
STATE st <- { t | t <- st: p1(t)!= a };

FUNC REML(b:B)
STATE st <- { t | t <- st: p2(t)!= b };