354 lines
12 KiB
Markdown
354 lines
12 KiB
Markdown
---
|
|
title: Two-Party Buyer Protocol
|
|
---
|
|
|
|
<!--
|
|
var Syndicate = require('../../src/main.js');
|
|
-->
|
|
|
|
# {{ page.title }}
|
|
|
|
This is an extended two-buyer book-purchase protocol, based
|
|
loosely on an example given in:
|
|
|
|
> K. Honda, N. Yoshida, and M. Carbone, “Multiparty asynchronous
|
|
> session types,” POPL 2008.
|
|
|
|
## The Scenario
|
|
|
|
A book-seller responds to requests for book prices when asked. A
|
|
pair of prospective buyers run through a shopping list. For each
|
|
book, the first buyer offers to split the cost of the book with
|
|
the second. If the second has enough money left, it accepts;
|
|
otherwise, it rejects the offer, and the first buyer tries a
|
|
different split. If the second buyer agrees to a split, it then
|
|
negotiates the purchase of the book with the book-seller.
|
|
|
|
## The Protocol
|
|
|
|
### Role: SELLER
|
|
|
|
When interest in `bookQuote($title, _)` appears, asserts
|
|
`bookQuote(title, Maybe Float)`, `false` meaning not available,
|
|
and otherwise an asking-price.
|
|
|
|
When interest in `order($title, $offer-price, _, _)` appears,
|
|
asserts `order(title, offer-price, false, false)` for "no sale",
|
|
otherwise `order(title, offer-price, PositiveInteger, String)`, an
|
|
accepted sale.
|
|
|
|
### Role: BUYER
|
|
|
|
Observes `bookQuote(title, $price)` to learn prices.
|
|
|
|
Observes `order(title, offer-price, $id, $delivery-date)` to make orders.
|
|
|
|
### Role: SPLIT-PROPOSER
|
|
|
|
Observes `splitProposal(title, asking-price, contribution,
|
|
$accepted)` to make a split-proposal and learn whether it was
|
|
accepted or not.
|
|
|
|
### Role: SPLIT-DISPOSER
|
|
|
|
When interest in `splitProposal($title, $asking-price,
|
|
$contribution, _)` appears, asserts `splitProposal(title,
|
|
askingPrice, contribution, true)` to indicate they are willing to
|
|
go through with the deal, in which case they then perform the role
|
|
of BUYER for title/asking-price, or asserts `splitProposal(title,
|
|
asking-price, contribution, false)` to indicate they are unwilling
|
|
to go through with the deal.
|
|
|
|
## The Code
|
|
|
|
### Type Declarations
|
|
|
|
First, we declare *assertion types* for our protocol.
|
|
|
|
assertion type bookQuote(title, price);
|
|
assertion type order(title, price, id, deliveryDate);
|
|
|
|
assertion type splitProposal(title, price, contribution, accepted);
|
|
|
|
### Utilities
|
|
|
|
This routine is under consideration for possible addition to the
|
|
core library.
|
|
|
|
function whileRelevantAssert(P) {
|
|
react {
|
|
assert P;
|
|
} until {
|
|
case retracted Syndicate.observe(P);
|
|
}
|
|
}
|
|
|
|
### Implementation: SELLER
|
|
|
|
function seller() {
|
|
actor {
|
|
|
|
We give our actor two state variables: a dictionary recording our
|
|
inventory of books (mapping title to price), and a counter
|
|
tracking the next order ID to be allocated.
|
|
|
|
this.books = {
|
|
"The Wind in the Willows": 3.95,
|
|
"Catch 22": 2.22,
|
|
"Candide": 34.95
|
|
};
|
|
this.nextOrderId = 10001483;
|
|
|
|
Looking up a price yields `false` if no such book is in our
|
|
inventory.
|
|
|
|
this.priceOf = function (title) {
|
|
return (title in this.books) && this.books[title];
|
|
};
|
|
|
|
The seller responds to interest in bookQuotes by asserting a
|
|
responsive record, if one exists.
|
|
|
|
react {
|
|
during Syndicate.observe(bookQuote($title, _)) {
|
|
assert bookQuote(title, this.priceOf(title));
|
|
}
|
|
}
|
|
|
|
It also responds to order requests.
|
|
|
|
react {
|
|
on asserted
|
|
Syndicate.observe(order($title, $offerPrice, _, _)) {
|
|
|
|
We cannot sell a book we do not have, and we will not sell for
|
|
less than our asking price.
|
|
|
|
var askingPrice = this.priceOf(title);
|
|
if ((askingPrice === false) || (offerPrice < askingPrice)) {
|
|
whileRelevantAssert(
|
|
order(title, offerPrice, false, false));
|
|
} else {
|
|
|
|
But if we can sell it, we do so by allocating an order ID and
|
|
replying to the orderer.
|
|
|
|
var orderId = this.nextOrderId++;
|
|
delete this.books[title];
|
|
|
|
actor {
|
|
whileRelevantAssert(
|
|
order(title, offerPrice, orderId, "March 9th"));
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
### Implementation: SPLIT-PROPOSER and book-quote-requestor
|
|
|
|
function buyerA() {
|
|
actor {
|
|
var self = this;
|
|
|
|
Our actor remembers which books remain on its shopping list, and
|
|
tries to buy them one at a time, sharing costs with `buyerB`.
|
|
|
|
self.titles = ["Catch 22",
|
|
"Encyclopaedia Brittannica",
|
|
"Candide",
|
|
"The Wind in the Willows"];
|
|
|
|
JavaScript's callback-oriented blocking means that we express our
|
|
loop in almost a tail-recursive style, using helper functions
|
|
`buyBooks` and `trySplit`.
|
|
|
|
buyBooks();
|
|
|
|
function buyBooks() {
|
|
if (self.titles.length === 0) {
|
|
console.log("A has bought everything they wanted!");
|
|
return;
|
|
}
|
|
|
|
var title = self.titles.shift();
|
|
|
|
First, retrieve a quote for the title, and analyze the result.
|
|
|
|
react until {
|
|
case asserted bookQuote(title, $price) {
|
|
if (price === false) {
|
|
console.log("A learns that "+title+" is out-of-stock.");
|
|
buyBooks();
|
|
} else {
|
|
console.log("A learns that the price of "+title+
|
|
" is "+price);
|
|
|
|
Next, repeatedly make split offers to a SPLIT-DISPOSER until
|
|
either one is accepted, or the contribution from the
|
|
SPLIT-DISPOSER becomes pointlessly small. We start the process by
|
|
offering to split the price of the book evenly.
|
|
|
|
trySplit(title, price, price / 2);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
function trySplit(title, price, contribution) {
|
|
console.log("A makes an offer to split the price of "+title+
|
|
" contributing "+contribution);
|
|
|
|
If we are about to offer to split the price, but the other buyer
|
|
would contribute less than 10c, then it's not worth bothering; we
|
|
may as well buy it ourselves. Another version of the program could
|
|
perform the BUYER role here.
|
|
|
|
if (contribution > (price - 0.10)) {
|
|
console.log("A gives up on "+title+".");
|
|
buyBooks();
|
|
} else {
|
|
|
|
Make our proposal, and wait for a response.
|
|
|
|
react until {
|
|
case asserted
|
|
splitProposal(title, price, contribution, true) {
|
|
console.log("A learns that the split-proposal for "+
|
|
title+" was accepted");
|
|
buyBooks();
|
|
}
|
|
|
|
case asserted
|
|
splitProposal(title, price, contribution, false) {
|
|
console.log("A learns that the split-proposal for "+
|
|
title+" was rejected");
|
|
trySplit(title,
|
|
price,
|
|
contribution + ((price - contribution) / 2));
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
### Implementation: SPLIT-DISPOSER and BUYER
|
|
|
|
function buyerB() {
|
|
actor {
|
|
|
|
This actor maintains a record of the amount of money it has left
|
|
to spend.
|
|
|
|
this.funds = 5.00;
|
|
|
|
It spends its time waiting for a SPLIT-PROPOSER to offer a
|
|
`splitProposal`.
|
|
|
|
react {
|
|
on asserted
|
|
Syndicate.observe(splitProposal($title,
|
|
$price,
|
|
$theirContribution,
|
|
_))
|
|
{
|
|
var myContribution = price - theirContribution;
|
|
console.log("B is being asked to contribute "+myContribution+
|
|
" toward "+title+" at price "+price);
|
|
|
|
We may not be able to afford contributing this much.
|
|
|
|
if (myContribution > this.funds) {
|
|
console.log("B hasn't enough funds ("+this.funds+
|
|
" remaining)");
|
|
whileRelevantAssert(
|
|
splitProposal(title, price, theirContribution, false));
|
|
} else {
|
|
|
|
But if we *can* afford it, update our remaining funds and spawn a
|
|
small actor to handle the actual purchase now that we have agreed
|
|
on a split.
|
|
|
|
var remainingFunds = this.funds - myContribution;
|
|
console.log("B accepts the offer, leaving them with "+
|
|
remainingFunds+" remaining funds");
|
|
this.funds = remainingFunds;
|
|
|
|
actor {
|
|
react {
|
|
|
|
While waiting for order confirmation, take the opportunity to
|
|
signal to our SPLIT-PROPOSER that we accepted their proposal.
|
|
|
|
assert splitProposal(title,
|
|
price,
|
|
theirContribution,
|
|
true);
|
|
|
|
When order confirmation arrives, this purchase is completed.
|
|
|
|
} until {
|
|
case asserted order(title, price, $id, $date) {
|
|
console.log("The order for "+title+" has id "+id+
|
|
", and will be delivered on "+date);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
### Starting Configuration
|
|
|
|
ground dataspace {
|
|
seller();
|
|
buyerA();
|
|
buyerB();
|
|
}
|
|
|
|
## A Sample Run
|
|
|
|
Run the program with `../../bin/syndicatec index.js | node` from a
|
|
checkout of the Syndicate repository.
|
|
|
|
A learns that the price of Catch 22 is 2.22
|
|
A makes an offer to split the price of Catch 22 contributing 1.11
|
|
B is being asked to contribute 1.11 toward Catch 22 at price 2.22
|
|
B accepts the offer, leaving them with 3.8899999999999997 remaining funds
|
|
A learns that the split-proposal for Catch 22 was accepted
|
|
A learns that Encyclopaedia Brittannica is out-of-stock.
|
|
The order for Catch 22 has id 10001483, and will be delivered on March 9th
|
|
A learns that the price of Candide is 34.95
|
|
A makes an offer to split the price of Candide contributing 17.475
|
|
B is being asked to contribute 17.475 toward Candide at price 34.95
|
|
B hasn't enough funds (3.8899999999999997 remaining)
|
|
A learns that the split-proposal for Candide was rejected
|
|
A makes an offer to split the price of Candide contributing 26.212500000000002
|
|
B is being asked to contribute 8.7375 toward Candide at price 34.95
|
|
B hasn't enough funds (3.8899999999999997 remaining)
|
|
A learns that the split-proposal for Candide was rejected
|
|
A makes an offer to split the price of Candide contributing 30.581250000000004
|
|
B is being asked to contribute 4.368749999999999 toward Candide at price 34.95
|
|
B hasn't enough funds (3.8899999999999997 remaining)
|
|
A learns that the split-proposal for Candide was rejected
|
|
A makes an offer to split the price of Candide contributing 32.765625
|
|
B is being asked to contribute 2.184375000000003 toward Candide at price 34.95
|
|
B accepts the offer, leaving them with 1.7056249999999968 remaining funds
|
|
A learns that the split-proposal for Candide was accepted
|
|
A learns that the price of The Wind in the Willows is 3.95
|
|
A makes an offer to split the price of The Wind in the Willows contributing 1.975
|
|
The order for Candide has id 10001484, and will be delivered on March 9th
|
|
B is being asked to contribute 1.975 toward The Wind in the Willows at price 3.95
|
|
B hasn't enough funds (1.7056249999999968 remaining)
|
|
A learns that the split-proposal for The Wind in the Willows was rejected
|
|
A makes an offer to split the price of The Wind in the Willows contributing 2.9625000000000004
|
|
B is being asked to contribute 0.9874999999999998 toward The Wind in the Willows at price 3.95
|
|
B accepts the offer, leaving them with 0.718124999999997 remaining funds
|
|
A learns that the split-proposal for The Wind in the Willows was accepted
|
|
A has bought everything they wanted!
|
|
The order for The Wind in the Willows has id 10001485, and will be delivered on March 9th
|