#include BREL.cam
;--------------------------------------------------------------------
; RSC-REPOSITORY                                             ORDER/96
;--------------------------------------------------------------------
;                         Copyright@1996 by F. Luis Neves
;
; Author(s):              JNO (Jose N. Oliveira), FLN (F. Luis Neves)
; Revisions:              22.Mar.96 Rev: 
;                                   Rev:
;
;--------------------------------------------------------------------
;
;
; Comments: Binary Relation over a Set Component
; 
; (a) Filiation: ORDER < BREL
; (b) Interface:
;                        -----------
;                       |           | <--- SCLOSE
;             INIT ---> |           | 
;                       |           | <--- TCLOSE
;          REMR(A) ---> |           |
;                       |           | GET:AxA ---> 
;          REML(B) ---> |   ORDER   | 
;                       |           | SELR(A):B-set --->
;         INS(A,B) ---> |           | 
;                       |           | SELL(B):A-set --->
;           RCLOSE ---> |           |
;                       |           |
;                        -----------
;
; (c) State: S = A<->A
; (d) Model:
;
;--------------------------------------------------------------------
;

TYPE

S = A<->A;
A = ANY;

ENDTYPE

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

FUNC RCLOSE()
STATE let (x=p1-set(st) U p2-set(st))
      in st <- st U { < a,a > | a <- x };

FUNC SCLOSE()
STATE st <- st U { < p2(t),p1(t) > | t <- st };

FUNC TCLOSE()
STATE let (tc=lambda(r).
           let (s= { <p1(t),p2(u)> | t <- r, u <- r: p2(t)==p1(u)})
           in if subset(s,r) then r else tc(r U s) )
      in st <- tc(st);