%:- module Ord.

:- include 'upper-onto.ncl'.

:- sorts
  Slot >> ItemID;  Slot >> ItemPrice;
  Role >> Buyer;  Role >> Seller.

:- objects
  reqForQuote(Buyer,Seller,ItemID) :: Message;
  quote(Seller,Buyer,ItemID,ItemPrice) :: Message;
  accept(Buyer,Seller,ItemID,ItemPrice) :: Message;
  reject(Buyer,Seller,ItemID,ItemPrice) :: Message;
  deliver :: Condition;  payment :: Condition;
  b :: Buyer;  s :: Seller;
  myItem :: ItemID;  myPrice :: ItemPrice.
  
:- variables
  itemID :: ItemID;  itemPrice :: ItemPrice.

nonexecutable act(reqForQuote(b,s,itemID)) if
fl(reqForQuote(b,s,itemID)).

nonexecutable act(quote(s,b,itemID,itemPrice)) if 
-fl(reqForQuote(b,s,itemID)) ++  fl(quote(s,b,itemID,itemPrice)).

nonexecutable act(accept(b,s,itemID,itemPrice)) if 
-fl(quote(s,b,itemID,itemPrice)) ++ 
fl(accept(b,s,itemID,itemPrice)) ++
fl(reject(b,s,itemID,itemPrice)). 

nonexecutable act(reject(b,s,itemID,itemPrice)) if 
-fl(quote(s,b,itemID,itemPrice)) ++ 
fl(accept(b,s,itemID,itemPrice)) ++
fl(reject(b,s,itemID,itemPrice)). 

nonexecutable act(reject(b,s,itemID,itemPrice)) if 
act(accept(b,s,itemID,itemPrice)).

act(quote(s,b,itemID,itemPrice)) causes 
create(cc(s,b,payment,deliver)).

act(accept(b,s,itemID,itemPrice)) causes create(
cc(b,s,deliver,payment)). 

:- query
label :: 5;  maxstep :: 4;  0: initial;
maxstep: fl(reject(b,s,itemID,itemPrice)) ++ fl(accept(b,s,itemID,itemPrice)).