Added Kirsty's comments

UserManagement/AppointmentContext.bcc

 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <org.eventb.core.scContextFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd;ac.soton.xeventb.xcontext.base">
-    <org.eventb.core.scCarrierSet name="STATUS" org.eventb.core.source="/UserManagement/AppointmentContext.buc|org.eventb.core.contextFile#AppointmentContext|org.eventb.core.carrierSet#_w8ygQA35Ee-bMZTDvaEJhw" org.eventb.core.type="ℙ(STATUS)"/>
-    <org.eventb.core.scCarrierSet name="TREATMENT" org.eventb.core.source="/UserManagement/AppointmentContext.buc|org.eventb.core.contextFile#AppointmentContext|org.eventb.core.carrierSet#_w8wEAA35Ee-bMZTDvaEJhw" org.eventb.core.type="ℙ(TREATMENT)"/>
-    <org.eventb.core.scCarrierSet name="DATE" org.eventb.core.source="/UserManagement/AppointmentContext.buc|org.eventb.core.contextFile#AppointmentContext|org.eventb.core.carrierSet#_w8x5MA35Ee-bMZTDvaEJhw" org.eventb.core.type="ℙ(DATE)"/>
-    <org.eventb.core.scCarrierSet name="NHSNUM" org.eventb.core.source="/UserManagement/AppointmentContext.buc|org.eventb.core.contextFile#AppointmentContext|org.eventb.core.carrierSet#_w8xSIA35Ee-bMZTDvaEJhw" org.eventb.core.type="ℙ(NHSNUM)"/>
+    <org.eventb.core.scCarrierSet name="STATUS" org.eventb.core.source="/UserManagement/AppointmentContext.buc|org.eventb.core.contextFile#AppointmentContext|org.eventb.core.carrierSet#_OeNksg4kEe-1OOl4iWIhfA" org.eventb.core.type="ℙ(STATUS)"/>
+    <org.eventb.core.scCarrierSet name="TREATMENT" org.eventb.core.source="/UserManagement/AppointmentContext.buc|org.eventb.core.contextFile#AppointmentContext|org.eventb.core.carrierSet#_OeM9oA4kEe-1OOl4iWIhfA" org.eventb.core.type="ℙ(TREATMENT)"/>
+    <org.eventb.core.scCarrierSet name="DATE" org.eventb.core.source="/UserManagement/AppointmentContext.buc|org.eventb.core.contextFile#AppointmentContext|org.eventb.core.carrierSet#_OeNksQ4kEe-1OOl4iWIhfA" org.eventb.core.type="ℙ(DATE)"/>
+    <org.eventb.core.scCarrierSet name="NHSNUM" org.eventb.core.source="/UserManagement/AppointmentContext.buc|org.eventb.core.contextFile#AppointmentContext|org.eventb.core.carrierSet#_OeNksA4kEe-1OOl4iWIhfA" org.eventb.core.type="ℙ(NHSNUM)"/>
 </org.eventb.core.scContextFile>

UserManagement/AppointmentContext.bpo

-<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.poFile org.eventb.core.poStamp="1">
-    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="1">
-        <org.eventb.core.poIdentifier name="STATUS" org.eventb.core.type="ℙ(STATUS)"/>
-        <org.eventb.core.poIdentifier name="TREATMENT" org.eventb.core.type="ℙ(TREATMENT)"/>
-        <org.eventb.core.poIdentifier name="DATE" org.eventb.core.type="ℙ(DATE)"/>
-        <org.eventb.core.poIdentifier name="NHSNUM" org.eventb.core.type="ℙ(NHSNUM)"/>
-    </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/UserManagement/AppointmentContext.bpo|org.eventb.core.poFile#AppointmentContext|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="1"/>
-</org.eventb.core.poFile>

UserManagement/AppointmentContext.bps

-<?xml version="1.0" encoding="UTF-8"?>
-<org.eventb.core.psFile/>
\ No newline at end of file

UserManagement/AppointmentContext.buc

 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <org.eventb.core.contextFile org.eventb.core.configuration="org.eventb.core.fwd;ac.soton.xeventb.xcontext.base" org.eventb.core.generated="false" version="3">
-    <org.eventb.core.carrierSet name="_w8wEAA35Ee-bMZTDvaEJhw" org.eventb.core.generated="false" org.eventb.core.identifier="TREATMENT"/>
-    <org.eventb.core.carrierSet name="_w8xSIA35Ee-bMZTDvaEJhw" org.eventb.core.generated="false" org.eventb.core.identifier="NHSNUM"/>
-    <org.eventb.core.carrierSet name="_w8x5MA35Ee-bMZTDvaEJhw" org.eventb.core.generated="false" org.eventb.core.identifier="DATE"/>
-    <org.eventb.core.carrierSet name="_w8ygQA35Ee-bMZTDvaEJhw" org.eventb.core.generated="false" org.eventb.core.identifier="STATUS"/>
+    <org.eventb.core.carrierSet name="_OeM9oA4kEe-1OOl4iWIhfA" org.eventb.core.generated="false" org.eventb.core.identifier="TREATMENT"/>
+    <org.eventb.core.carrierSet name="_OeNksA4kEe-1OOl4iWIhfA" org.eventb.core.generated="false" org.eventb.core.identifier="NHSNUM"/>
+    <org.eventb.core.carrierSet name="_OeNksQ4kEe-1OOl4iWIhfA" org.eventb.core.generated="false" org.eventb.core.identifier="DATE"/>
+    <org.eventb.core.carrierSet name="_OeNksg4kEe-1OOl4iWIhfA" org.eventb.core.generated="false" org.eventb.core.identifier="STATUS"/>
 </org.eventb.core.contextFile>

UserManagement/AppointmentMachine.bps

-<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.psFile>
-    <org.eventb.core.psStatus name="INITIALISATION/inv1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv4/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv5/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv8/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="registerNewPatient/inv3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="BookAppointment/inv3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="changePatientPassword/inv3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="changeDentistPassword/inv3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="changeDentistPassword/inv4/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterPatientToDentist/inv3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="154" org.eventb.core.psBroken="true" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterPatientToDentist/inv4/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterPatientToAdministrator/inv3/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterDentistToAdministrator/inv3/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterDentistToAdministrator/inv4/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="CancelAppointment/inv3/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="RebookAppointment/inv3/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="CheckInAppointment/inv3/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="CompletedAppointment/inv3/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="MissedAppointment/inv3/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="CheckOverdueAppointments/inv3/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="GetsPatientsTreatmentRecord/grd0/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="154" org.eventb.core.psManual="false"/>
-</org.eventb.core.psFile>

UserManagement/AppointmentMachine.bumx

@@ -62,9 +62,24 @@ events
     where
         @grd4: patient_nhs_num ∈ NHSNUM
     then
-        @act3: nhs_num ≔ nhs_num ∪ {new_patient ↦ patient_nhs_num}
+        @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
@@ -77,8 +92,8 @@ events
         @grd2: chosen_dentist ∈ dom(dentist)
         @grd3: chosen_date ∈ dates
         @grd4: chosen_date > current_date
-        @grd5: treatment ∈ dentist_treatments[{chosen_dentist}]
-        @grd6: ∀a,b,c,d,e· (a ↦ b ↦ c ↦ d ↦ e) ∈ appointments ⇒ a ≠ pt ∧ d ≠ treatment 
+        @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}
@@ -104,12 +119,12 @@ events
 
     event AdminRegisterPatientToDentist extends AdminRegisterPatientToDentist
     then
-        @act3: nhs_num ≔ nhs_num ∖ ({register_user} ◁ nhs_num)
+        @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)
+        @act3: nhs_num ≔ nhs_num ∖ ({register_user} ◁ nhs_num)// removing patients nhs number
     end
 
     event AdminRegisterDentistToAdministrator extends AdminRegisterDentistToAdministrator

UserManagement/UserContext.bcc

-<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.scContextFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd;ac.soton.xeventb.xcontext.base">
-    <org.eventb.core.scCarrierSet name="USER" org.eventb.core.source="/UserManagement/UserContext.buc|org.eventb.core.contextFile#UserContext|org.eventb.core.carrierSet#_w8gzcA35Ee-bMZTDvaEJhw" org.eventb.core.type="ℙ(USER)"/>
-    <org.eventb.core.scCarrierSet name="PASSWORD" org.eventb.core.source="/UserManagement/UserContext.buc|org.eventb.core.contextFile#UserContext|org.eventb.core.carrierSet#_w8iooA35Ee-bMZTDvaEJhw" org.eventb.core.type="ℙ(PASSWORD)"/>
-</org.eventb.core.scContextFile>

UserManagement/UserContext.bpo

-<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.poFile org.eventb.core.poStamp="0">
-    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="0">
-        <org.eventb.core.poIdentifier name="USER" org.eventb.core.type="ℙ(USER)"/>
-        <org.eventb.core.poIdentifier name="PASSWORD" org.eventb.core.type="ℙ(PASSWORD)"/>
-    </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/UserManagement/UserContext.bpo|org.eventb.core.poFile#UserContext|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="0"/>
-</org.eventb.core.poFile>

UserManagement/UserContext.bps

-<?xml version="1.0" encoding="UTF-8"?>
-<org.eventb.core.psFile/>
\ No newline at end of file

UserManagement/UserContext.buc

 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <org.eventb.core.contextFile org.eventb.core.configuration="org.eventb.core.fwd;ac.soton.xeventb.xcontext.base" org.eventb.core.generated="false" version="3">
-    <org.eventb.core.carrierSet name="_w8gzcA35Ee-bMZTDvaEJhw" org.eventb.core.generated="false" org.eventb.core.identifier="USER"/>
-    <org.eventb.core.carrierSet name="_w8iooA35Ee-bMZTDvaEJhw" org.eventb.core.generated="false" org.eventb.core.identifier="PASSWORD"/>
+    <org.eventb.core.carrierSet name="_OeQA8A4kEe-1OOl4iWIhfA" org.eventb.core.generated="false" org.eventb.core.identifier="USER"/>
+    <org.eventb.core.carrierSet name="_OeQA8Q4kEe-1OOl4iWIhfA" org.eventb.core.generated="false" org.eventb.core.identifier="PASSWORD"/>
 </org.eventb.core.contextFile>

UserManagement/UserMachine.bps

-<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.psFile>
-    <org.eventb.core.psStatus name="INITIALISATION/inv0/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv6/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv7/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="setRootAdmins/inv0/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="setRootAdmins/inv6/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="setRootAdmins/inv7/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="setRootAdmins/inv8/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="registerNewPatient/grd3/WD" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psBroken="true" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="registerNewPatient/inv2/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="registerNewPatient/inv6/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psBroken="true" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="registerNewPatient/inv7/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="registerNewPatient/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="loginUser/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="loginUser/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="logoutUser/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="logoutUser/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="changePatientPassword/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="changePatientPassword/inv2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="changePatientPassword/inv6/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="changePatientPassword/inv7/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="changePatientPassword/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="changeDentistPassword/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="changeDentistPassword/inv1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="changeDentistPassword/inv6/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="changeDentistPassword/inv7/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="changeDentistPassword/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="changeAdminPassword/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="changeAdminPassword/inv0/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="changeAdminPassword/inv6/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="changeAdminPassword/inv7/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="changeAdminPassword/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterPatientToDentist/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterPatientToDentist/inv1/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterPatientToDentist/inv2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterPatientToDentist/inv6/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterPatientToDentist/inv7/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterPatientToAdministrator/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterPatientToAdministrator/inv0/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterPatientToAdministrator/inv2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterPatientToAdministrator/inv6/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterPatientToAdministrator/inv7/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterDentistToAdministrator/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterDentistToAdministrator/inv0/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterDentistToAdministrator/inv1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterDentistToAdministrator/inv6/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="AdminRegisterDentistToAdministrator/inv7/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-</org.eventb.core.psFile>