Car rental
This system provides a service for car rental and an example of user requirements.
The service CarRental can receive a car rental request (request?), and returns the availability of the specified car for the given dates (reply!). Such a request can be received and replied several times until reservation (book?). In this case, the service confirms the reservation (book!) by sending an identifier.
The user requirements start with the search of a car (searchCar!), and then he/she submits some dates to check availability of the car for this period (searchDate!). After reception of an answer (reply?), the user can internally decide (using tau actions) to either submit another search (searchCar!, searchDate!) or reserve the car (resp. reserve! and confirmation with reserve?).
The Compatibility Matrix:
![](style/matrixCarRental.png)
Analysis:
Considering the unspecified-receptions compatibility notion, the carRental and the user protocols present several mismatches (incompatibility issues). Let us comment some of these mismatches:
- Message names: this mismatch can occur when messages have different names, e.g., searchCar! and request?.
- One to n correspondences: this mismatch can be detected in the case of one message which matches n (n>1) messages, e.g., message request? matches messages searchCar! and searchDate!.
- Parameter types: this mismatch can occur when the emitted and received parameter lists do not share the same types, e.g., resp:tresp and resp:bool.