Skip to content
Snippets Groups Projects
Commit da2402c1 authored by Vishnu Priya's avatar Vishnu Priya
Browse files

REQ11

parent 0818d1fa
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
UserManagement/UserMachine.bcm
+ 91
− 55
View file @ da2402c1
<?xml version="1.0" encoding="UTF-8" standalone="no"?> <?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scMachineFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd;ac.soton.xeventb.xmachine.base"> <org.eventb.core.scMachineFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd;ac.soton.xeventb.xmachine.base">
<org.eventb.core.scSeesContext name="'" org.eventb.core.scTarget="/UserManagement/UserContext.bcc" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.seesContext#_8y5v0AldEe-O984l8O-k1g"/> <org.eventb.core.scSeesContext name="'" org.eventb.core.scTarget="/UserManagement/UserContext.bcc" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.seesContext#_Qg7ZUArBEe-O984l8O-k1g"/>
<org.eventb.core.scInternalContext name="UserContext"> <org.eventb.core.scInternalContext name="UserContext">
<org.eventb.core.scCarrierSet name="USER" org.eventb.core.source="/UserManagement/UserContext.buc|org.eventb.core.contextFile#UserContext|org.eventb.core.carrierSet#_5NRswAk4Ee-O984l8O-k1g" org.eventb.core.type="ℙ(USER)"/> <org.eventb.core.scCarrierSet name="USER" org.eventb.core.source="/UserManagement/UserContext.buc|org.eventb.core.contextFile#UserContext|org.eventb.core.carrierSet#_5NRswAk4Ee-O984l8O-k1g" 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#_5NRswQk4Ee-O984l8O-k1g" org.eventb.core.type="ℙ(PASSWORD)"/> <org.eventb.core.scCarrierSet name="PASSWORD" org.eventb.core.source="/UserManagement/UserContext.buc|org.eventb.core.contextFile#UserContext|org.eventb.core.carrierSet#_5NRswQk4Ee-O984l8O-k1g" org.eventb.core.type="ℙ(PASSWORD)"/>
</org.eventb.core.scInternalContext> </org.eventb.core.scInternalContext>
<org.eventb.core.scInvariant name="UserContexu" org.eventb.core.label="inv0" org.eventb.core.predicate="admin∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W4QldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scInvariant name="UserContexu" org.eventb.core.label="inv0" org.eventb.core.predicate="admin∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZQrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="UserContexv" org.eventb.core.label="inv1" org.eventb.core.predicate="dentist∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W4gldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scInvariant name="UserContexv" org.eventb.core.label="inv1" org.eventb.core.predicate="dentist∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZgrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="UserContexw" org.eventb.core.label="inv2" org.eventb.core.predicate="patient∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W4wldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scInvariant name="UserContexw" org.eventb.core.label="inv2" org.eventb.core.predicate="patient∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZwrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="UserContexx" org.eventb.core.label="inv3" org.eventb.core.predicate="dom(admin)⊆USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W5AldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scInvariant name="UserContexx" org.eventb.core.label="inv3" org.eventb.core.predicate="dom(admin)⊆USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AaArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="UserContexy" org.eventb.core.label="inv4" org.eventb.core.predicate="dom(dentist)⊆USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W5QldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scInvariant name="UserContexy" org.eventb.core.label="inv4" org.eventb.core.predicate="dom(dentist)⊆USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AaQrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="UserContexz" org.eventb.core.label="inv5" org.eventb.core.predicate="dom(patient)⊆USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W5gldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scInvariant name="UserContexz" org.eventb.core.label="inv5" org.eventb.core.predicate="dom(patient)⊆USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AagrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="UserContex{" org.eventb.core.label="inv6" org.eventb.core.predicate="admin∩dentist∩patient=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W5wldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scInvariant name="UserContex{" org.eventb.core.label="inv6" org.eventb.core.predicate="admin∩dentist∩patient=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AawrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="UserContex|" org.eventb.core.label="inv7" org.eventb.core.predicate="registered=admin∪dentist∪patient" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W6AldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scInvariant name="UserContex|" org.eventb.core.label="inv7" org.eventb.core.predicate="registered=admin∪dentist∪patient" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="UserContex}" org.eventb.core.label="inv8" org.eventb.core.predicate="loggedin⊆registered" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y698AldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scInvariant name="UserContex}" org.eventb.core.label="inv8" org.eventb.core.predicate="loggedin⊆registered" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncQrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scVariable name="loggedin" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_8y5v1AldEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/> <org.eventb.core.scVariable name="loggedin" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_Qg8AYwrBEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
<org.eventb.core.scVariable name="patient" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_8y5v0wldEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/> <org.eventb.core.scVariable name="patient" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_Qg8AYgrBEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
<org.eventb.core.scVariable name="dentist" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_8y5v0gldEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/> <org.eventb.core.scVariable name="dentist" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_Qg8AYQrBEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
<org.eventb.core.scVariable name="registered" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_8y6W4AldEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/> <org.eventb.core.scVariable name="registered" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_Qg8AZArBEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
<org.eventb.core.scVariable name="admin" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_8y5v0QldEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/> <org.eventb.core.scVariable name="admin" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_Qg8AYArBEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
<org.eventb.core.scEvent name="UserContex~" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y698QldEe-O984l8O-k1g"> <org.eventb.core.scEvent name="UserContex~" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8ncgrBEe-O984l8O-k1g">
<org.eventb.core.scAction name="'" org.eventb.core.assignment="admin ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y698QldEe-O984l8O-k1g|org.eventb.core.action#_8y698gldEe-O984l8O-k1g"/> <org.eventb.core.scAction name="'" org.eventb.core.assignment="admin ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8ncgrBEe-O984l8O-k1g|org.eventb.core.action#_Qg8ncwrBEe-O984l8O-k1g"/>
<org.eventb.core.scAction name="(" org.eventb.core.assignment="dentist ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act1" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y698QldEe-O984l8O-k1g|org.eventb.core.action#_8y698wldEe-O984l8O-k1g"/> <org.eventb.core.scAction name="(" org.eventb.core.assignment="dentist ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act1" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8ncgrBEe-O984l8O-k1g|org.eventb.core.action#_Qg8ndArBEe-O984l8O-k1g"/>
<org.eventb.core.scAction name=")" org.eventb.core.assignment="patient ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act2" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y698QldEe-O984l8O-k1g|org.eventb.core.action#_8y699AldEe-O984l8O-k1g"/> <org.eventb.core.scAction name=")" org.eventb.core.assignment="patient ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act2" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8ncgrBEe-O984l8O-k1g|org.eventb.core.action#_Qg8ndQrBEe-O984l8O-k1g"/>
<org.eventb.core.scAction name="*" org.eventb.core.assignment="loggedin ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act3" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y698QldEe-O984l8O-k1g|org.eventb.core.action#_8y699QldEe-O984l8O-k1g"/> <org.eventb.core.scAction name="*" org.eventb.core.assignment="loggedin ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act3" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8ncgrBEe-O984l8O-k1g|org.eventb.core.action#_Qg8ndgrBEe-O984l8O-k1g"/>
<org.eventb.core.scAction name="+" org.eventb.core.assignment="registered ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act4" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y698QldEe-O984l8O-k1g|org.eventb.core.action#_8y699gldEe-O984l8O-k1g"/> <org.eventb.core.scAction name="+" org.eventb.core.assignment="registered ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act4" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8ncgrBEe-O984l8O-k1g|org.eventb.core.action#_Qg8ndwrBEe-O984l8O-k1g"/>
</org.eventb.core.scEvent> </org.eventb.core.scEvent>
<org.eventb.core.scEvent name="UserContey'" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="setRootAdmins" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g"> <org.eventb.core.scEvent name="UserContey'" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="setRootAdmins" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="root∈USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g|org.eventb.core.guard#_8y69-gldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="root∈USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg8newrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="root_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lAAldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="root_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg8nfArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="admin=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lAQldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="admin=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg9OgArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="root_password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g|org.eventb.core.parameter#_8y69-QldEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/> <org.eventb.core.scParameter name="root_password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg8negrBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
<org.eventb.core.scParameter name="root" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g|org.eventb.core.parameter#_8y69-AldEe-O984l8O-k1g" org.eventb.core.type="USER"/> <org.eventb.core.scParameter name="root" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg8neQrBEe-O984l8O-k1g" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="root_passwore" org.eventb.core.assignment="admin ≔ {root ↦ root_password}" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g|org.eventb.core.action#_8y7lAgldEe-O984l8O-k1g"/> <org.eventb.core.scAction name="root_passwore" org.eventb.core.assignment="admin ≔ {root ↦ root_password}" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g|org.eventb.core.action#_Qg9OgQrBEe-O984l8O-k1g"/>
<org.eventb.core.scAction name="root_passworf" org.eventb.core.assignment="registered ≔ {root ↦ root_password}" org.eventb.core.label="act1" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g|org.eventb.core.action#_8y7lAwldEe-O984l8O-k1g"/> <org.eventb.core.scAction name="root_passworf" org.eventb.core.assignment="registered ≔ {root ↦ root_password}" org.eventb.core.label="act1" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g|org.eventb.core.action#_Qg9OggrBEe-O984l8O-k1g"/>
</org.eventb.core.scEvent> </org.eventb.core.scEvent>
<org.eventb.core.scEvent name="UserContey(" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="registerNewPatient" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g"> <org.eventb.core.scEvent name="UserContey(" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="registerNewPatient" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="new_patient∈USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lBwldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="new_patient∈USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg9OhgrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="new_patient_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lCAldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="new_patient_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg9OhwrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="new_patient∉dom(registered)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lCQldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="new_patient∉dom(registered)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg9OiArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd3" org.eventb.core.predicate="card(admin)&gt;0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lCgldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scGuard name="*" org.eventb.core.label="grd3" org.eventb.core.predicate="card(admin)&gt;0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg9OiQrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="new_patient_password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.parameter#_8y7lBgldEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/> <org.eventb.core.scParameter name="new_patient_password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg9OhQrBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
<org.eventb.core.scParameter name="new_patient" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.parameter#_8y7lBQldEe-O984l8O-k1g" org.eventb.core.type="USER"/> <org.eventb.core.scParameter name="new_patient" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg9OhArBEe-O984l8O-k1g" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="new_patient_passwore" org.eventb.core.assignment="patient ≔ patient∪{new_patient ↦ new_patient_password}" org.eventb.core.label="act1" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.action#_8y7lCwldEe-O984l8O-k1g"/> <org.eventb.core.scAction name="new_patient_passwore" org.eventb.core.assignment="patient ≔ patient∪{new_patient ↦ new_patient_password}" org.eventb.core.label="act1" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.action#_Qg9OigrBEe-O984l8O-k1g"/>
<org.eventb.core.scAction name="new_patient_passworf" org.eventb.core.assignment="registered ≔ registered∪{new_patient ↦ new_patient_password}" org.eventb.core.label="act2" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.action#_8y7lDAldEe-O984l8O-k1g"/> <org.eventb.core.scAction name="new_patient_passworf" org.eventb.core.assignment="registered ≔ registered∪{new_patient ↦ new_patient_password}" org.eventb.core.label="act2" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.action#_Qg9OiwrBEe-O984l8O-k1g"/>
</org.eventb.core.scEvent> </org.eventb.core.scEvent>
<org.eventb.core.scEvent name="UserContey)" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="loginUser" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g"> <org.eventb.core.scEvent name="UserContey)" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="loginUser" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="user∈dom(registered)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g|org.eventb.core.guard#_8y8MEgldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="user∈dom(registered)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg91kgrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="user_password=registered(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g|org.eventb.core.guard#_8y8MEwldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="user_password=registered(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg91kwrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="user∉dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g|org.eventb.core.guard#_8y8MFAldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="user∉dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg91lArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="user_password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g|org.eventb.core.parameter#_8y8MEQldEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/> <org.eventb.core.scParameter name="user_password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg91kQrBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
<org.eventb.core.scParameter name="user" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g|org.eventb.core.parameter#_8y8MEAldEe-O984l8O-k1g" org.eventb.core.type="USER"/> <org.eventb.core.scParameter name="user" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg91kArBEe-O984l8O-k1g" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="user_passwore" org.eventb.core.assignment="loggedin ≔ loggedin∪{user ↦ user_password}" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g|org.eventb.core.action#_8y8MFQldEe-O984l8O-k1g"/> <org.eventb.core.scAction name="user_passwore" org.eventb.core.assignment="loggedin ≔ loggedin∪{user ↦ user_password}" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g|org.eventb.core.action#_Qg91lQrBEe-O984l8O-k1g"/>
</org.eventb.core.scEvent> </org.eventb.core.scEvent>
<org.eventb.core.scEvent name="UserContey*" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="logoutUser" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y8MFgldEe-O984l8O-k1g"> <org.eventb.core.scEvent name="UserContey*" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="logoutUser" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91lgrBEe-O984l8O-k1g">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="user∈dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y8MFgldEe-O984l8O-k1g|org.eventb.core.guard#_8y8MGQldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="user∈dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91lgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg91mQrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="password=loggedin(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y8MFgldEe-O984l8O-k1g|org.eventb.core.guard#_8y8MGgldEe-O984l8O-k1g" org.eventb.core.theorem="false"/> <org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="password=loggedin(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91lgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg91mgrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y8MFgldEe-O984l8O-k1g|org.eventb.core.parameter#_8y8MGAldEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/> <org.eventb.core.scParameter name="password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91lgrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg91mArBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
<org.eventb.core.scParameter name="user" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y8MFgldEe-O984l8O-k1g|org.eventb.core.parameter#_8y8MFwldEe-O984l8O-k1g" org.eventb.core.type="USER"/> <org.eventb.core.scParameter name="user" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91lgrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg91lwrBEe-O984l8O-k1g" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="passwore" org.eventb.core.assignment="loggedin ≔ loggedin ∖ {user ↦ password}" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y8MFgldEe-O984l8O-k1g|org.eventb.core.action#_8y8MGwldEe-O984l8O-k1g"/> <org.eventb.core.scAction name="passwore" org.eventb.core.assignment="loggedin ≔ loggedin ∖ {user ↦ password}" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91lgrBEe-O984l8O-k1g|org.eventb.core.action#_Qg91mwrBEe-O984l8O-k1g"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="UserContey+" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="changePatientPassword" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="user∈dom(patient)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg-cowrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="password=loggedin(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg-cpArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="new_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg-cpQrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd3" org.eventb.core.predicate="user∈dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg-cpgrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg-coQrBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
<org.eventb.core.scParameter name="new_password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg-cogrBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
<org.eventb.core.scParameter name="user" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg-coArBEe-O984l8O-k1g" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="new_passwore" org.eventb.core.assignment="loggedin ≔ loggedin{user ↦ new_password}" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.action#_Qg-cpwrBEe-O984l8O-k1g"/>
<org.eventb.core.scAction name="new_passworf" org.eventb.core.assignment="registered ≔ registered{user ↦ new_password}" org.eventb.core.label="act1" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.action#_Qg-cqArBEe-O984l8O-k1g"/>
<org.eventb.core.scAction name="new_passworg" org.eventb.core.assignment="patient ≔ patient{user ↦ new_password}" org.eventb.core.label="act2" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.action#_Qg-cqQrBEe-O984l8O-k1g"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="UserContey," org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="changeDentistPassword" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="user∈dom(dentist)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DsArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="password=loggedin(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DsQrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="new_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DsgrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd3" org.eventb.core.predicate="user∈dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DswrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg-crArBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
<org.eventb.core.scParameter name="new_password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg-crQrBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
<org.eventb.core.scParameter name="user" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg-cqwrBEe-O984l8O-k1g" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="new_passwore" org.eventb.core.assignment="loggedin ≔ loggedin{user ↦ new_password}" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.action#_Qg_DtArBEe-O984l8O-k1g"/>
<org.eventb.core.scAction name="new_passworf" org.eventb.core.assignment="registered ≔ registered{user ↦ new_password}" org.eventb.core.label="act1" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.action#_Qg_DtQrBEe-O984l8O-k1g"/>
<org.eventb.core.scAction name="new_passworg" org.eventb.core.assignment="dentist ≔ dentist{user ↦ new_password}" org.eventb.core.label="act2" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.action#_Qg_DtgrBEe-O984l8O-k1g"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="UserContey-" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="changeAdminPassword" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="user∈dom(admin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DuwrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="password=loggedin(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DvArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="new_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_qwArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd3" org.eventb.core.predicate="user∈dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_qwQrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg_DuQrBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
<org.eventb.core.scParameter name="new_password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg_DugrBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
<org.eventb.core.scParameter name="user" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg_DuArBEe-O984l8O-k1g" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="new_passwore" org.eventb.core.assignment="loggedin ≔ loggedin{user ↦ new_password}" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.action#_Qg_qwgrBEe-O984l8O-k1g"/>
<org.eventb.core.scAction name="new_passworf" org.eventb.core.assignment="registered ≔ registered{user ↦ new_password}" org.eventb.core.label="act1" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.action#_Qg_qwwrBEe-O984l8O-k1g"/>
<org.eventb.core.scAction name="new_passworg" org.eventb.core.assignment="admin ≔ admin{user ↦ new_password}" org.eventb.core.label="act2" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.action#_Qg_qxArBEe-O984l8O-k1g"/>
</org.eventb.core.scEvent> </org.eventb.core.scEvent>
</org.eventb.core.scMachineFile> </org.eventb.core.scMachineFile>
UserManagement/UserMachine.bpo
+ 271
− 109
View file @ da2402c1
This diff is collapsed.
UserManagement/UserMachine.bpr
+ 492
− 0
View file @ da2402c1
This diff is collapsed.
UserManagement/UserMachine.bps
+ 34
− 19
View file @ da2402c1
<?xml version="1.0" encoding="UTF-8" standalone="no"?> <?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.psFile> <org.eventb.core.psFile>
<org.eventb.core.psStatus name="INITIALISATION/inv0/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="INITIALISATION/inv0/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIALISATION/inv1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="INITIALISATION/inv1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIALISATION/inv2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="INITIALISATION/inv2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIALISATION/inv6/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="INITIALISATION/inv6/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIALISATION/inv7/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="INITIALISATION/inv7/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIALISATION/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="INITIALISATION/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="setRootAdmins/inv0/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="setRootAdmins/inv0/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="setRootAdmins/inv6/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="setRootAdmins/inv6/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="setRootAdmins/inv7/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="setRootAdmins/inv7/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="setRootAdmins/inv8/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="setRootAdmins/inv8/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="registerNewPatient/grd3/WD" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psBroken="true" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="registerNewPatient/grd3/WD" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" 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="49" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="registerNewPatient/inv2/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="registerNewPatient/inv6/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psBroken="true" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="registerNewPatient/inv6/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" 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="49" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="registerNewPatient/inv7/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="registerNewPatient/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="registerNewPatient/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="loginUser/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="loginUser/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="loginUser/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="loginUser/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="logoutUser/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="logoutUser/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="logoutUser/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="logoutUser/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="changePatientPassword/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="changePatientPassword/inv2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="changePatientPassword/inv6/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="changePatientPassword/inv7/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="changePatientPassword/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="changeDentistPassword/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="changeDentistPassword/inv1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="changeDentistPassword/inv6/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="changeDentistPassword/inv7/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="changeDentistPassword/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="changeAdminPassword/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="changeAdminPassword/inv0/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="changeAdminPassword/inv6/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="changeAdminPassword/inv7/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="changeAdminPassword/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
</org.eventb.core.psFile> </org.eventb.core.psFile>
UserManagement/UserMachine.bum
+ 91
− 55
View file @ da2402c1
This diff is collapsed.
UserManagement/UserMachine.bumx
+ 64
− 0
View file @ da2402c1
...@@ -114,4 +114,68 @@ events ...@@ -114,4 +114,68 @@ events
@act0: loggedin ≔ loggedin ∖ {user ↦ password} @act0: loggedin ≔ loggedin ∖ {user ↦ password}
end end
/*
* REQ11
* A logged in user can change their password
*/
event changePatientPassword
any
user
password
new_password
where
@grd0: user ∈ dom(patient)
@grd1: password = loggedin(user)
@grd2: new_password ∈ PASSWORD
@grd3: user ∈ dom(loggedin) // Patient must be logged in
then
@act0: loggedin ≔ loggedin  {user ↦ new_password}
@act1: registered ≔ registered  {user ↦ new_password}
@act2: patient ≔ patient  {user ↦ new_password}
end
/*
* REQ11
* A logged in user can change their password
*/
event changeDentistPassword
any
user
password
new_password
where
@grd0: user ∈ dom(dentist)
@grd1: password = loggedin(user)
@grd2: new_password ∈ PASSWORD
@grd3: user ∈ dom(loggedin) // Patient must be logged in
then
@act0: loggedin ≔ loggedin  {user ↦ new_password}
@act1: registered ≔ registered  {user ↦ new_password}
@act2: dentist ≔ dentist  {user ↦ new_password}
end
/*
* REQ11
* A logged in user can change their password
*/
event changeAdminPassword
any
user
password
new_password
where
@grd0: user ∈ dom(admin)
@grd1: password = loggedin(user)
@grd2: new_password ∈ PASSWORD
@grd3: user ∈ dom(loggedin) // Patient must be logged in
then
@act0: loggedin ≔ loggedin  {user ↦ new_password}
@act1: registered ≔ registered  {user ↦ new_password}
@act2: admin ≔ admin  {user ↦ new_password}
end
end end
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment