'Event-B Rodin platform, Modelling relations for hotel system

I'm a beginner on Event-B and I'm trying to model a hotel system. In context I have set of Rooms for booking Customer who can make a reservation, checkin, checkout and cancellation. I also have Permission when the room is Empty or Occupied and Options it means that the hotel has different types of room such as one beds, double beds, etc.

This is my context:

    CONTEXT
        HotelData   ›
    SETS
    ⚬   ROOMS    ›
    ⚬   CUSTOMERS    ›
    ⚬   PERMISSION   ›
    ⚬   OPTION   ›
    CONSTANTS
    ⚬   ROOM_NUMBER  ›
    ⚬   OCCUPIED     ›
    ⚬   EMPTY    ›
    ⚬   Options  ›
    AXIOMS
    ⚬   axm1:   finite(ROOMS) not theorem ›
    ⚬   axm3:   ROOM_NUMBER ∈ ROOMS → ℕ not theorem ›
    ⚬   axm4:   partition(PERMISSION, {OCCUPIED}, {EMPTY}) not theorem ›
    ⚬   axm5:   Options ∈ ROOMS ↔ OPTION not theorem ›
    ⚬   axm6:   dom(Options) = ROOMS not theorem ›
    ⚬   axm7:   ran(Options) = OPTION not theorem ›
    END

And my machine:

room_numbers is showed at the first time as empty rooms. vacant_room displayed whether it is OCCUPIED or EMPTY. isBooked - relation between customer and room which our customer chose.

MACHINE
        HotelSystemBooking  ›
    SEES
    ⚬    HotelData 
    VARIABLES
    ⚬   isBooked     ›
    ⚬   customer     ›
    ⚬   vacant_room  ›
    ⚬   r_number     ›
    ⚬   room_numbers     ›
    INVARIANTS
    ⚬   inv1:   isBooked ∈ CUSTOMERS ↔ ROOMS not theorem ›
    ⚬   inv2:   customer ∈ ℙ(CUSTOMERS) not theorem ›
    ⚬   inv3:   vacant_room ∈ PERMISSION not theorem ›
    ⚬   inv4:   r_number ∈ ROOMS ⇸ ℙ(ℕ) not theorem ›
    ⚬   inv5:   room_numbers ∈ ROOMS ⇸ ℕ not theorem ›
    ⚬   inv6:   ∀ f · f ∈ ROOMS ∧ f ∈ ran(isBooked) ⇒ f ∈ dom(r_number) ∧ f ∈ dom(room_numbers) ∧ f ∈ dom(Options) not theorem ›
    ⚬   inv7:   ¬(vacant_room = OCCUPIED ∧ vacant_room = EMPTY) not theorem ›
    EVENTS
    ⚬   INITIALISATION:  not extended ordinary ›
        THEN
        ⚬   act1:   isBooked ≔ ∅ ›
        ⚬   act2:   customer ≔ ∅ ›
        ⚬   act3:   vacant_room ≔ EMPTY ›
        ⚬   act4:   r_number ≔ ∅ ›
        ⚬   act5:   room_numbers ≔ ROOMS × {0} ›
        END

    ⚬   reservation:     not extended ordinary ›
        ANY
        ⚬   c    ›
        ⚬   r    ›
        ⚬   room_number  ›
        WHERE
        ⚬   grd1:   c ∈ CUSTOMERS not theorem ›
        ⚬   grd2:   r ∈ ROOMS not theorem ›
        ⚬   grd3:   room_number ∈ ℕ not theorem ›
        ⚬   grd4:   r ∈ dom(r_number) ∧ room_number ∉ r_number(r) not theorem ›
        ⚬   grd5:   room_number < room_numbers(r) not theorem ›
        THEN
        ⚬   act1:   isBooked ≔ isBooked ∪ {c ↦ r} ›
        ⚬   act2:   r_number(r) ≔ r_number(r) ∪ {room_number} ›
        END

    ⚬   cancellation:    not extended ordinary ›
        ANY
        ⚬   c    ›
        ⚬   r    ›
        ⚬   room_number  ›
        WHERE
        ⚬   grd1:   c ∈ CUSTOMERS ∧ r ∈ ROOMS ∧ (c ↦ r) ∈ isBooked not theorem ›
        ⚬   grd2:   r ∈ dom(room_numbers) ∧ room_number < room_numbers(r) not theorem ›
        ⚬   grd3:   r ∈ dom(r_number) ∧ room_number ∈ r_number(r) not theorem ›
        THEN
        ⚬   act1:   isBooked ≔ isBooked ∖ {c ↦ r} ›
        ⚬   act2:   r_number(r) ≔ r_number(r) ∖ {room_number} ›
        END

    ⚬   checkin:     not extended ordinary ›
        ANY
        ⚬   c    ›
        ⚬   size1    ›
        ⚬   r    ›
        WHERE
        ⚬   grd1:   c ∈ CUSTOMERS ∧ c ∈ dom(isBooked) not theorem ›
        ⚬   grd2:   size1 ∈ ℕ not theorem ›
        ⚬   grd3:   r ∈ ROOMS not theorem ›
        THEN
        ⚬   act1:   customer ≔ {c} ∪ dom(isBooked)  ›
        ⚬   act2:   room_numbers ≔ room_numbers ∪ {r ↦ size1} ›
        END

    ⚬   checkout:    not extended ordinary ›
        ANY
        ⚬   c    ›
        ⚬   r    ›
        WHERE
        ⚬   grd1:   c ∈ CUSTOMERS ∧ c ∈ dom(isBooked) ∧ r ∈ ROOMS ∧ (c ↦ r) ∈ isBooked not theorem ›
        THEN
        ⚬   act1:   isBooked ≔ {c} ⩤ isBooked ›
        ⚬   act2:   room_numbers ≔ {r} ⩤ room_numbers ›
        ⚬   act3:   r_number ≔ {r} ⩤ r_number ›
        END

    ⚬   reservation_query:   not extended ordinary ›
        ANY
        ⚬   r    ›
        WHERE
        ⚬   grd1:   r ∈ ROOMS not theorem ›
        THEN
        ⚬   act1:   customer ≔ isBooked∼[{r}] ›
        END

    ⚬   reservation_occupied:    not extended ordinary ›
        ANY
        ⚬   c    ›
        ⚬   o    ›
        WHERE
        ⚬   grd1:   c ∈ CUSTOMERS ∧ o ∈ OPTION ∧ (c ↦ o) ∈ isBooked;Options not theorem ›
        THEN
        ⚬   act1:   vacant_room ≔ OCCUPIED ›
        END

    ⚬   reservation_free:    not extended ordinary ›
        ANY
        ⚬   c    ›
        ⚬   o    ›
        WHERE
        ⚬   grd1:   c ∈ CUSTOMERS ∧ o ∈ OPTION ∧ (c ↦ o) ∉ isBooked;Options not theorem ›
        THEN
        ⚬   act1:   vacant_room ≔ EMPTY ›
        END

    END

I have some problems with reservation this line -> grd5: room_number < room_numbers(r) what's wrog with that line? I have other problems in reservation but with inv6. The same inv but in cancellation. Inv5 - checkin and inv6 in checkout. I also want to improve it a little and want to know how can I express vacant_room in terms of room_numbers and thus I will remove that PERMISSION when it is OCCUPIED and EMPTY. Maybe you know how to make it better?

I tried to make a relations between different types of rooms and the customer but now it looks not so much as I expected. I think to update it a little bit and have some ideas. I thought that room_numbers need to decrease and to create a constant function for vacant_room to show maximum number of vacant rooms and maybe assign it once with room_numbers variable. And vacant_room variable express through room_numbers. But there is a question how can I make the relation between customer?

modelingrelationevent-b


Sources

This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.

Source: Stack Overflow

Solution Source

Related Questions