Colored Petri nets modeling
Consider a travel agency that mediates hotel reservations. The following things can happen:
- The travel agency waits for customers to arrive and listen to their requests.
- Based on the request, several available hotels are presented to the customer. The presented ho-tels are locked for reservation up to five minutes.
- The customer has now three choices:
- He decides to change his request, the process continues at 1.
- He is not interested; the process finishes.
- He decides to book one of the hotels presented, the process continues at 4. This has to happen within the timeout; otherwise this step is not possible.
- Again, two things can happen:
- The travel date arrives, the customer visits the hotel, and the hotel transmits a charge to the travel agency. The process finishes.
- The booking is cancelled before the travel date arrives. The process finishes.
a) Model the process described as a coloured Petri net. Include all necessary guard functions, arc expressions, etc.
b) Discuss the problems that might arise from the timeout.
More information on colored Petri nets can be found in the book in chapter 4.2.3.