module NEGOTIATION_PROCESSES (NEGOTIATION_TYPES) is

-------------------------------------------------------------------------------
-- Definition of initial and next values exchanged during negotiation rounds
-- in the online book auction example of [Salaun-Ferrara-Chirichiello-04]
-------------------------------------------------------------------------------

type Comp is
   -- computation of initial values
   times1,
   times2,
   -- computation of next values
   add1,
   add2,
   minus1,
   minus2
end type

-------------------------------------------------------------------------------

function compute (n: Nat, c: Comp) : Nat is
   case c in
     times1 -> return n
   | times2 -> return n * 2
   | add1   -> return n + 1
   | add2   -> return n + 2
   | minus1 -> return n - 1
   | minus2 -> return n - 2
   end case
end function

-------------------------------------------------------------------------------
-- Requester process for the online book auction example
-------------------------------------------------------------------------------

-- A requester is a client. It starts the controller which is responsible for
-- the negotiation with adequate parameters and it waits for an answer.
-- Parameters are the identifier of the book, the initial price to propose,
-- the invariant to respect, the function to compute values to propose.

process Requester [request, reply, order, refusal, sendpriceP, sendpriceR, givingup: any]
                  (ref: Nat, pi: Nat, inv: Inv, computfct: Comp) is
   Controller [request, reply, order, refusal, sendpriceP, sendpriceR, givingup]
              (ref, pi, inv, computfct);
   i -- for the equivalence with the original LOTOS specification
end process

-------------------------------------------------------------------------------

-- The controller process sends a request to a provider to verify that store has
-- available copies of the book. Depending on the reply, it starts the subprocess
-- NegotiateC in charge of the negotiation rounds or it recalls its again to try
-- another bookstore.
-- Parameters are those transmitted by the client/requester.

process Controller [request, reply, order, refusal, sendpriceP, sendpriceR, givingup: any]
                   (ref: Nat, pi: Nat, inv: Inv, computfct: Comp) is
   var b, status: Bool in
      loop L in
         alt
            request (ref);
            reply (?b);
            if b then
               NegotiateC [order, refusal, sendpriceP, sendpriceR, givingup] (pi, inv, computfct, ?status);
	       i; -- for the equivalence with the original LOTOS specification
               if status then
                  -- case of a successful order
                  break L
               end if
            end if
            -- let us try another bookstore
         []
            -- the controller stops the negotiation (or no satisfactory answers)
            break L
         end alt
      end loop
   end var
end process

-------------------------------------------------------------------------------

-- This process deals with the negotiation rounds on behalf of the Controller.
-- It proposes prices or receives prices and depending on the value of its
-- invariant for each price it refuses or orders the book.
-- It uses a simple strategy: it buys as soon as the price satifies its required
-- invariant.
-- It is based on the assumption that each participant proposes values towards
-- the other party, that is to say, that a provider lowers the value, and that a
-- requester rises the value.

process NegotiateC [order, refusal, sendpriceP, sendpriceR, givingup: any]
                   (in var curp: Nat, inv: Inv, computfct: Comp,
                    out status: Bool) is
   loop L in
      alt
         var p: Nat in
            sendpriceP (?p);
            if conform (p, inv) then
               order;
               status := true;
               break L
            else
               refusal
            end if
         end var
      []
         only if conform (curp, inv) then
            sendpriceR (curp);
            alt
               order;
               status := true;
               break L
            []
               refusal;
               curp := compute (curp, computfct)
            end alt
         end if
      []
         givingup;
         -- The client/requester stops because results not satisfactory
         status := false;
         break L
      end alt
   end loop
end process

-------------------------------------------------------------------------------
-- Provider process for the online book auction example
-------------------------------------------------------------------------------

-- A provider waits for some requests. Then, it tests if the book belongs to its
-- base. If it is the case, it launches its negotiating subprocess. Otherwise, it
-- calls itself recursively.
-- Parameters are the bookstore, the function to compute the initial value to
-- propose, and the function to compute the other values.

process Provider [request, reply, order, refusal, sendpriceP, sendpriceR, givingup: any]
                 (in var bs: BookStore, initfct: Comp, computfct: Comp) is
   loop L in
      alt
         var r: Nat, status: Bool in
            request (?r);
            reply (isAvailable (r, bs));
            if isAvailable (r, bs) then
               NegotiateP [order, refusal, sendpriceP, sendpriceR, givingup]
                          (compute (retrievePrice (r, bs), initfct),
                           retrieveInv (r, bs), computfct, ?status);
	       i; -- for the equivalence with the original LOTOS specification
               if status then
                  bs := decrease (r, 1, bs)
               end if
            end if
         end var
      []
         break L
      end alt
   end loop
end process

-------------------------------------------------------------------------------

-- This process deals with the negotiation rounds on behalf of a provider; it is
-- complementary to the process NegotiatieC introduced above.
-- Let us remind that both the provider and the client can propose values.

process NegotiateP [order, refusal, sendpriceP, sendpriceR, givingup: any]
                   (in var curprice: Nat, inv: Inv, computfct: Comp,
                    out status: Bool) is
   loop L in
      alt
         if conform (curprice, inv) then
            sendpriceP (curprice);
            alt
               order;
               status := true;
               break L
            []
               refusal;
               curprice := compute (curprice, computfct)
            end alt
         else
            -- The provider stops because it is impossible to reach an agreement
            status := false;
            break L
         end if
      []
         var p: Nat in
            sendpriceR (?p);
            if conform (p, inv) then
               order;
               status := true;
               break L
            else
               refusal
            end if
         end var
      []
         givingup;
         -- Stops because the client stops too
         status := false;
         break L
      end alt
   end loop
end process

-------------------------------------------------------------------------------

end module