In order to further illustrate Full Maude's object-oriented features, we specify a simple rent-a-car store example. Several rules in this specification have variables in their righthand sides or conditions not present in their lefthand sides; therefore, these rules are not directly executable by the rewrite engine and are declared as nonexecutable. In order to run the object-oriented system, we will have to use strategies; a possible such strategy will be presented in Section 15.6.
The regulations of the system, especially those that govern the rental processes, are the following:
Let us begin with the static aspects of this system, i.e., with its structure. We can identify three main classes, namely the store, customer, and car classes. There are three kinds of cars: economy, mid-size, and full-size cars.
Customers may rent cars. This relationship may be represented by a Rental class which, in addition to references to the objects involved in the relationship, has some extra attributes. The system also requires some control over time, which we get with a class representing calendars that provides the current date and simulates the passage of time.
The Customer class has three attributes, namely, suspended, cash, and debt to keep track of, respectively, whether he is suspended or not, the amount of cash that the customer currently has, and his debt with the store. Such a class is defined by the following Maude declaration:
class Customer | cash : Nat, debt : Nat, suspended : Bool .
The attribute available of the Car class indicates whether the car is currently available or not, and rate records the daily rental rate. We model the different types of cars for rent by three different subclasses, namely, EconomyCar, MidSizeCar and FullSizeCar.
class Car | available : Bool, rate : Nat . class EconomyCar . class MidSizeCar . class FullSizeCar . subclasses EconomyCar MidSizeCar FullSizeCar < Car .
Each object of class Rental will establish a relationship between a customer and a car, whose identifiers are kept in attributes customer and car, respectively. In addition to these, the class Rental is also declared with attributes deposit, pickUpDate, and dueDate to store, respectively, the amount of money left as a deposit by the customer, the date in which the car is picked up by the customer, and the date in which the car should be returned to the store.
class Rental | deposit : Nat, dueDate : Nat, pickUpDate : Nat,
customer : Oid, car : Oid .
Given the simple use that we are going to make of dates, we can represent them, for example, as natural numbers. Then, we may have a calendar object that keeps the current date and gets increased by a rewrite rule as follows:
class Calendar | date : Nat .
rl [new-day] :
< O : Calendar | date : F >
=> < O : Calendar | date : F + 1 > .
We do not worry here about the frequency with which the date gets increased, the possible synchronization problems in a distributed setting, or with any other issues related to the specification of time. See the papers [63,65] on the specification of real-time systems in rewriting logic and Maude for a discussion on these issues.
Four actions can be identified in our example:
The rental of a car by a customer is specified by the car-rental rule below, which involves the customer renting the car, the car itself (which must be available, i.e., not currently rented), and a calendar object supplying the current date. The rental can take place if the customer is not suspended, that is, if her identifier is not in the set of identifiers of suspended customers of the store, and if the customer has enough cash to make the corresponding deposit. Notice that a customer could rent a car for less time she really is going to use it on purpose, because either she does not have enough money for the deposit, or prefers making a smaller deposit. According to the description of the system, the payment takes place when returning the car, although there is an extra charge for the days the car was not reserved.
crl [car-rental] :
< U : Customer | cash : M, suspended : false >
< I : Car | available : true, rate : Rt >
< C : Calendar | date : Today >
=> < U : Customer | cash : M - Amnt >
< I : Car | available : false >
< C : Calendar | >
< A : Rental | pickUpDate : Today, dueDate : Today + NumDays,
car : I, deposit : Amnt, customer : U, rate : Rt >
if Amnt := Rt * NumDays /\ M >= Amnt
[nonexec] .
Note that, as already mentioned, those attributes of an object that are not relevant for a rule do not need to be mentioned. Attributes not appearing in the righthand side of a rule will maintain their previous values unmodified. Furthermore, since the variables A and NumDays appear in the righthand side or condition of the rule but not in its lefthand side, this rule has to be declared as nonexec. Note as well the use of the attributes customer and car in objects of class Rental, which makes explicit that a rental relationship is between the customer and the car specified by these attributes.
A customer returning a car late cannot be forced to pay the total amount of money due at return time. Perhaps she does not have such an amount of money in hand. The return of a rented car is specified by the rules below. The first rule handles the case in which the car is returned on time, that is, the current date is smaller or equal to the due date, and therefore the deposit is greater or equal to the amount due.
crl [on-date-car-return] :
< U : Customer | cash : M >
< I : Car | rate : Rt >
< A : Rental | customer : U, car : I, pickUpDate : PDt,
dueDate : DDt, deposit : Dpst >
< C : Calendar | date : Today >
=> < U : Customer | cash : (M + Dpst) - Amnt >
< I : Car | available : true >
< C : Calendar | >
if (Today <= DDt) /\ Amnt := Rt * (Today - PDt)
[nonexec] .
In this case, part of the deposit needs to be reimbursed. We can see that the Rental object disappears in the righthand side of the rule, that is, it is removed from the set of rentals and the availability of the car is restored.
The second rule deals with the case in which the car is returned late.
crl [late-car-return] :
< U : Customer | debt : M >
< I : Car | rate : Rt >
< A : Rental | customer : U, car : I, pickUpDate : PDt,
dueDate : DDt, deposit : Dpst >
< C : Calendar | date : Today >
=> < U : Customer | debt : (M + Amnt) - Dpst >
< I : Car | available : true >
< C : Calendar | >
if DDt < Today *** it is returned late
/\ Amnt := Rt * (DDt - PDt)
+ ((Rt * (Today - DDt)) * (100 + 20)) quo 100
[nonexec] .
In this case, the customer's debt is increased by the portion of the amount due not covered by the deposit.
Debts may be paid at any time, the only condition being that the amount paid is between zero and the amount of money owed by the customer at that time.
crl [pay-debt] :
< U : Customer | debt : M, cash : N >
=> < U : Customer | debt : M - Amnt, cash : N - Amnt >
if 0 < Amnt /\ Amnt <= N /\ Amnt <= M
[nonexec] .
Customers who are late in returning a rented car or in paying their debts ``may'' be suspended. The first rule deals with the case in which a customer has a pending debt, and the second one handles the case in which a customer is late in returning a rented car.
crl [suspend-late-payers] :
< U : Customer | debt : M, suspended : false >
=> < U : Customer | suspended : true >
if M > 0 .
crl [suspend-late-returns] :
< U : Customer | suspended : false >
< I : Car | >
< A : Rental | customer : U, car : I, dueDate : DDt >
< C : Calendar | date : Today >
=> < U : Customer | suspended : true >
< I : Car | >
< A : Rental | >
< C : Calendar | >
if DDt < Today .
Since the system is not terminating, and there are several rules with variables in their righthand sides or conditions not present in their lefthand sides and not satisfying the admissibility conditions discussed in Section 5.3, strategies are necessary for controlling its execution. We can define many different strategies and use them in many different ways (see Section 11.5); a concrete possibility will be described later in Section 15.6.