SapNego.scr

//$ ~/scribbler/scribble/scribblec-assrt.sh -assrt -fair -z3 -batch SapNego.scr
//$ sessionstar SapNego.scr Negotiate C

module SapNego;

type <fstar> "int" from "" as int;

// C = Consumer, P = Producer
global protocol Negotiate(role C, role P)
{
  propose(initialPrice: int) from C to P;
  //do NegoAux(C, P);  @'[initialPrice]'
  do NegoAux(C, P);  @'P[initialPrice] C[initialPrice]'
}

aux global protocol NegoAux(role C, role P)
            //@'[prop: int = 0]' {
            @'P[propP: int = 0] C[propC: int = 0]' {
  choice at P
  {
    accpt(confirmedPrice1: int) from P to C;
      @"propP = confirmedPrice1"
    confirm() from C to P;
  }
  or
  {
    counter(counterOfferPrice: int) from P to C;
      @"counterOfferPrice < propP || counterOfferPrice > propP"

    // TODO: swap C/P roles via do
    choice at C
    {
      accpt(confirmedPrice2: int) from C to P;
        @"counterOfferPrice = confirmedPrice2"
      confirm() from P to C;
    }
    or
    {
      counter(countercounter: int) from C to P;
        @"(countercounter < counterOfferPrice || countercounter > counterOfferPrice)
            && (countercounter < propC || countercounter > propC)"
      //do NegoAux(C, P);  @'[countercounter]'
      do NegoAux(C, P);  @'P[countercounter] C[countercounter]'
    }
    or
    {
      reject() from C to P;
    }
  }
  or
  {
    reject() from P to C;
  }
}





/* FIXME:

// C = Consumer, P = Producer
global protocol Negotiate(role C, role P)
{
  propose(initialPrice: int) from C to P;
  do NegoAux(C, P);  @'P[initialPrice]'
}

aux global protocol NegoAux(role C, role P) @'P[prop: int = 0]' {
  choice at P
  {
    accpt(confirmedPrice1: int) from P to C;
      @"prop = confirmedPrice1"
    confirm() from C to P;
  }
  or
  {
    counter(counterOfferPrice: int) from P to C;
      @"counterOfferPrice < prop || counterOfferPrice > prop"  // !!!
    choice at C
    {
      accpt(confirmedPrice2: int) from C to P;
        @"counterOfferPrice = confirmedPrice2"
      confirm() from P to C;
    }
    or
    {
      counter(countercounter: int) from C to P;
        @"(countercounter < counterOfferPrice || countercounter > counterOfferPrice)
            && (countercounter < prop || countercounter > prop)"
      do NegoAux(C, P);  @'P[countercounter]'
    }
    or
    {
      reject() from C to P;
    }
  }
  or
  {
    reject() from P to C;
  }
}
//*/



/*
global protocol NegotiateOrig(role C, role P)
{
  propose(initialPrice: int) from C to P;
  do NegoOrigAux(C, P);  @'[initialPrice]'
}

aux global protocol NegoOrigAux(role C, role P) @'[prop: int = 0]' {
  choice at P
  {
    accpt(confirmedPrice1: int) from P to C;
      @"prop = confirmedPrice1"
    confirm() from C to P;
  }
  or
  {
    counter(counterOfferPrice: int) from P to C;
      @"counterOfferPrice < prop || counterOfferPrice > prop"
    choice at C
    {
      accpt(confirmedPrice2: int) from C to P;
        @"counterOfferPrice = confirmedPrice2"
      confirm() from P to C;
    }
    or
    {
      counter(countercounter: int) from C to P;
        @"(countercounter < counterOfferPrice || countercounter > counterOfferPrice)
            && (countercounter < prop || countercounter > prop)"
      do NegoOrigAux(C, P);  @'[countercounter]'
    }
    or
    {
      reject() from C to P;
    }
  }
  or
  {
    reject() from P to C;
  }
}
//*/