Specification of a car rental company

SPECIFICATION Company

TEMPLATE Customer
DATA TYPES
  String;
ATTRIBUTES
  Name : string;
  Address : string;
EVENTS
  BIRTH createCustomer(aName : string, anAddress : string);
  updateAddress(anAddress : string);
VALUATION
  [ createCustomer ] Name = aName, Address = anAddress;
  [ updateAddress ] Address = anAddress;
BEHAVIOR
  PROCESS Customer =
    ( createCustomer -> CustomerUpdate );
  PROCESS CustomerUpdate =
    ( { Address <> anAddress : "new address `" + anAddress + 
	"' must not be equal to old one" } 
	updateAddress -> CustomerUpdate );
END TEMPLATE

// ---------------------

TEMPLATE Car
DATA TYPES
  String, Int, Bool;
ATTRIBUTES
  CarNo : string;
  CarCat : int;     // 1..5
  Brand : string;
  Available : bool;
EVENTS
  BIRTH createCar(aCarNo : string, aCarCat : int, aBrand : string);
  pickUp;
  return;
CONSTRAINTS
  1 <= CarCat AND CarCat <= 5;
VALUATION
  [ createCar ]
      CarNo = aCarNo, CarCat = aCarCat, Brand = aBrand, Available = TRUE;
  [ pickUp ] Available = FALSE;
  [ return ] Available = TRUE;
BEHAVIOR
  PROCESS Car =
    ( createCar -> CarAvailable );
  PROCESS CarAvailable =
    ( { Available : "car is not available for pickUp" } 
	pickUp -> CarAway );
  PROCESS CarAway = 
    ( { NOT Available : "car is not away" } 
	return -> CarAvailable );
END TEMPLATE

// ---------------------

TEMPLATE Booking
DATA TYPES
  String, Int, Bool;
TEMPLATES
  Customer, Car;
ATTRIBUTES
  TheCustomer : customer;
  TheCar : car;
  BookingCat : int;   // 1..5
  StartDay : int;     // YYYYMMDD
  EndDay : int;       // YYYYMMDD
  IsClosed : bool;
  DERIVED IsOpen : bool;
  DERIVED IsCurrent : bool;
EVENTS
  BIRTH createBooking(aCustomer : customer, aCat : int,
                      aStartDay : int, anEndDay : int);
  makeCurrent(aCar : car);
  close;
CONSTRAINTS
  1 <= BookingCat AND BookingCat <= 5;
  19900101 <= StartDay AND StartDay <= EndDay AND EndDay <= 20001231;
VALUATION
  [ createBooking ]
      TheCustomer = aCustomer, BookingCat = aCat,
      StartDay = aStartDay, EndDay = anEndDay,
      IsClosed = FALSE;
  [ makeCurrent ] TheCar = aCar;
  [ close ] TheCar = NIL(car), IsClosed = TRUE;
DERIVATION
  IsOpen = UNDEF(TheCar) AND NOT(IsClosed);
  IsCurrent = DEF(TheCar) AND NOT(IsClosed);
BEHAVIOR
  PROCESS Booking =
    ( createBooking -> BookingOpen );
  PROCESS BookingOpen =
    ( { BookingCat <= CarCat(aCar) : "category of car is too low" } 
	makeCurrent -> BookingCurrent );
  PROCESS BookingCurrent =
    ( close -> BookingClosed );
  PROCESS BookingClosed = ( );
END TEMPLATE

// ---------------------

TEMPLATE Company
DATA TYPES
  String, Int;
TEMPLATES
  Customer, Car, Booking;
SUBOBJECTS
  Customers : MAP(CustomerNo : int, Customer : customer);
  Cars : MAP(CarNo : string, Car : car);
  Bookings : MAP(BookingNo : int, Booking : booking);
ATTRIBUTES
  Today : int;   // YYYYMMDD
  NextCustomerNo, NextBookingNo : int;
  DERIVED CurrentCustomersAndCars : BAG(TUPLE(Name : string, CarNo : string));
  DERIVED ReturnCarsMenu : BAG(string);
  DERIVED DeliverCarsMenu : 
      BAG(TUPLE(BookingNo : int, BookingCat : int,
                PossibleCars : BAG(TUPLE(CarNo : string, CarCat : int))));
EVENTS
  BIRTH create;
  addCustomer(aName : string, anAddress : string);
  addBooking(aCustomer : customer, aCat : int,
             aStartDay : int, anEndDay : int);
  incTime(aDay : int);
  returnCar(aCarNo : string);
  closeReturnCars;
  addCar(aCarNo : string, aCarCat : int, aBrand : string);
  deliverCar(aBookingNo : int, aCarNo : string);
  closeDeliverCars;
CONSTRAINTS
  NextCustomerNo >= 0;
  NextBookingNo >= 0;

  // make sure that each car is assigned to at most one booking
  FORALL (C IN Cars)
    (CNT(SELECT B
         FROM   B IN Bookings
         WHERE  TheCar(Booking(B)) = Car(C)) <= 1);
VALUATION
  [ create ]
      NextCustomerNo = 0, NextBookingNo = 0;
  [ addCustomer ]
      NextCustomerNo = NextCustomerNo + 1;
  [ addBooking ]
      NextBookingNo = NextBookingNo + 1;
  { aDay > 19000000 : "invalid date `" + STR(aDay) + "'" }
  [ incTime ]
      Today = aDay;
DERIVATION
  CurrentCustomersAndCars =
    SELECT Name(Customer(CUS)), CarNo(Car(CAR))
    FROM   CUS IN Customers, CAR IN Cars
    WHERE  EXISTS ( B IN Bookings )
               ( TheCustomer(Booking(B)) = Customer(CUS) AND
                 TheCar(Booking(B)) = Car(CAR) );

  ReturnCarsMenu =
    SELECT CarNo(TheCar(Booking(B)))
    FROM   B IN Bookings
    WHERE  EndDay(Booking(B)) <= Today AND IsCurrent(Booking(B));

  DeliverCarsMenu =
    SELECT BookingNo(B), BookingCat(Booking(B)),
           ( SELECT CarNo(Car(C)), CarCat(Car(C))
             FROM   C IN Cars
             WHERE  Available(Car(C)) AND
                    CarCat(Car(C)) >= BookingCat(Booking(B)) )
    FROM   B IN Bookings
    WHERE  StartDay(Booking(B)) = Today AND IsOpen(Booking(B));

INTERACTION
  addCustomer >>
    createCustomer(aName, anAddress) IN Customers(NextCustomerNo);
	// shortcut for: MAP_SEL(Customers(SELF), NextCustomerNo);

  addBooking >>
    createBooking(aCustomer, aCat, aStartDay, anEndDay) IN
	Bookings(NextBookingNo);

  // return car and close booking for this car
  returnCar >> return IN Cars(aCarNo),
    close IN SINGLE(SELECT Booking(B)
	            FROM   B IN Bookings
		    WHERE  CarNo(TheCar(Booking(B))) = aCarNo);

  addCar >> createCar(aCarNo, aCarCat, aBrand) IN Cars(aCarNo);

  // deliver car and mark booking as current for this car
  deliverCar >> pickUp IN Cars(aCarNo),
    makeCurrent(Cars(aCarNo)) IN Bookings(aBookingNo);

BEHAVIOR
  PROCESS Company =
    ( create -> SetTime );

  PROCESS SetTime =
    ( incTime -> AddCustomerOrBooking );

  PROCESS AddCustomerOrBooking =
    ( addCustomer -> AddCustomerOrBooking
    | { Today < aStartDay : "start day must be after today" } 
	addBooking -> AddCustomerOrBooking
    | { Today < aDay AND
        FORALL (B IN Bookings)
	  // don't skip start day of open bookings
          (IsOpen(Booking(B)) IMPLIES aDay <= StartDay(Booking(B)) AND
	  // don't skip past end day of current bookings
          IsCurrent(Booking(B)) IMPLIES aDay <= EndDay(Booking(B))) } 
        incTime -> ReturnCars );

  PROCESS ReturnCars =
    ( { aCarNo IN ReturnCarsMenu : 
	"car `" + STR(aCarNo) + "' not in ReturnCarsMenu" } 
	returnCar -> ReturnCars
    | { EMPTY(ReturnCarsMenu) : "there are still cars to return" }
	closeReturnCars -> DeliverCars );

  PROCESS DeliverCars =
    ( addCar -> DeliverCars
    | { aBookingNo IN ( SELECT BookingNo(B)
                        FROM   B IN Bookings
                        WHERE  StartDay(Booking(B)) = Today )
                   AND Available(Cars(aCarNo)) 
	: "no booking number `" + STR(aBookingNo) + "' or car not available" }
        // category is checked in Booking behavior
        deliverCar -> DeliverCars
    | { FORALL (B IN Bookings)
          ( StartDay(Booking(B)) = Today IMPLIES
            IsCurrent(Booking(B)) ) }
        closeDeliverCars -> AddCustomerOrBooking );
END TEMPLATE

Home|People|Teaching|Publications