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:

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.

The values shown in the matrix depend on the mismatch list detected between the carRental and the user protocols. States which have few mismatches, e.g., states u1 and c1, have higher compatibility degrees than those having more mismatches, e.g., states u2 and c2. Since many incompatibility issues are detected, the protocols have a low global compatibility degree which is equal to 0.26 (t=0.7).