Iteration 1: Constraints

Five Important Constraints

On this page, we summarized the five most interesting constraints which are not covered by the domain model (version 1.1). This is the final version for submission.

---

1. Each FlexiBookSystem can only have one owner account

For each FlexiBookSystem:
sizeOf (select a from accounts such as a is typeOf OwnerAccount) <= 1

Logic: Here we make sure the system will only have one or zero (the system has not been booted yet) UserAccount instance.

2. Appointment cannot be updated or canceled by the customer on the day of the appointment

For each Appointment:
isCancellable(): Boolean = self.appointmentStartDate.isAfter(system.getCurrentDate());
implies isCancellable = true;

Logic: Here we make sure the Appointment can be cancelled only if its date is after today.

3. The system can only have one account logged in at a time

For each FlexiBookSystem:
sizeOf (select a from accounts such as a.isCurrentlyLoggedIn equals true) <= 1

For each FlexiBookSystem:
self.hasUserLoggedIn implies sizeOf (select a from accounts such as a.isCurrentlyLoggedIn equals true) equals 1

Logic: Here we make first make sure the total number of logged-in accounts is zero or one.
Then we make use of the state boolean "hasUserLoggedIn" to indicate the system now is full.

4. ServiceCombo cannot be the same as another ServiceCombo

For each FlexiBookSystem:
ForAll sc1,sc2 in self.services such that sc1,sc2 is TypeOf(ServiceCombo)
it is true that (sc1<>sc2) implies that (sc1.serviceName<>sc2.serviceName)
AND
ForAll sc1,sc2 in self.services such that sc1,sc2 is TypeOf(ServiceCombo)
it is true that (sc1<>sc2) implies that (sc1.otherServices exclude sc2.otherServices) is not empty

Logic: Here we make first make two different service combo objects must have different names. This is an easy check.
Then we emphasize the contents of the service combos must have different single-services by using "exclude".

5. Cannot make appointments during unavailable time

For each Appointment:
forAll v in Calendar.vacations:
implies isOnBusinessDay() AND isInBusinessHour() AND isInOpenTimeSlot() = true;

isOnBusinessDay(): Boolean = (self.appointmentStartDate.isAfter(v.endDate)) or
(self.appointmentStartDate.isBefore(v.startDate))

isInBusinessHour(): Boolean = [self.appointmentStartTime.isAfter(DailySchedule.openTime)
AND (self.appointmentStartTime + self.service.timeLength).isBefore(DailySchedule.lunchBreakStartTime)]
OR
[self.appointmentStartTime.isAfter(DailySchedule.lunchBreakEndTime)
AND (self.appointmentStartTime + self.service.timeLength).isBefore(DailySchedule.closeTime)]

isInOpenTimeSlot(): Boolean =
forAll a in (select a from Calendar.appointments such that a.appointmentStartDate equals self.appointmentStartDate)
if (a not equal to self) implies
[self.appointmentStartTime.isAfter(a.appointmentStartTime + a.service.downTimeStartAt)
AND (self.appointmentStartTime+ self.service.timeLength).isBefore(a.appointmentStartTime + a.service.downTimeEndAt)]
OR
[self.appointmentStartTime.isAfter(a.appointmentStartTime + a.service.timeLength)
AND (self.appointmentStartTime + self.service.timeLength).isBefore(a.appointmentStartTime)]

Logic: First, method "isOnBusinessDay()" makes sure the appointment date do NOT intersect with closed dates and vacations.
Then, method "isInBusinessHour()" makes sure the time slot of the appointment (service start -> service end) must be included by business hours.
The final method "isInOpenTimeSlot()" checks all appointments on the same date. When comparing all appointments on this date (except itself), the appointment must make sure:
1. Either it is included in other appointment's downtime
or 2. it does not intersect with others' time slots
Finally, a good appointment needs to satisfy ALL THREE CRITERIA!