// Hotel Example

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

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

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

// 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: eat, payCash
// (b) Rendezvous involving the CLIENT and the ROOM: checkIn, checkOut
// (c) Rendezvous involving all three objects: chargeRoom