Skip to content
Snippets Groups Projects
Select Git revision
  • e74fe8cfa9ab22520aee469a30e5ea67ec6ed075
  • master default protected
2 results

august.bib

Blame
  • 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