#include FDEP.cam

; Creation date: Fri Dec 12 10:56:59 WET 1997

;STATE st   : AccId->(AccHolder-set)*NAT;

FUNC Init(): VOID
RETURN st <- [];

FUNC AddAccHolders(a: AccId, b: AccHolder-set): VOID
STATE st    <- st    + let (f=lambda(x).< p1(x) U b, p2(x) >)
                     in (*->f)(st   /{a});

FUNC OpenAccount(a: AccId, b: AccHolder-set, c: C): VOID
STATE  st <- [ a -> < b,c > ] + st ;

FUNC Credit(a: AccId, b: NAT): VOID
STATE  st    <- st    + let (f=lambda(x).< p1(x), p2(x) .+ b >)
                        in (*->f)(st   /{a});

FUNC  Withdraw(a: AccId, b: NAT): VOID
STATE  st    <- st    + let (f=lambda(x).
                               let (c=p2(x),
                                    d= if c >= b then c .- b else c)
                               in < p1(x), c >)
                        in (*->f)(st   /{a});

FUNC GoodCostumers(a: NAT): AccHolder-set
RETURN UNION( { p1(st   [k]) | k <- dom(st   ): p2(st   [k]) >= a });