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

withdraw(Amt,Acct) :- o((Amt > 0) * bal(Acct,B1) * (Amt < B1) *
                          del(bal(Acct,B1)) * (B2 is B1-Amt) *
                          ins(bal(Acct,B2)) * monitor(withdraw(Amt,Acct))).

deposit(Amt,Acct) :- o((Amt > 0) * del(bal(Acct,B1)) * (B2 is B1+Amt) *
                         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) :- o1(transfer(Amt,acct1,acct2) # transfer(Amt,acct1,acct3) # 
             transfer(Amt,acct1,acct4)).

test1(Amt) :- o1(transfer(Amt,acct1,acct2) # transfer(Amt,acct1,acct3)).