// Hotel V3 - including test sequences and checking of properties

// in this version, the checkIn and checkOut operations are rendezvous with all three system components, 
//    and the RESTAURANT LTS assures that checkIn and checkOut can only be performed 
//                when the client did not enter the restaurant.

// 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 | checkIn -> RESTAURANT | checkOut -> RESTAURANT),
   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: no interaction
// (c) Rendezvous involving all three objects: checkIn, checkOut, chargeRoom
// (d) interaction involving only the ROOM: clean

set All_interactions = {enter, checkIn, checkOut, eat, payCash, chargeRoom, clean}

Sequence_1 = (enter -> eat -> payCash -> checkIn -> checkOut -> END) + All_interactions.
||TEST_1 = (SYSTEM || Sequence_1).

Sequence_2 = (enter -> eat -> payCash -> checkIn -> checkOut -> Sequence_2) + All_interactions.
||TEST_2 = (SYSTEM || Sequence_2).

Sequence_3 = (enter -> eat -> checkIn -> chargeRoom -> checkOut -> clean -> Sequence_3) + All_interactions.
||TEST_3 = (SYSTEM || Sequence_3).

Sequence_4 = (checkIn -> enter -> eat -> chargeRoom  -> checkOut -> clean -> Sequence_4) + All_interactions.
||TEST_4 = (SYSTEM || Sequence_4).


property CHECK_A = (eat -> payCash -> CHECK_A).
||CHECKED_SYSTEM_A = (SYSTEM || CHECK_A).

property CHECK_B = (checkIn -> checkOut -> CHECK_B).
||CHECKED_SYSTEM_B = (SYSTEM || CHECK_B).