Salon Appointment Booking App — a FizzBee walkthrough

Individual seeking to book a salon service.

Service provider whose availability is managed in the system.

Select a stylist and time slot to schedule a service.

Actors: Customer

Set and update the times when they are available for bookings.

Actors: Stylist

Global catalog (all stylists offer the same services/prices)Per-stylist catalog (each stylist defines their own services/prices)

One-at-a-time (1:1)Concurrent (allow overlapping bookings)

Manages the salon operations, stylist accounts, and global configurations.

Instantly confirmed (system auto-accepts based on availability)recommendedManual approval required (requests remain pending until accepted)

Yes, customers can cancel via the apprecommendedNo, they must contact the salon directly

Yes, there is a strict cutoff timerecommendedNo, they can cancel right up to the appointment time

Add new stylists, update their details, or deactivate them.

Actors: Salon Owner / Admin

Define the standardized list of services, durations, and prices for the salon.

Actors: Salon Owner / Admin

Customer views their upcoming and past appointment history.

Actors: Customer

Stylist views their daily or weekly booked appointments.

Actors: Stylist

Customer cancels an upcoming appointment.

Actors: Customer

Stylist or admin cancels a customer's appointment (e.g., due to illness or emergency).

Actors: Stylist

Yes, services need configured buffer times between appointmentsrecommendedNo, appointments can be booked strictly back-to-back based only on service duration

Yes, send automated notifications (Email/SMS)recommendedNo, users will check the app manually

Generating spec
Quick checks
Extensive verification

Automatically cancel all their upcoming appointmentsPrevent removal/deactivation if they have upcoming appointmentsrecommendedKeep the appointments but require them to be reassigned to another stylist

Reassign an existing appointment to a different stylist.

Actors: actor_owner

Automatically cancel appointments booked for this servicePrevent removal of the service if it is booked in upcoming appointmentsKeep existing appointments as-is, but hide the service from new bookings (Soft Delete)recommended

Yes, removing the availability automatically cancels the overlapping appointmentNo, the system prevents removing availability if an appointment is bookedrecommended

Reassignment must be done immediately (blocks deactivation until resolved)recommendedAppointments can be placed in an 'unassigned' state to be handled later

Strictly enforce (reassignment blocked if the new stylist is unavailable)recommendedAdmin override (allow reassignment even if it creates conflicts/double-bookings)

Generating spec
Quick checks
Extensive verification

Behavior Model v1Open ↗

Behavior scenarios

Shared setup

Walkthrough
1. The owner adds a new stylist (Stylist#0) to the salon roster.
2. The owner adds a service (svc0) to the global catalog.
3. Stylist#0 adds an availability slot (slot0) to their schedule.
4. All participants' views are updated to reflect the new stylist, service, and availability.
Trace
```
1. Owner#0.AddStylist
2. Owner#0.AddService
3. Stylist#0.AddAvailability
    slot=slot0
4. Owner#0.Refresh
5. Stylist#0.Refresh
6. Customer#0.Refresh
7. Customer#1.Refresh
```
Walkthrough (from Setup A)
1. Customer#0 selects the service and the available slot to book an appointment.
2. The system views update to show the slot is now occupied and the appointment is confirmed.
Trace
```
8. Customer#0.BookAppointment
    svc=svc0
    sched={stylist=Stylist#0, slot=slot0}
9. Owner#0.Refresh
10. Stylist#0.Refresh
11. Customer#0.Refresh
12. Customer#1.Refresh
```

Scenarios

Walkthrough (from Setup A)
1. Customer#0 selects service svc0 and Stylist#0's available slot0 to book their appointment.
2. The system records the appointment, linking it to the customer and the specific stylist and slot.
Trace
```
8. Customer#0.BookAppointment
    svc=svc0
    sched={stylist=Stylist#0, slot=slot0}
    expect: db.appointments contains record with id=appt0
    expect: db.appointments[appt0].customer == Customer#0
    expect: db.appointments[appt0].service == svc0
```
Verifies: AppointmentInSchedule (always), AppointmentStylistActive (always), CanBookAppointment (exists), implements exp_availability_constraint
Walkthrough (from Setup B)
1. Customer#1 attempts to book an appointment for the same stylist and slot (Stylist#0, slot0).
2. The system blocks the booking because the slot is no longer available in the authoritative schedule.
Trace
```
13. Customer#1.BookAppointment
    svc=svc0
    sched={stylist=Stylist#0, slot=slot0}
    expect: action disabled by require (len([a for a in self.appointments if a.stylist == stylist_id and a.slot == slot]) == 0)
```
Verifies: StylistNoOverlap (always), implements exp_no_double_booking
Walkthrough (from Setup B)
1. The owner removes service svc0 from the global catalog.
2. While the service is no longer in the catalog for new bookings, the existing appointment (appt0) still correctly references svc0.
Trace
```
13. Owner#0.RemoveService
    svc=svc0
    expect: svc0 not in db.catalog
14. System#0.Refresh
    expect: db.appointments[appt0].service == svc0
```
Verifies: implements exp_service_soft_delete
Walkthrough (from Setup B)
1. Stylist#0 attempts to remove their availability for slot0.
2. The system blocks the removal because an active appointment is already scheduled for that specific slot.
Trace
```
13. Stylist#0.RemoveAvailability
    slot=slot0
    expect: action disabled by require (len([a for a in self.appointments if a.stylist == stylist_id and a.slot == slot]) == 0)
```
Verifies: AppointmentInSchedule (always), implements exp_avail_block_removal
Walkthrough (from Setup B)
1. The owner removes Stylist#0 from the active roster.
2. The system deactivates the stylist and clears the assignment from the existing appointment, moving it to an 'unassigned' state rather than cancelling it.
Trace
```
13. Owner#0.RemoveStylist
    s=Stylist#0
    expect: Stylist#0 not in db.active_stylists
    expect: db.appointments[appt0].stylist == None
    expect: db.appointments[appt0].slot == None
```
Verifies: HasUnassignedAppointment (exists), implements exp_unassigned_state, implements exp_inactive_stylist
Walkthrough (from Setup B)
1. The owner adds a second stylist (Stylist#1) and they provide availability for slot0.
2. The owner removes Stylist#0, causing the existing appointment to become unassigned.
3. The owner's view updates to show the unassigned appointment and the new stylist's availability.
4. The owner reassigns the unassigned appointment to Stylist#1 at slot0.
Trace
```
13. Owner#0.AddStylist
14. Stylist#1.AddAvailability
    slot=slot0
15. Owner#0.RemoveStylist
    s=Stylist#0
16. Owner#0.Refresh
17. Owner#0.ReassignUnassigned
    appt={id=appt0, customer=Customer#0, stylist=None, slot=None, service=svc0}
    sched={stylist=Stylist#1, slot=slot0}
    expect: db.appointments[appt0].stylist == Stylist#1
    expect: db.appointments[appt0].slot == slot0
```
Verifies: AppointmentInSchedule (always), AppointmentStylistActive (always), implements exp_reassign_strict

Walkthrough (from Setup B)

The owner adds Stylist#1, who adds availability for slot0.
Customer#1 books Stylist#1 for slot0, occupying that slot.
The owner removes Stylist#0, making the original appointment (appt0) unassigned.
The owner's view updates, but when they attempt to reassign the unassigned appt0 to Stylist#1 at slot0, the system blocks it because the slot is already booked.

Trace

13. Owner#0.AddStylist
14. Stylist#1.AddAvailability
    slot=slot0
15. Customer#1.Refresh
16. Customer#1.BookAppointment
    svc=svc0
    sched={stylist=Stylist#1, slot=slot0}
17. Owner#0.RemoveStylist
    s=Stylist#0
18. Owner#0.Refresh
19. Owner#0.ReassignUnassigned
    appt={id=appt0, customer=Customer#0, stylist=None, slot=None, service=svc0}
    sched={stylist=Stylist#1, slot=slot0}
    expect: action disabled by require (len([a for a in self.appointments if a.stylist == new_stylist_id and a.slot == new_slot]) == 0)

Verifies: StylistNoOverlap (always), implements exp_reassign_strict

Approved without comment.

Customer

Stylist

Book Appointment

Manage Availability

Do all stylists offer the same services and prices, or does each stylist have their own list?

Can a stylist handle multiple customers at once (e.g., during a hair color soak), or is it strictly one-at-a-time?

Salon Owner / Admin

Do appointments require manual confirmation from the stylist or salon, or are they instantly confirmed upon booking?

Can customers cancel their own appointments via the app?

Is there a cutoff time before which customers must cancel? (e.g., cannot cancel within 24 hours of the appointment)

Manage Stylist Profiles

Manage Global Service Catalog

View My Appointments

View Schedule

Cancel Appointment

Cancel Customer Appointment

An appointment can only be booked if the stylist has explicit, unbroken availability for the entire duration of the service.

A stylist cannot be booked for multiple appointments whose times overlap.

Appointments cannot be booked or rescheduled for a date and time that has already passed.

When an appointment is cancelled, the associated time slot immediately becomes available for other customers to book.

New appointments cannot be booked with a stylist profile that has been deactivated.

Do services require automatic buffer times (e.g., 10 minutes for cleanup/setup) that block the stylist's schedule but are not part of the customer's appointment time?

Should the system automatically notify stylists and customers when appointments are booked or cancelled?

Requirements gap

If a stylist is removed or deactivated, what should happen to their existing upcoming appointments?

Reassign Appointment

If a service is removed from the global catalog, what happens to existing appointments booked for that service?

Removing a service hides it from new bookings, but existing appointments retain their reference to the original service.

Can a stylist remove an availability time slot if a customer has already booked an appointment during that time?

A stylist cannot remove an availability slot that is currently occupied by an active appointment; the appointment must be cancelled first.

Since appointments are kept when a stylist is deactivated, must the owner reassign them immediately to complete the deactivation, or can appointments remain in an 'unassigned' state to be sorted out later?

An appointment can exist in an active but unassigned state if its assigned stylist is deactivated.

When an admin reassigns an appointment to a different stylist, does the system strictly enforce the new stylist's availability and schedule, or can the admin override overlapping conflicts?

Reassigning an appointment to a new stylist is blocked if the new stylist does not have sufficient availability or has an overlapping appointment.