Buyer choreography example

Description

This is a buying scenario that describes the interaction between:

  • a buyer;
  • a seller;
  • a bank.

The buyer starts the choreography by deciding which item she is interested in. Then the adaptive scope begins, led by the seller. Notably, the non-functional property N.scope_name defines the name of the scope price_inquiry. The other non-functional property of this scope states that there are no active offers (N.offers = 0). If no adaptation rule applies, the seller will retrieve the price with function getPrice and send it to the buyer for acceptance.

scope @seller {
  s_price@seller =  getPrice( s_prod );
  offer: seller( s_price ) -> buyer( b_price );
  priceOk@buyer = getInput( "Do you accept the price " + b_price + " [yes/no]" )
} prop { N.offers = 0, N.scopename = "price_inquiry" };

The rule price_inquiry applies if there are no offers. Notice that the rule introduces the new function getDiscountedPrice used to retrieve the discounted price based on the cardID of the buyer.

rule {
  include getDiscountedPrice from "socket://localhost:8000"
  on {
    N.offers == 0 and
    N.scopename == "price_inquiry"
  }
  do {
    cardId@buyer = getInput( "Insert your customer card ID");
    card: buyer( cardId ) -> seller( cardId );
    s_price@seller = getDiscountedPrice( s_prod, cardId );
    offer: seller( s_price ) -> buyer( b_price );
    priceOk@buyer = getInput( "Do you accept the price " + b_price + " [yes/no]" )
  }
}

Then, if the buyer accepts the deal, the choreography will proceed with the subsequent scope, whose N.scope_name is payment. The non-functional property of this scope states that the security level of the procedure is 1 (N.security_level = 1).

scope @bank {
  payment_ok@bank = true;
  pay : buyer() -> bank()
} prop { N.scope_name = "payment" and N.security_level = 1 };

The corresponding rule applies since the security level of the adaptive scope is below 2. The adapted procedure requires an explicit agreement from the buyer and introduces the new function testChallenge that checks the correct insertion of the PIN number to confirm the payment.

rule {
  include testChallenge from "socket://localhost:8001"
  on { N.securityLevel < 2 and N.scopename == "payment" }
  do {
    auth@buyer = getInput( "Do you authorise the payment? [yes/no]");
    if( auth == "yes" )@buyer{
      account: bank( "Insert your account ID" ) -> buyer( b_req );
      b_acc@buyer = getInput( b_req );
      account: buyer( b_acc ) -> bank( bank_acc ); 
      pin: bank( "Insert your PIN" ) -> buyer( b_req );
      b_pin@buyer = getInput( b_req );
      pin: buyer( b_pin ) -> bank( bank_pin ); 
      match@bank = testChallenge( bank_acc, bank_pin );
      if ( match == true )@bank{
        paymentOK@bank = true
      } else {
        paymentOk@bank = false
      }
    }
  }
}

Code

Click on the buttons below to download the code of this example.