BookingManager_api_single.tla

--------------------------- MODULE BookingManager ---------------------------
\* 
\*  This is my TLA+ specification of a restaurant booking manager exercice
\* 
\* FEATURES:
\* - A user can add tables
\* - A table can get unlimited people (1..n)
\* - A user can set the time range of the open hours
\* - A user can add, edit or cancel reservations
\* 
EXTENDS Naturals, FiniteSets
\* ======================================
\* SETUP :
\* ======================================
\* Tables available in the restaurant
\* Tables == 1..5
\* Opening hours of the restaurant
\* OpeningHours == 7..12
CONSTANTS Tables, OpeningHours
\* ======================================
VARIABLES Reservations, FreeSlots
vars == <<Reservations, FreeSlots>>
\* ======================================
\* Slots are the Possible combinations of a single reservation
\* e.g. : <1, 7> : slot that associates Table 1 to 7:00pm
\*        <1, 8> : slot that associates Table 2 to 8:00pm, etc
Slots == Tables \X OpeningHours

\* Actions
Reserve(table, hour) == 
    /\ <<table, hour>> \in FreeSlots
    /\ Reservations' = Reservations \cup {<<table, hour>>}
    /\ FreeSlots' = FreeSlots \ {<<table, hour>>}

CancelReservation(table, hour) ==
    /\ <<table, hour>> \in Reservations
    /\ Reservations' = Reservations \ {<<table, hour>>}
    /\ FreeSlots' = FreeSlots \cup {<<table, hour>>}

EditReservation(oldTable, oldHour, newTable, newHour) == 
    /\ <<oldTable, oldHour>> \in Reservations 
    /\ <<newTable, newHour>> \in FreeSlots 
    /\ Reservations' = (Reservations \ {<<oldTable, oldHour>>}) \cup {<<newTable, newHour>>}
    /\ FreeSlots' = (FreeSlots \ {<<newTable, newHour>>}) \cup {<<oldTable, oldHour>>}
\* ======================================

Init ==
    /\ Reservations = {}
    /\ FreeSlots = Slots
    
Next == \E <<A, B>> \in Slots \X Slots : \/ Reserve(A[1], A[2])
                                         \/ CancelReservation(A[1], A[2])
                                         \/ EditReservation(A[1], A[2], B[1], B[2])

Fairness ==
    /\ \A <<t, h>> \in Slots : WF_vars(Reserve(t, h))
    /\ \A <<t, h>> \in Slots : WF_vars(CancelReservation(t, h))
    /\ \A <<old, new>> \in Slots \X Slots : WF_vars(EditReservation(old[1], old[2], new[1], new[2]))

\* ======================================

Spec == Init /\ [][Next]_vars /\ Fairness

\* ======================================

TypeCheck ==
    \* A reservation is defined as a table that
    \* is booked for an opening hour
    \* i.e. : a reservation is a booked slot 
    /\ Reservations \in SUBSET Slots
    /\ FreeSlots \in SUBSET Slots

\* Invariants

\* Checks at any point in time that :
\* A slot that has been reserved should never be 
\* available / free at the same time
ReservationsAndFreeSlotsShouldNeverOverlap ==
    /\ \A r \in Reservations : r \notin FreeSlots

\* Checks if the restaurant capacity is respected
\* the sum of available slots and reserved slots
\* never exceed the restaurant's capacity (total slots)
FreeAndReservedSlotsDoNotExceedRestaurantCapacity ==
    /\ Cardinality(FreeSlots) + Cardinality(Reservations) = Cardinality(Slots)

Invariants == 
    /\ ReservationsAndFreeSlotsShouldNeverOverlap
    /\ FreeAndReservedSlotsDoNotExceedRestaurantCapacity 


\* All free slots eventually get reserved
SlotsGetReserved ==
    \A s \in Slots : s \in FreeSlots ~> s \in Reservations

THEOREM Spec => [] Invariants
THEOREM Spec => [] TypeCheck
THEOREM Spec => SlotsGetReserved 
=============================================================================
\* Modification History
\* Last modified Sat Mar 05 13:39:07 CET 2022 by youne
\* Created Sat Mar 05 08:35:16 CET 2022 by youne