Платформа Event-B Rodin, Моделирование отношений для гостиничной системы

Question

Я новичок в Event-B и пытаюсь смоделировать гостиничную систему. В контексте у меня есть набор комнат для бронирования Клиент, который может сделать бронирование, регистрацию, выезд и отмену. У меня также есть Разрешение, когда комната пуста или занята, и варианты это означают, что в отеле есть разные типы номеров, такие как одна кровать, двуспальная кровать и т. д.

Это мой контекст:

          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

И моя машина:

room_numbers сначала отображаются как пустые комнаты.vacant_room показывает, занята она или ПУСТА.isBooked - связь между клиентом и номером, который выбрал наш клиент.

      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

У меня проблемы с резервированием этой линии -> grd5: room_number < room_numbers(r)что не так с этой строкой? У меня другие проблемы с резервированием, но с inv6. Тот же инв, но в отмене. Inv5 - регистрация и inv6 в оформлении. Я также хочу немного улучшить его и хочу знать, как я могу выразить вакантную_комнату с точки зрения номеров комнат и, таким образом, я удалю это РАЗРЕШЕНИЕ, когда она ЗАНЯТА и ПУСТА. Может быть, вы знаете, как сделать его лучше?

Я пытался наладить отношения между разными типами комнат и заказчиком, но теперь это выглядит не так, как я ожидал. Думаю немного обновить и есть идеи. Я думал, что room_numbers нужно уменьшить и создать постоянную функцию для vacant_room, чтобы показать максимальное количество свободных комнат и, возможно, назначить ее один раз с переменной room_numbers. А переменную vacant_room выразить через room_numbers. Но возникает вопрос, как я могу сделать отношения между клиентом?