BookingManager_api_customers.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
\* Users/Customers of the restaurant
\* Users/Customers == 1..4
CONSTANTS Tables, OpeningHours, Users
\* ======================================
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(user, table, hour) == 
    /\ <<table, hour>> \in FreeSlots
    /\ Reservations' = [ Reservations EXCEPT ![user] = <<table, hour>> ]
    /\ FreeSlots' = FreeSlots \ {<<table, hour>>}

CancelReservation(user, table, hour) ==
    /\ Reservations[user] = <<table, hour>>
    /\ Reservations' = [ Reservations EXCEPT ![user] = <<>> ]
    /\ FreeSlots' = FreeSlots \cup {<<table, hour>>}

EditReservation(user, oldTable, oldHour, newTable, newHour) == 
    /\ Reservations[user] = <<oldTable, oldHour>> 
    /\ <<newTable, newHour>> \in FreeSlots 
    /\ Reservations' = [ Reservations EXCEPT ![user] = <<newTable, newHour>> ]
    /\ FreeSlots' = (FreeSlots \ {<<newTable, newHour>>}) \cup {<<oldTable, oldHour>>}

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


\*FreeUsers == { CHOOSE u \in Users : Reservations[u] = <<>> }


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

Fairness ==
    /\ \A <<u, t, h>> \in Users \X Slots : WF_vars(Reserve(u, t, h))
    /\ \A <<u, t, h>> \in Users \X Slots : WF_vars(CancelReservation(u, t, h))
    /\ \A <<u, old, new>> \in Users \X Slots \X Slots : WF_vars(EditReservation(u, 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 bu a user (customer)
    \* i.e. : a reservation is a user who booked a timeslot 
    /\ Reservations \in [ u \in Users |-> Slots ]
    /\ FreeSlots \in SUBSET Slots

\* Invariants

\* Checks at any point in time that :
\* There should never be two customers that manage to book
\* the same table for the same timeslot (any 2 customers 
\* MUST have different reservations)
TwoCustomersShouldNotBookTheSameReservation ==
    /\ \A slot \in Slots : ~ ( \A <<a, b>> \in Users \X Users : Reservations[a] = slot /\ Reservations[b] = slot /\ a /= b ) 

\* 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({ \A <<s, u>> \in Slots \X Users : Reservations[u] /= <<>> }) = Cardinality(Slots)

Invariants == 
    /\ TwoCustomersShouldNotBookTheSameReservation
\*    /\ 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 Fri Mar 11 18:20:15 CET 2022 by youne
\* Created Sat Mar 05 08:35:16 CET 2022 by youne