/* BUYER SELLER SHIPPER SERVICE INTERACTION  */
/* Based on an example in a paper by Carbone, Honda and Yoshida */

defproc Buyer(buyer) =
  new session in (
        quoteCh!(session,buyer).
           session?(quote).
           select {
              session!(accept).session?(deliverydetails).Buyer(buyer);
              session!(reject).Buyer(buyer)
           });

defproc Seller(seller) =
                 quoteCh?(session,bu).
                 session!(price).
                 session?(choice).
                 select {
                    [choice=accept].
                    new t in (
                       deliveryCh!(t,seller).
                       t?(deliverydetails,sh).
                       session!(deliverydetails).
                       Seller(seller));
                    [choice=reject].
                    Seller(seller)
                 };

defproc Shipper(shipper) =
                 deliveryCh?(t,se).
                 t!(deliverydetails,shipper).
                 Shipper(shipper);

defproc System = Buyer(bu) | Seller(se) | Shipper(sh);

/* CONFORMANCE TO CHOREOGRAPHY */

defprop sArrow(message,src,dst) =
    inside((1 and @src and < message! > true)  | 
           (1 and @dst and < message? > true ) | true);

defprop sBuyer2Seller(message) = sArrow(message,bu,se);
defprop sSeller2Buyer(message) = sArrow(message,se,bu);
defprop sShipper2Seller(message) = sArrow(message,sh,se);
defprop sSeller2Shipper(message) = sArrow(message,se,sh);

defprop buyerSellerInteraction(session, A) =
    sBuyer2Seller(quoteCh) and
    [] ( sSeller2Buyer(session) and
         []( sBuyer2Seller(session) and
             [][]( A )));

defprop sellerShipperInteraction(A) =
    sSeller2Shipper(deliveryCh) and
    [] hidden t.
        ( sShipper2Seller(t) and
          [] ( A ));

defprop sGlobalDescription = 
    maxfix X.(
        hidden session.
        buyerSellerInteraction(session, 
            X 
            or 
            sellerShipperInteraction( 
                sSeller2Buyer(session) and []X)));

check System |= sGlobalDescription;

/* DEADLOCK FREEDOM */

defprop aLive = maxfix X. (show_fail(< tau > true) and [tau]X);
check System |= aLive;

/* RACE FREEDOM */

defprop write(x) = (1 and < x! > true);
defprop read(x) = (1 and < x? > true);
defprop hasRace =
    inside (exists x.( write(x) | write(x) | read(x) | true));
defprop raceFree = maxfix X.((not hasRace) and []X);
check System |= raceFree;