:- include 'protocol-ontology.ncl'.

:- sorts
  Slot >> ItemID;  
  Slot >> ItemPrice;
  Role >> Customer;  
  Role >> Merchant.

:- objects
  reqForQuote(Customer,Merchant,ItemID) :: Message;
  quote(Merchant,Customer,ItemID,ItemPrice) :: Message;
  accept(Customer,Merchant,ItemID,ItemPrice) :: Message;
  reject(Customer,Merchant,ItemID,ItemPrice) :: Message;
  deliver(ItemID) :: Condition; 
  payment(ItemPrice) :: Condition;
  c :: Customer;  
  m :: Merchant;
  myItem :: ItemID;  
  myPrice :: ItemPrice.

:- variables
  item :: ItemID;  
  price :: ItemPrice.

nonexecutable act(reqForQuote(c,m,item)) if
fl(reqForQuote(c,m,item)).

nonexecutable act(quote(m,c,item,price)) if
-fl(reqForQuote(c,m,item)) ++ fl(quote(m,c,item,price)).

nonexecutable act(accept(c,m,item,price)) if
-fl(quote(m,c,item,price)) ++ fl(accept(c,m,item,price))
++ fl(reject(c,m,item,price)).

nonexecutable act(reject(c,m,item,price)) if
-fl(quote(m,c,item,price)) ++ fl(accept(c,m,item,price))
++ fl(reject(c,m,item,price)).

nonexecutable act(accept(c,m,item,price)) if act(reject(c,m,item,price)).

act(quote(m,c,item,price)) causes
create(cc(m,c,payment(price),deliver(item))).

act(accept(c,m,item,price)) causes 
create(cc(c,m,deliver(item),payment(price))).

:- query
label :: 5;  maxstep :: 4;  0: initial;
maxstep: fl(accept(c,m,item,price)) ++ fl(reject(c,m,item,price)).