// Hotel Example (2)
// in this version of the hotel system, there are two additional interactions: 
//    (a) the client must enter the restaurant before eating, and 
//    (b) the room must be cleaned before becoming free again.
// Correspondingly, the state diagram of the overall system becomes quite complex.

// state machine of the client: it has only one state, all client actions are possible any time.
CLIENT =  (checkIn -> CLIENT | checkOut -> CLIENT | enter -> CLIENT |
          eat -> CLIENT | payCash -> CLIENT | chargeRoom -> CLIENT).

// state machine of a restaurant. The alphabet of this LTS is {enter, eat, payCash, chargeRoom}
RESTAURANT = (enter -> ORDER),
   ORDER = (eat -> DONE),
   DONE = (payCash -> RESTAURANT | chargeRoom -> RESTAURANT). 

// state machine of a room. The alphabet of this LTS is {checkIn, checkOut, chargeRoom, clean}
ROOM = (checkIn -> OCCUPIED),
   OCCUPIED = (checkOut -> FREED | chargeRoom -> OCCUPIED),
   FREED = (clean -> ROOM).

// The system consists of one client, one restaurant and one room
||SYSTEM = (CLIENT || RESTAURANT || ROOM).
// List of interactions in this system:
// (a) Rendezvous involving the CLIENT and the RESTAURANT: enter, eat, payCash
// (b) Rendezvous involving the CLIENT and the ROOM: checkIn, checkOut
// (c) Rendezvous involving all three objects: chargeRoom
// (d) interaction involving only the ROOM: clean