We provide here a collection of examples of interaction models taken from our test cases, based on areas such as bioinformatics, business and emergency response.

Customer and vendor negotiation

A customer, C, can send a request to a vendor, V, to buy an item, X, that the customer needs and believes the vendor sells. Then the customer takes the role of negotiator with the vendor.A negotiating customer with a set, S, of negotiated attributes of the desired item, X, either receives an offer of a new attribute, A, or it receives a request to commit to the current set of negotiated attributes and replies with the constrants, CA, it wishes to impose on those attributes. In the scenario of purchasing a computer, A could represent, for example, the size of the monitor.A vendor, V, receives a request from a customer, C, to buy an item, X; then takes the role of negotiator with the customer over the attribute set, S, that applies to that item. A negotiating vendor with a set, S, of negotiable attributes of the desired item, X, either takes the first attribute, A, of S and offers it to the customer for acceptance, or if S is empty it asks the customer to commit to the attributes they have discussed and receives the customer's constraints, CA, on the final values of those attributes. If these are satisfiable, it informs the customer of the final attribute values, F, for the sold item.


//  Written by Dave Robertson
//
//  LCC Specification for a customer and vendor negotiation:

a(customer,C)::
	ask(buy(X)) => a(vendor,V) <- need(X) and sells(X,V) then
	a(neg_customer(X,V,[]),C)

a(neg_customer(X,V,S),C)::
	(
		offer(A) <= a(neg_vendor(X,C,_),V) then
		accept(A) => a(neg_vendor(X,C,_),V) <- acceptable(A) then
		a(neg_customer(X,V,[att(A)|S],C)
	)
	or
	(
		ask(commit) <= a(neg_vendor(X,C,_),V) then
		tell(commit(S,CA)) => a(neg_vendor(X,C,_),V) <- choose(S,CA) then
		tell(sold(F)) <= a(neg_vendor(X,C,_),V)
	)

a(vendor,V)::
	ask(buy(X)) <= a(customer,C) then
	a(neg_vendor(X,C,S),V) <- attributes(X,S)

a(neg_vendor(X,C,S),V)::
	(
		offer(A) <= a(neg_customer(X,V,_),C) <- S=[A|T] and available(A) then
		accept(A) => a(neg_customer(X,V,_),C) then
		a(neg_vendor(X,C,T),V)	
	)
	or
	(
		ask(commit) => a(neg_customer(X,V,_),C) <- S = [] then
		tell(commit(F,CA)) <= a(neg_customer(X,V,_),C) then
		tell(sold(F)) => a(neg_customer(X,V,_),C) <- CA
	)

Printing sales orders

An input device, I, can send a message to a sales agent, S, containing information about an order, X; it then continues in the same role.A sales agent, S, can receive from an input device an order, X, and can send to a printer, P, the order X that the sales believes to be a valid input. Then the sales either receives from the printer that the order has been successfully printed or that the order has failed to print. In both cases, the sales continues in the same role.A printer, P, can receive an order, X, from a sales, S, and either sends to the sales that the order has been successfully printed if the printing was completed. Otherwise, the printer can ask the administrator, A, for assistance, receive a response from the administrator, and sends a response to the sales that the printing has failed.An administrator, A, receives a request from a printer, P, for help and then sends it a response offering help.
[More details]


//  Written by Li Guo and modified by Michael Chan
//
//  LCC Specification for a sales order printing process:

r( inputdevice, initial)
r( sales, necessary, 1)
r( printer, necessary, 1)
r( admin, necessary,1)

a(I, inputdevice)::
	getInput(X) => a(S, sales) then
	a(I, inputdevice)

a(S, sales)::
	getInput(X) <= a(I, inputdevice) then
	saleOrder(X) => a(printer, P) <- validInput(X) then
	(
		(printed(SaleOrder(X)) <= a(P, printer) 
		then
			a(S, sales)) 
		or
		(
			failed(saleOrder(X)) <= a(P, printer) 
			then
			a(loop(X), sales)
		)
	)

a(P, printer)::
saleOrder(X) <= a(loop(X), sales) 
	then
	(
		printed(saleOrder(X)) => a(loop(X), sales) 
		or
		(
			askForHelp(help) => a(A, admin) 
			then
			(help) <= a(A, admin) 
			then
			failed(saleOrder(X)) => a(X, sales) 
			then
			a(P, printer)
		)
	)

a(A, admin)::
	askForHelp(help) <= a(P, printer) then
	(help) => a(P, printer)

Shipping service

A shipping service customer, C, can send a request to a shipping service, P, for a shipment. It then either receives a single notice from the shipping service informing it that the items have been shipped or takes the role of a pending shipment customer when some items are yet to be shipped.A pending shipment customer, PC, receives a notice from the priority shipping service provider, PP, until all requested items have been shipped. It continues in this role until all items have been shipped.A shipping service provider, P, receives a shipping request from a shipping service customer, C. It then either sends a shipping notice to the customer if the shipment is complete, or takes the role of a priority shipping service provider, PP, if there remain some unshipped items.A priority shipping service provider, PP, sends notices to the pending shipment customer, PC, and continues to be in this role until all items have been shipped.
[More details]


//  Written by Li Guo and modified by Michael Chan
//
//  LCC Specification for a shipping service process:

a(shippingservicecustomer, C) ::
	shiprequest => a(shippingservice, P) then
	(
		shippingnotice(status) <= a(shippingservice, P)
		or
		(
			a(pendingshipmentcustomer(loop(m)), PC) <-
			(itemsshipped = 0) and itemsshipped < itemstotal
		)
		or null
	)

a(pendingshipmentcustomer(loop(m)), PC) ::
	shippingnotice(status) <= a(priorityshippingservice(loop(m)), PP) then
	(
		a(pendingshipmentcustomer(loop(m)), PC) <- 
		(itemsshipped < itemstotal) and itemsshipped = itemsshipped + itemscount
	)
	or null

a(shippingservice, P) ::
	shiprequest <= a(shippingservicecustomer, C) then
	(
		(
			shippingnotice(status) => a(shippingservicecustomer, C)
			<- (status = itemscount) and getvariableproperty(shiprequest, shipcomplete)
		)
		or
		(
			a(priorityshippingservice(loop(m)), PP)
			<- (itemsshipped = 0) and (itemsshipped < itemstotal)
		)
		or null
	)

a(priorityshippingservice(loop(m)), PP) ::
	shippingnotice(status) => a(pendingshipmentcustomer(loop(m)), PC) <- status = yes then
	(
		(
			a(priorityshippingservice(loop(m)), P) 
			<- (itemsshipped < itemstotal) and (itemsshipped = itemsshipped + itemscount)
		)
		or null
	)

Egglue Powered