
% The following program is based on Example 6 of my DBPL'97 paper.
% Since withdraw and deposit commute, conc0 is used instead of conc.
% This eliminates needless backtracking in case of failure.
%
trans(transfer(Amt,Acct1,Acct2)) :- isolate(conc0(withdraw(Amt,Acct1),
                                                  deposit(Amt,Acct2))).

trans(withdraw(Amt,Acct)) :- isolate(seq(Amt > 0,
                                      seq(bal(Acct,B1),
                                       seq(Amt < B1,
                                        seq(del(bal(Acct,B1)),
                                         seq(B2 is B1-Amt,
                                          seq(ins(bal(Acct,B2)),
                                               monitor(withdraw(Amt,Acct))))))))).

trans(deposit(Amt,Acct)) :- isolate(seq(Amt > 0,
                                     seq(del(bal(Acct,B1)),
                                      seq(B2 is B1+Amt,
                                       seq(ins(bal(Acct,B2)),
                                            monitor(deposit(Amt,Acct))))))).


% Set up some accounts.
%
init :- ins(bal(acct1,100)), ins(bal(acct2,100)), ins(bal(acct3,100)),
        ins(bal(acct4,100)), ins(bal(acct5,100)), ins(bal(acct6,100)).


% Test the above program, by removing an amount, Amt, from account %
% acct1 three times.  Since the transfer transaction commutes with
% itself, conc0 is used instead of conc.  This prevents needless
% backtracking; ie, if one interleaving of the transfers fail, then they
% all will.  Execute test(40) to see.
%
test(Amt) :-  execute(conc0(transfer(Amt,acct1,acct2),
                       conc0(transfer(Amt,acct1,acct3),
                              transfer(Amt,acct1,acct4)))).


% Declare bal/2 to be a base predicate.
%
bal(X,Y) :- db(bal(X,Y)).


% The following dummy rules tell Prolog that certain predicates are defined.
%
transfer(dummy,dummy,dummy) :- fail.
withdraw(dummy,dummy) :- fail.
deposit(dummy,dummy) :- fail.
