To buy a product, pay a fee to the broker and the cost of the product to the seller. These steps can be done in parallel: transfer(Fee,Buyer,Broker) | transfer(Cost,Buyer,Seller) This can be regarded as a composition where the same service (money transfer) is invoked twice. We can elaborate on this service as follows (where "," denotes sequential composition): transfer(Amount,Account1,Account2) :- withdraw(Amount,Account1), deposit(Amount,Account2). withdraw(Amount,Account):- balance(Account,Balance), Balance >= Amount, % Precondition change_balance(Account,Balance,Balance-Amount). deposit(Amount,Account) :- balance(Account,Balance), Amount >= 0, % Precondition change_balance(Account,Balance,Balance+Amount). change_balance(Account,Balance1,Balance2) :- delete(balance(Account,Balance1)), insert(balance(Account,Balance2)).What follows is an equivalent set of process descriptions using PSL.

These activities are specified as terms:

(forall (?x) (activity (buy_product ?x))) (forall (?x ?y ?z) (activity (transfer ?x ?y ?z))) (forall (?x ?y) (activity (withdraw ?x ?y))) (forall (?x ?y) (activity (deposit ?x ?y)))

(forall (?x ?y ?z) (subactivity (transfer ?x ?y ?z) (buy_product ?y))) (forall (?x ?y ?z) (subactivity (withdraw ?x ?y) (transfer ?x ?y ?z))) (forall (?x ?y ?z) (subactivity (deposit ?x ?z) (transfer ?x ?y ?z)))The process description for

(forall (?occ) (implies (occurrence_of ?occ (buy_product ?Buyer)) (exists (?occ1 ?occ2 ?Fee ?Cost ?broker ?Seller) (and (occurrence_of (transfer ?Fee ?Buyer ?Broker)) (occurrence_of (transfer ?Cost ?Buyer ?Seller)) (subactivity_occurrence ?occ1 ?occ) (subactivity_occurrence ?occ2 ?occ)))))The process description for

(forall (?occ) (implies (occurrence_of ?occ (transfer ?Amount ?Account1 ?Account2)) (exists (?occ1 ?occ2 ?occ3) (and (occurrence_of ?occ1 (withdraw ?Amount ?Account1)) (occurrence_of ?occ2 (deposit ?Amount ?Account2)) (subactivity_occurrence ?occ1 ?occ) (subactivity_occurrence ?occ2 ?occ) (leaf_occ ?occ3 ?occ1) (min_precedes ?occ3 (root_occ ?occ2))))))The axiomatization of the next set of activities requires a little more information, since there is some ambiguity about which activities are subactivities of others.

(forall (?x ?y ?z) (activity (change_balance ?x ?y ?z))) (subactivity (change_balance ?Account ?Balance1 ?Balance2) (deposit ?Amount ?Account)) (subactivity (change_balance ?Account ?Balance1 ?Balance2) (withdraw ?Amount ?Account))In this case,

(forall (?occ) (implies (and (occurrence_of ?occ (withdraw ?Amount ?Account)) (prior (balance ?account ?Balance) (root_occ ?occ)) (greaterEq ?Balance ?amount)) (exists (?occ1) (and (occurrence_of ?occ1 (change_balance ?account ?Balance (plus ?Balance ?Amount))) (subactivity_occurrence ?occ1 ?occ))))The effects of

(forall (?occ) (implies (and (occurrence_of ?occ (change_balance ?Account ?Amount1 ?Amount2)) (leaf_occ ?occ1 ?occ)) (and (holds (balance ?Account ?Amount2)) (not (holds (balance ?Account ?Amount1))))))

(forall (?occ) (implies (and (occurrence_of ?occ (withdraw ?Amount ?Account)) (legal ?occ)) (and (prior (balance ?account ?Balance) (root_occ ?occ)) (greaterEq ?Balance ?amount))))

(forall (?occ ?occ1) (implies (and (occurrence_of ?occ (withdraw ?Amount ?Account)) (leaf_occ ?occ1 ?occ)) (and (holds (balance ?account (minus ?Balance ?Amount)) (not (holds (balance ?account ?Balance)))))