Karl/Michael's Money Transfer Usecase ===================================== 1. Perform money transfer from Buyer's Bank to Seller's Bank through Broker. Involves two transfers: cost of good to Seller, then transaction fee to Broker. The process modeling part in Transaction Logic: %% Parallel (interleaved) transfer purchaseViaBroker(PurchAmt,Fee,BuyerAcct,SellerAcct,BrokerAcct) :- transfer(PurchAmt,BuyerAcct,SellerAcct) | transfer(Fee,BuyerAcct,BrokerAcct). %% Sequential transfer (alternative) purchaseViaBroker(PurchAmt,Fee,BuyerAcct,SellerAcct,BrokerAcct) :- transfer(PurchAmt,BuyerAcct,SellerAcct), transfer(Fee,BuyerAcct,BrokerAcct). transfer(Amount,Account1,Account2) :- withdraw(Amount,Account1), deposit(Amount,Account2). withdraw(Amount,Account):- balance(Account,Balance), Balance >= Amount, change_balance(Account,Balance,Balance-Amount). deposit(Amount,Account) :- balance(Account,Balance), Amount >= 0, change_balance(Account,Balance,Balance+Amount). change_balance(Account,Balance1,Balance2) :- btdelete{balance(Account,Balance1)}, btinsert{balance(Account,Balance2)}. - Two transfers of X and Y are equivalent to one transfer of X+Y (between same accounts). But the fee is double. Can be specified as in the FLOWS proposal: create a new transaction, doubleTransfer and define its fee to be the sum of the fees of the individual transfers. However, I think this representation misses the point. What about triple transfers? Another definition? It should be possible to *prove* the desired properties from basic process specifications. Indeed, in Transaction Logic one can prove that: balance(buyer,Balance), NewBalance = Balance - Fee1 - Fee2 - PurchAmt1 - PurchAmt2, purchaseViaBroker(PurchAmt1,Fee1,BuyerAcct, SellerAcct1,BrokerAcct1), purchaseViaBroker(PurchAmt2,Fee2,BuyerAcct, SellerAcct2,BrokerAcct2) -> purchaseViaBroker(PurchAmt1,Fee1,BuyerAcct, SellerAcct1,BrokerAcct1), purchaseViaBroker(PurchAmt2,Fee2,BuyerAcct, SellerAcct2,BrokerAcct2), balance(buyer,NewBalance) 2. In reality, the above broker service is better represented as an object, which has data and can perform operations. Will address several additional issues from Karl's example - to illustrate the complexity of the modeling task: - This service is a financial operation - This service doesn't do international transfers - If Broker's fee is paid within X days, Buyer gets Y% discount. - If money aren't transfered within specified amt of time of the fee payment date, give additional discount. - If both transfers are executed the trade is complete (this is guaranteed by the semantics of Transaction Logic) - Unless Buyers address is known to the bank the transfer will not be executed - After the transfer is initiated the bank sends an acknowledgement message, which is a legally binding document - Buyer & Seller can trade in currency C - Buyer wants to pay the Seller before paying the Broker. The example is using the FLORA-2 syntax: discountTransfer : financialOperation. transferServ123 : discountTransfer[ brokerAcct -> 'ABC12345', gracePeriod -> 2, % days to pay transaction fee qosGuarantee -> 3, % max days to execute transaction %% feeCalculator: see below - reified formula fee -> ${feeCalculator(_TransactDate,_FeeDate,_Fee)}, %% can be more complex, eg precondition(_) defined by rules precondition(InObj) -> ${( %% buyer has valid address validAddress(InObj.buyerAcct.customer.address), %% Buyer and seller can agree on currency InObj.buyerAcct.bank..currency = InObj.sellerAcct.bank..currency, %% no international transfers - expressed as precondition InObj.buyerAcct.bank.address.country = InObj.sellerAcct.bank.address.country )}, action -> ${#transferViaBroker(_InObj, _Fee)}, #invoke(_InObj) ]. Service[#invoke(InObj)] :- Service : discountBroker, Service[action -> Action, precondition(InObj) -> Condition], Condition, % test precondition %% Provide input to transaction: a HiLog feature Action = _(InObj,Fee,Service.brokerAcct), Service[fee->FeePredicate], % assume that the pred has 4 args date(Today), %% unify Fee arg of Transaction with Fee arg of FeePredicate %% feeDate indicates when the fee will be paid FeePredicate = _(Service, Today, InObj.feeDate, Fee), FeePredicate, % calculate the transaction fee %% Send customer an ack. Sign with a legally binding signature getSignature(Sig), send(InObj.buyerAcct.customer,transfer(Sig,InObj,Today)), Action. % execute the service feeCalculator(Service,TransactDate,PayDate,20) :- Service[gracePeriod -> Grace], PayDate - TransactDate < Grace, !. feeCalculator(Service,TransactDate,PayDate,15) :- Service[qosGuarantee -> QOS], TransactDate - PayDate > QOS, !. feeCalculator(_Service,TransactDate,PayDate,25) :- true. #transferViaBroker(InObj, Fee, BrokerAccount) :- %% transfer to seller #transfer(InObj.Amount,InObj.buyerAcct,InObj.sellerAcct) | % parallel ops are not implemented in FLORA-2 #transfer(Fee, InObj.buyerAcct, BrokerAccount) #transfer(Amount, From, To) :- #withdraw(Amount,From), #deposit(Amount,To). #withdraw(Amount,Account):- balance(Account,Balance), Balance >= Amount, Balance2 is Balance-Amount, #change_balance(Account,Balance,Balance2). #deposit(Amount,Account) :- balance(Account,Balance), Amount >= 0, Balance2 is Balance+Amount, #change_balance(Account,Balance,Balance2). #change_balance(Account,Balance1,Balance2) :- delete{balance(Account,Balance1)}, insert{balance(Account,Balance2)}. [*] A note on: "Buyer wants to pay the Seller before paying the Broker." I view it as part of negotiations, not of service specification. This can be accommodated by allowing the client to specify a constraint, such as paySeller => payBroker in Transaction Logic. The actual constraint will look something like path,transfer(_,InObj.buyerAcct,InObj.sellerAcct),path => path,transfer(_,InObj.buyerAcct,Service.brokerAcct),path The InObj should then have an attribute clientConstraints. Then we could change the last line of #invoke from Action. to Action /\ InObj.clientConstraints [*] /\ not implemented. In general, temporal constraints on execution are hard to enforce [*] Example of precondition defined by rules: %% If service non-international, add an appropriate precondition Service[precondition(_InObj) ->> ${_InObj.buyerAcct.bank.address.country = _InObj.sellerAcct.bank.address.country}] :- not Service : internationalTransfer. In another use case will show a more object-oriented way of specifying pre/postconditions via rules.