Select Git revision
Forked from
ab604 / thesis-template
Source project has a limited visibility.
AppointmentMachine.bumx 11.44 KiB
machine AppointmentMachine refines UserMachine
sees AppointmentContext UserContext //this allows the appointment machine to use both contexts
//creating the variables required for the appointment machine
variables
patient //the patient
registered //the status of the appointment: registered
loggedin //whether the use has been logged in or not
dentist
admin
dentist_treatments //list of treatments the dentist can carry out
treatments //all the treatments available
nhs_num //the NHS number for the user
dates //the dates available to book an appointment
appointments //all the appointments booked
current_date
//these are all different statuses of the appointment
status
booked
checked_in
cancelled
missed
completed
invariants
@inv0: treatments ⊆ TREATMENT
@inv1: dates ⊆ ℕ
@inv2: status ⊆ STATUS
@inv3: appointments ⊆ dom(patient) × dom(dentist) × dates × ℙ(TREATMENT) × status
/*
* REQ 8: A dentist has a list of treatments that they are qualified to
perform.
*/
@inv4: dentist_treatments ⊆ dom(dentist) × ℙ(treatments)
@inv5: current_date ∈ ℕ
@inv6: nhs_num ⊆ USER × NHSNUM // each user has an nhs number
@inv7: {booked, checked_in, cancelled, missed, completed} ⊆ STATUS
@inv8: partition(status, {booked}, {checked_in}, {cancelled}, {missed}, {completed})
events
event INITIALISATION extends INITIALISATION
then
@act5: treatments ≔ ∅
@act6: dentist_treatments ≔ ∅
@act7: nhs_num ≔ ∅
@act8: dates ≔ ∅
@act9: appointments ≔ ∅
@act10: current_date ≔ 010124 // setting current date to first of january
@act11: status ≔ ∅
end
/*
* REQ 10: A registered patient must have a unique NHS number
*/
event registerNewPatient extends registerNewPatient
any
patient_nhs_num
where
@grd4: patient_nhs_num ∈ NHSNUM
then
@act3: nhs_num ≔ nhs_num ∪ {new_patient ↦ patient_nhs_num} //adding nhs number of new patient
end
/*
* REQ 12: A logged-in patient can book a new appointment for a
treatment with a registered dentist. *
* REQ 13: The booked dentist must be qualified to perform the
treatment.
*
* REQ 14: An appointment can only be booked for a future date.
*
* REQ 15: A patient cannot have two booked appointments for the
same treatment.
*
* REQ 16: A patient cannot have a booked appointment within 14
days of the patient’s receiving the same treatment.
*/
event BookAppointment
any
pt
chosen_dentist
chosen_date
treatment
where
@grd0: pt ∈ dom(patient)
@grd1: pt ∈ dom(loggedin)
@grd2: chosen_dentist ∈ dom(dentist)
@grd3: chosen_date ∈ dates
@grd4: chosen_date > current_date
@grd5: treatment ∈ dentist_treatments[{chosen_dentist}] // checking treatment is in the chosen dentists list of treatments
@grd6: ∀a,b,c,d,e· (a ↦ b ↦ c ↦ d ↦ e) ∈ appointments ⇒ a ≠ pt ∧ d ≠ treatment // checking patient hasn't already booked an appointment for the same treatment
@grd7: ¬(∃b,c,d,e · (pt ↦ b ↦ c ↦ d ↦ e) ∈ appointments ∧ (chosen_date − c) < 14)//patient cannot book appointment for same treatment within 14 days
then
@act1: appointments ≔ appointments ∪ {pt ↦ chosen_dentist ↦ chosen_date ↦ treatment ↦ booked}
end
event loginUser extends loginUser
end
event logoutUser extends logoutUser
end
event setRootAdmins extends setRootAdmins
end
event changePatientPassword extends changePatientPassword
end
event changeDentistPassword extends changeDentistPassword
end
event changeAdminPassword extends changeAdminPassword
end
event AdminRegisterPatientToDentist extends AdminRegisterPatientToDentist
then
@act3: nhs_num ≔ nhs_num ∖ ({register_user} ◁ nhs_num) // removing patients nhs number
end
event AdminRegisterPatientToAdministrator extends AdminRegisterPatientToAdministrator
then
@act3: nhs_num ≔ nhs_num ∖ ({register_user} ◁ nhs_num)// removing patients nhs number
end
event AdminRegisterDentistToAdministrator extends AdminRegisterDentistToAdministrator
end
/*
* REQ 17 - A logged-in patient can cancel their booked appointment up to 2 days before the appointment date
* and the appointment status changes to “cancelled”
*/
event CancelAppointment
any
pt
dent dat
treat
stat
where
// specifying types:
@grd0: pt ∈ dom(patient)
@grd1: dent ∈ dom(dentist)
@grd2: dat ∈ dates
@grd3: treat ∈ ℙ(TREATMENT)
@grd4: stat ∈ status
@grd5: pt ∈ dom(loggedin) // Patient must be logged in
@grd6: (pt ↦ dent ↦ dat ↦ treat ↦ stat) ∈ appointments ⇒ stat = booked // status must be "booked"
then
@act0: appointments ≔ appointments { pt ↦ dent ↦ dat ↦ treat ↦ cancelled} // change status to "cancelled"
end
/*
* REQ 18 - A logged-in patient can re-book their booked appointment up to 2 days before the appointment date
*/
event RebookAppointment
any
pt
dent
dat
treatment
newDat
stat
where
// specifying types:
@grd0: pt ∈ dom(patient)
@grd1: dent ∈ dom(dentist)
@grd2: dat ∈ dates
@grd3: stat ∈ status
@grd4: newDat ∈ dates
@grd5: newDat > current_date
@grd6: treatment ∈ dentist_treatments[{dent}]
@grd7: pt ∈ dom(loggedin) // Patient must be logged in
// checks if current date is over 2 days before the appointment date and if the status of appointment is booked:
@grd8: (pt ↦ dent ↦ dat ↦ treatment ↦ stat) ∈ appointments ⇒ ((current_date − dat) > 2 ∧ stat = booked)
then
@act0: appointments ≔ appointments { pt ↦ dent ↦ newDat ↦ treatment ↦ booked} // change the date of the appointment
end
/*
* REQ 19 - A patient can check in on the appointment date
* and the appointment status changes to “checked-in”
*/
event CheckInAppointment
any
pt
dent
dat
treat
stat
where
// specifying types:
@grd0: pt ∈ dom(patient)
@grd1: dent ∈ dom(dentist)
@grd2: dat ∈ dates
@grd3: treat ∈ ℙ(TREATMENT)
@grd4: stat ∈ status
@grd5: pt ∈ dom(loggedin) // Patient must be logged in
@grd6: (pt ↦ dent ↦ dat ↦ treat ↦ stat) ∈ appointments ⇒ current_date = dat // checks if current date is the appointment date
then
@act0: appointments ≔ appointments { pt ↦ dent ↦ dat ↦ treat ↦ checked_in} // change status to "checked in"
end
/*
* REQ 20 - After a checked-in patient receives the required treatment
* a logged-in dentist updates the appointment to “completed”
*/
event CompletedAppointment
any
pt
dent
dat
treat
stat
where
// specifying types:
@grd0: dent ∈ dom(dentist)
@grd1: pt ∈ dom(patient)
@grd2: dat ∈ dates
@grd3: treat ∈ ℙ(TREATMENT)
@grd4: stat ∈ status
@grd5: dent ∈ dom(loggedin) // Dentist must be logged in
// checks if the current date is the appointment date and if the patient has checked in:
@grd6: (pt ↦ dent ↦ dat ↦ treat ↦ stat) ∈ appointments ⇒ current_date = dat ∧ stat = checked_in
then
@act0: appointments ≔ appointments { pt ↦ dent ↦ dat ↦ treat ↦ completed} // changes status to "completed"
end
/*
* REQ 21 - When the patients do not turn up to their appointment
* an administrator sets the appointment status to “missed”
*/
event MissedAppointment
any
ad
pt
dent
dat
treat
stat
where
// specifying types:
@grd0: ad ∈ dom(admin)
@grd1: pt ∈ dom(patient)
@grd2: dent ∈ dom(dentist)
@grd3: dat ∈ dates
@grd4: stat ∈ status
@grd5: treat ∈ ℙ(TREATMENT)
@grd6: ad ∈ dom(loggedin) // admin must be logged in
// checks if current date is greater than the appointment date and if the status is still "booked"
@grd7: (pt ↦ dent ↦ dat ↦ treat ↦ stat) ∈ appointments ⇒ current_date > dat ∧ stat = booked
then
@act0: appointments ≔ appointments { pt ↦ dent ↦ dat ↦ treat ↦ missed} // change status to missed
end
/*
* REQ 22 - The system should ensure that there are no overdue appointments
* (i.e., “booked” appointments with a past appointment date)
*/
event CheckOverdueAppointments
any
pt
dent
dat
treat
stat
where
// specifying types:
@grd0: pt ∈ dom(patient)
@grd1: dent ∈ dom(dentist) @grd2: dat ∈ dates
@grd3: treat ∈ ℙ(TREATMENT)
@grd4: stat ∈ status
// checks whether appointment date has passed and if the status of the appointment is still booked
@grd5: (pt ↦ dent ↦ dat ↦ treat ↦ stat) ∈ appointments ⇒ current_date > dat ∧ stat = booked
then
@act0: appointments ≔ appointments {pt ↦ dent ↦ dat ↦ treat ↦ missed} // changes status of appointment to missed
end
/*
* REQ 23
* A logged-in administrator or dentist to view a patient
* appointment record with their NHS number
* @param patient_nhs_number is the patient's nhs number to be looked up
*/
event GetsPatientAppointmentRecord
any
patient_nhs_number
appointment_records_result
user
pt
where
//declaring types
@grd0: patient_nhs_number ∈ nhs_num
@grd1: appointment_records_result ⊆ appointments
@grd2 user ∈ USER
@grd3: pt ∈ patient
@grd4 pt ≔ dom(nhs_num)
@grd5: user ∈ dom(admin) ∪ (dom(dentist)) //checks that user is a admin or dentist
@grd6: user ∈ dom(loggedin) // Admin must be logged in
// @grd7: appointment_records_result = a ∣ a ∈ appointments ∧ (dom({appointments}) = dom(nhs_num)}
end
/*
* REQ 24
* A logged-in patient can check their booked
* appointments on a specific day.
*/
event GetsBookedAppointmentonASpecificDay
any
patient_nhs_number
appointment_records_result //the result returned
user
pt
date_specified //date to view the appointment
where
//declaring types
@grd0: patient_nhs_number ∈ nhs_num
@grd1: appointment_records_result ⊆ appointments
@grd2 user ∈ USER
@grd3: pt ∈ patient
@grd4: date_specified ∈ dates
@grd5: user ∈ dom(patient) //checks that user is a patient
// @grd6: appointment_records_result = a ∣ a ∈ appointments(date_specified)}
end
/*
* REQ 25
* A logged-in patient can view their treatment record.
*/
event GetsPatientsTreatmentRecord
any
pt //the logged in patient
treatment_record //the patient's treatment record (output/result)
user
password
where
@grd0: password = loggedin(pt) // Patient must be logged in
@grd1: user ∈ dom(loggedin) // Patient must be logged in
@grd2: treatment_record ∈ treatments
@grd3: user ∈ dom(patient) //checks that user is a patient
// @grd4: treatment_record = treatments ∣ treatments(patient) == pt
end
end