wsmlVariant _"http://www.wsmo.org/wsml/wsml-syntax/wsml-flight"

namespace {_"http://www.wsmo.org/ontologies/spChoreographies#",
sp  _"http://www.wsmo.org/ontologies/supplierProvider#",
corp  _"http://www.wsmo.org/ontologies/corporate#",
pSWSDL  _"http://www.wsmo.org/ontologies/providerSupplierWSDL#"
}

/*
 * There is no format for definition of orchestration that 
 * passes the validator.  The following form is used.
 */

webService _"http://ontologies.deri.org/spWebService"
//  Supplier-Producer Choreographies:
interface spUserInterface
orchestration productShippingOrchestration
  stateSignature productShippingOrchestrationSignature
  guardedTransitions producerShipperOrchestrationRules


stateSignature productShippingOrchestrationSignature

  in {
      sp#productName withGrounding
          spWS#wsdl.interfaceMessageReference(
		SP_PortType/pSWSDL#productName/In),
      sp#destination  withGrounding
          spWS#wsdl.interfaceMessageReference(
		SP_PortType/pSWSDL#destination/In),
      sp#shipperOffer withGrounding
          spWS#wsdl.interfaceMessageReference(
		SP_PortType/pSWSDL#shipperOffer/In),
      sp#globalAnswer  withGrounding
          spWS#wsdl.interfaceMessageReference(
		SP_PortType/pSWSDL#userAcknowledgement/In),
      sp#producerAnswer withGrounding
          spWS#wsdl.interfaceMessageReference(
		SP_PortType/pSWSDL#producerAnswer/In),
      sp#shipperAnswer withGrounding
          spWS#wsdl.interfaceMessageReference(
		SP_PortType/pSWSDL#shipperAnswer)
       sp#producerConfirmation withGrounding
          spWS#wsdl.interfaceMessageReference(
		SP_PortType/pSWSDL#producerConfirmation/In),
      sp#shipperConfirmation withGrounding
          spWS#wsdl.interfaceMessageReference(
		SP_PortType/pSWSDL#shipperConfirmation/In)

     }
  out {
      sp#producerRequest withGrounding
          spWS#wsdl.interfaceMessageReference(
		SP_PortType/pSWSDL#producerRequest/Out),
      sp#globalOffer  withGrounding
          spWS#wsdl.interfaceMessageReference(
		SP_PortType/pSWSDL#globalOffer/Out),
      sp#globalConfirmation withGrounding
          spWS#wsdl.interfaceMessageReference(
		SP_PortType/pSWSDL#globalConfirmation/Out),
      sp#compositeGoal  withGrounding
          spWS#wsdl.interfaceMessageReference(
		SP_PortType/pSWSDL#compositeGoal/Out)
      }


  shared {
      sp#shipperRequest withGrounding
          spWS#wsdl.interfaceMessageReference(
		SP_PortType/pSWSDL#pSRequest/Shared),

      sp#producerOffer withGrounding
          spWS#wsdl.interfaceMessageReference(
		SP_PortType/pSWSDL#producerOffer/Shared)
      }







guardedTransitions producerShipperOrchestrationRules

  if (?request[product hasValue ?product,
	         quantity hasValue ?amt] memberOf sp#productName)
     then ((invoke sp#producerRequest)		// (Choreography uses ?request)
           and
           (add(_#[product hasValue ?product,
                   quantity hasValue ?amt] memberOf sp#producerRequest)))	
		// other details may be generated



  if ((?pOffer[request hasValue ?request,
	         acceptReject hasValue sp#acceptance,
               productSize hasValue ?pSize] memberOf sp#producerOffer) and
      (?location memberOf sp#destination))
     then ((invoke shipperRequest)
           and
           (update(?pOffer[acceptReject hasValue sp#processed])))	



  if ((?pOffer[request hasValue ?request] memberOf sp#producerOffer) and
      (?sOffer[request hasValue ?request,
               acceptReject hasValue sp#acceptance] memberOf shipperOffer))
      then 
        update(?request[acceptRejectOffer hasValue
                          _[producerOffer hasValue ?pOffer,
                            shipperOffer hasValue ?sOffer]
                           memberOf sp#globalOffer])




  if (?response[acceptReject hasValue ?userAcceptance,
                request hasValue ?request] memberOf sp#globalAnswer)
     then
 ((add(_[acceptance hasValue ?userAcceptance,
	        request hasValue ?request] memberOf sp#producerAnswer)) and
   	 (add(_[acceptance hasValue ?userAcceptance,
     	        request hasValue ?request] memberOf sp#shipperAnswer)))
  // If the user acceptance has separate details for shipper and producer,
  // they should be separated here.

  if (?response[acceptReject hasValue sp#reject,
                request hasValue ?request] memberOf sp#globalAnswer)
     then
      (add(_[request hasValue ?request,
             succeed hasValue sp#failure] memberOf sp#compositeGoal))


  if ((?prodConf[request hasValue ?request] memberOf sp#producerConfirmation) and
      (?shipConf[request hasValue ?request] memberOf sp#shipperConfirmation) and
      (?response[acceptReject hasValue sp#accept,
                 request hasValue ?request] memberOf sp#globalAnswer))
    then
      ((add(_[request hasValue ?request,
              shipConfirmation hasValue ?shipConf,
              prodConfirmation hasValue ?prodConf]
             memberOf sp#globalConfirmation))
       and
       (add(_[request hasValue ?request,
              succeed hasValue sp#success] memberOf sp#compositeGoal)))
        



/// The following are not included in the diagrammed orchestration:

 if (?pOffer[request hasValue ?request,
             acceptReject hasValue sp#rejected] memberOf sp#producerOffer)
    then ((add(_[acceptReject hasValue sp#rejected] memberOf sp#globalOffer))
          and
          (add(_[request hasValue ?request,
		     succeed hasValue sp#failure] memberOf sp#compositeGoal)))
  // If producer rejects the request, prepare a rejection for the user
  // as the Global Offer and define the goal as having failed.

  if (?sOffer[request hasValue ?request,
              acceptReject hasValue sp#rejected] memberOf sp#shipperOffer)
    then ((add(_[acceptReject hasValue sp#rejected] memberOf sp#globalOffer))
          and
          (add(_[request hasValue ?request,
                 acceptance hasValue sp#rejected] memberOf sp#producerAnswer))
	    and
          (add(_[request hasValue ?request,
                 succeed hasValue sp#failure] memberOf sp#compositeGoal)))
  // If shipper rejects the request, prepare a rejection for the user
  // as the Global Offer and for the producer as a Producer Answer, 
  // and define the goal as having failed.