Daniela/Rick's Travel Usecase
=============================

  Will not do the specification of the service as an object
  as I did for the transfer example. Will go directly to the
  process specification part. The spec below should be a reified formula
  sticking out of an action attribute like this:

    danielaTravel[
       ...
       action -> ${...process spec ...},
       ...
    ].


1. Three services: Atomic service case
--------------------------------------

	registerEvent(EventName,StartDate,EndDate)

  [*] I took the liberty to add ArrvlDate, for simplicity

	bookAir(From,To,DprtDate,ArrvlDate,RtrnDate)

	bookHotel(HtlName,Addr,CheckInDate,CheckOutDate)


1.1 Naive reusable (and hence single-shot) composition
------------------------------------------------------

  Is trivial in (C)TR:

    danielaDoIt(EventName,EventStartDate,EventEndDate,
                From,To,DprtDate,ArrvlDate,RtrnDate,
		HtlName,HtlAddr,HtlCheckInDate,
		HtlCheckOutDate)
	 :-
	 (
           registerEvent(EventName,EventStartDate,EventEndDate)
	   |
	   bookAir(From,To,DprtDate,ArrvlDate,RtrnDate)
	   |
	   bookHotel(HtlName,Addr,CheckInDate,CheckOutDate)
	 ),
	 EventStartDate = ArrvlDate,
	 ArrvlDate = CheckInDate,
	 CheckOutDate = RtrnDate,
	 RtrnDate = EventEndDate.


  This is not to say that this is going to run efficiently in
  all cases (although in this case it will). An important point
  is that various planning algorithms can be naturally specified
  in TR.
  We showed how an improved STRIPS can be specified - it is an
  executable spec that will produce an actual plan.
  Most likely Daniela et al composition algorithm can also be
  specified (not invented) in CTR.

1.2 "Traveller profile" specification
-------------------------------------

  In FLOWS this part wasn't specified, but Rick said profile would be
  some sort of temporal constraint.

  Three profiles:
    	  researcher: event->ticket->hotel
	  manager: ticket->meeting->hotel
	  tourist: hotel->ticket->event

  Profiles can be expressed as temporal constraints in the TR syntax
  (analogously to the FLOWS proposal, but seems simpler):

       researcher:
	      path,registerEvent(_,_,_),path
	        => path,bookAir(_,_,_,_,_),path
	      /\
	      path,bookAir(_,_,_,_,_),path
	         => path,bookHotel(_,_,_,_),path

       manager:
	       path,bookAir(_,_,_,_,_),path
	        => path,registerEvent(_,_,_),path
	       /\
	       path,registerEvent(_,_,_),path
	         => path,bookHotel(_,_,_,_),path

       traveler: analogously


  [*] a => b is defined as  ~a + b, where  + is a dual to the serial
      conjinction:  a+b = ~(~a, ~b)


  Invocation of danielaTravel on behalf of a researcher:

      danielaDoIt(EventName,EventStartDate,EventEndDate,
                  From,To,DprtDate,ArrvlDate,RtrnDate,
		  HtlName,HtlAddr,HtlCheckInDate,
		  HtlCheckOutDate)
      /\
      path,registerEvent(_,_,_),path => path,bookAir(_,_,_,_,_),path
      /\
      path,bookAir(_,_,_,_,_),path => path,bookHotel(_,_,_,_),path


2. Three services: Multistep case
---------------------------------

  Services are now composed of atomic parts. bookAir & bookLand
  are alternatives.

	registerEvent(EventName,StartDate,EndDate) 
	   - this is atomic, not defined by rules

	bookAir(From,To,DprtDate,ArrvlDate,HtlAddr,RtrnDate) :-
	   bookPlane(From,To,DprtDate,ArrvlDate,RtrnDate),
	   %% bookLimo: depatureAddr,dateLeave,arriveAddr,dateBack
	   bookLimo(To,ArrvlDate,HtlAddr,RtrnDate).

	bookLand(From,To,DprtDate,ArrvlDate,HtlAddr,RtrnDate) :-
	   bookTrain(From,To,DprtDate,ArrvlDate,RtrnDate),
	   bookLimo(To,ArrvlDate,HtlAddr,RtrnDate).

	bookAccommodation(Airport,HtlName,HtlAddr,
	                  CheckInDate,CheckOutDate) :-
	   bookHotel(HtlName,HtlAddr,CheckInDate,CheckOutDate),
	   %% bookHotelShuttle: date, from/to_city
	   bookHotelShuttle(CheckInDate,Airport,HtlAddr).

2.1  Naive multi-step composition
---------------------------------

       danielaDoIt2(EventName,EventStartDate,EventEndDate,
                 From,To,DprtDate,ArrvlDate,RtrnDate,
	  	 HtlName,HtlAddr,HtlCheckInDate,
		 HtlCheckOutDate)
          :-
          (
            registerEvent(EventName,EventStartDate,EventEndDate)
	    |
	    (
	      bookAir(From,To,DprtDate,ArrvlDate,HtlAddr,RtrnDate)
	      \/
	      bookLand(From,To,DprtDate,ArrvlDate,HtlAddr,RtrnDate)
	    )
	    |
	    bookHotel(HtlName,HtlAddr,CheckInDate,CheckOutDate)
          ),
          EventStartDate = ArrvlDate,
          ArrvlDate = CheckInDate,
          CheckOutDate = RtrnDate,
          RtrnDate = EventEndDate.

2.2 User profiles
-----------------

  Same as before. Almost. I suppose that now Air\/OrTravel plays
  the role of Air in the first example. So, we should define

         mainTransport(From,To,DprtDate,ArrvlDate,HtlAddr,RtrnDate) :-
     	      bookAir(From,To,DprtDate,ArrvlDate,HtlAddr,RtrnDate).
         mainTransport(From,To,DprtDate,ArrvlDate,HtlAddr,RtrnDate) :-
  	      bookLand(From,To,DprtDate,ArrvlDate,HtlAddr,RtrnDate).
  
  Then daniela2 is redefined as

         danielaDoIt2(EventName,EventStartDate,EventEndDate,
                 From,To,DprtDate,ArrvlDate,RtrnDate,
		 HtlName,HtlAddr,HtlCheckInDate,
		 HtlCheckOutDate)
             :-
             (
               registerEvent(EventName,EventStartDate,EventEndDate)
               |
                mainTransport(From,To,DprtDate,ArrvlDate,HtlAddr,RtrnDate),
               |
                bookHotel(HtlName,HtlAddr,CheckInDate,CheckOutDate)
             ),
             EventStartDate = ArrvlDate,
             ArrvlDate = CheckInDate,
             CheckOutDate = RtrnDate,
             RtrnDate = EventEndDate.       

  Then profile for the manager will be

	      path,mainTransport(_,_,_,_,_,_),path
			   => path,registerEvent(_,_,_),path
	      /\
	      path,registerEvent(_,_,_),path
			   => path,bookHotel(_,_,_,_),path


   [*] This is a correct specification, which encompasses all possible
       interleavings. Applying profiles will allow only the interleavings
       that are consistent with the profile.

   [*] This is executable specification. Not claiming that CTR proof theory
       gives a better algorithm than the Daniela's.
       It is a better logical specification. It can be realized via a
       number of specialized algorithms.