m2_modules.bcm

<?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">
<org.eventb.core.scRefinesMachine name="'" org.eventb.core.scTarget="/progmanmodel/m1_programmes.bcm" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.refinesMachine#'"/>
<org.eventb.core.scSeesContext name="(" org.eventb.core.scTarget="/progmanmodel/c2_modules.bcc" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.seesContext#_AGA7QEHJEeqHd7PiYTbxHg"/>
<org.eventb.core.scInternalContext name="c0_users">
<org.eventb.core.scCarrierSet name="USER" org.eventb.core.source="/progmanmodel/c0_users.buc|org.eventb.core.contextFile#c0_users|org.eventb.core.carrierSet#_swFc0EHSEeqHCPZ-G665YQ" org.eventb.core.type="ℙ(USER)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInternalContext name="c1_programmes">
<org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/progmanmodel/c0_users.bcc|org.eventb.core.scContextFile#c0_users" org.eventb.core.source="/progmanmodel/c1_programmes.buc|org.eventb.core.contextFile#c1_programmes|org.eventb.core.extendsContext#_qcMHkEHSEeqHCPZ-G665YQ"/>
<org.eventb.core.scCarrierSet name="PROGRAMME" org.eventb.core.source="/progmanmodel/c1_programmes.buc|org.eventb.core.contextFile#c1_programmes|org.eventb.core.carrierSet#_qcMuoEHSEeqHCPZ-G665YQ" org.eventb.core.type="ℙ(PROGRAMME)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInternalContext name="c2_modules">
<org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/progmanmodel/c1_programmes.bcc|org.eventb.core.scContextFile#c1_programmes" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.extendsContext#_fuhrAEHSEeqHCPZ-G665YQ"/>
<org.eventb.core.scAxiom name="c1_programmet" org.eventb.core.label="axm21" org.eventb.core.predicate="credits={15,30,45,60}" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.axiom#_rGOvUUgCEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="c1_programmeu" org.eventb.core.label="axm22" org.eventb.core.predicate="sum∈(MODULE ↔ credits) → ℕ" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.axiom#_Ut5fQE5AEeqUxct8tLY9IA" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="c1_programmev" org.eventb.core.label="axm23" org.eventb.core.predicate="sum(∅ ⦂ ℙ(MODULE×ℤ))=0" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.axiom#_Ut5fQU5AEeqUxct8tLY9IA" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="c1_programmew" org.eventb.core.label="sum24" org.eventb.core.predicate="∀f⦂ℙ(MODULE×ℤ),m⦂MODULE·f∈MODULE ⇸ credits∧m∈dom(f)⇒sum(f)=sum({m} ⩤ f)+f(m)" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.axiom#_duc5wE5AEeqUxct8tLY9IA" org.eventb.core.theorem="false"/>
<org.eventb.core.scCarrierSet name="MODULE" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.carrierSet#_fuiSEEHSEeqHCPZ-G665YQ" org.eventb.core.type="ℙ(MODULE)"/>
<org.eventb.core.scConstant name="credits" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.constant#_rGOvUEgCEeqeqbGZOOBkaQ" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scConstant name="sum" org.eventb.core.source="/progmanmodel/c2_modules.buc|org.eventb.core.contextFile#c2_modules|org.eventb.core.constant#_Ut44ME5AEeqUxct8tLY9IA" org.eventb.core.type="ℙ(ℙ(MODULE×ℤ)×ℤ)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInvariant name="c0_usert" org.eventb.core.label="inv1" org.eventb.core.predicate="registered⊆USER" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.invariant#_QUDCYEHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c0_useru" org.eventb.core.label="inv2" org.eventb.core.predicate="logged_in⊆registered" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.invariant#_QUDpcEHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmet" org.eventb.core.label="inv11" org.eventb.core.predicate="programmes⊆PROGRAMME" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_liiugEHGEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmeu" org.eventb.core.label="inv12" org.eventb.core.predicate="programme_leader∈programmes → registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMEHGEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmev" org.eventb.core.label="inv13" org.eventb.core.predicate="administrators∈programmes ↔ registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_vOAHMUHGEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmew" org.eventb.core.label="inv14" org.eventb.core.predicate="published⊆programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.invariant#_Uat4UUgQEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmex" org.eventb.core.label="inv21" org.eventb.core.predicate="modules⊆MODULE" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.invariant#_AGHo8UHJEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmey" org.eventb.core.label="inv22" org.eventb.core.predicate="contains_module∈programmes ↔ modules" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.invariant#_FmSs8EHJEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programmez" org.eventb.core.label="inv23" org.eventb.core.predicate="module_leader∈modules → registered" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.invariant#_FmSs8UHJEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programme{" org.eventb.core.label="inv24" org.eventb.core.predicate="credits_awarded∈modules → credits" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.invariant#_2Be78EgCEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="c1_programme|" org.eventb.core.label="inv25" org.eventb.core.predicate="credits_awarded∈MODULE ⇸ credits" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.invariant#_dxz9oFGfEeq01sNmetMbsA" org.eventb.core.theorem="false"/>
<org.eventb.core.scVariable name="administrators" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.variable#_vN_gIUHGEeqHd7PiYTbxHg" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.scVariable name="contains_module" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.variable#_AGHB4UHJEeqHd7PiYTbxHg" org.eventb.core.type="ℙ(PROGRAMME×MODULE)"/>
<org.eventb.core.scVariable name="credits_awarded" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.variable#_2BeU4EgCEeqeqbGZOOBkaQ" org.eventb.core.type="ℙ(MODULE×ℤ)"/>
<org.eventb.core.scVariable name="logged_in" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.variable#_MTJYwEHEEeqKzaOTi1o2gg" org.eventb.core.type="ℙ(USER)"/>
<org.eventb.core.scVariable name="module_leader" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.variable#_AGHo8EHJEeqHd7PiYTbxHg" org.eventb.core.type="ℙ(MODULE×USER)"/>
<org.eventb.core.scVariable name="modules" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.variable#_AGHB4EHJEeqHd7PiYTbxHg" org.eventb.core.type="ℙ(MODULE)"/>
<org.eventb.core.scVariable name="programme_leader" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.variable#_vN_gIEHGEeqHd7PiYTbxHg" org.eventb.core.type="ℙ(PROGRAMME×USER)"/>
<org.eventb.core.scVariable name="programmes" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.variable#_iY418EHGEeqHd7PiYTbxHg" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.scVariable name="published" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.variable#_v6HsYEgTEeqeqbGZOOBkaQ" org.eventb.core.type="ℙ(PROGRAMME)"/>
<org.eventb.core.scVariable name="registered" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.variable#_MTIxsEHEEeqKzaOTi1o2gg" org.eventb.core.type="ℙ(USER)"/>
<org.eventb.core.scEvent name="programme_leades" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m1_programmes.bcm|org.eventb.core.scMachineFile#m1_programmes|org.eventb.core.scEvent#programme_leades" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh"/>
<org.eventb.core.scAction name="'" org.eventb.core.assignment="registered ≔ ∅ ⦂ ℙ(USER)" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#'|org.eventb.core.action#_TSDroEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.scAction name="(" org.eventb.core.assignment="logged_in ≔ ∅ ⦂ ℙ(USER)" org.eventb.core.label="act2" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#'|org.eventb.core.action#_TSESsEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.scAction name=")" org.eventb.core.assignment="programmes ≔ ∅ ⦂ ℙ(PROGRAMME)" org.eventb.core.label="act11" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gh|org.eventb.core.action#_0s5_4EHGEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="*" org.eventb.core.assignment="programme_leader ≔ ∅ ⦂ ℙ(PROGRAMME×USER)" org.eventb.core.label="act12" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gh|org.eventb.core.action#_0s5_4UHGEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="+" org.eventb.core.assignment="administrators ≔ ∅ ⦂ ℙ(PROGRAMME×USER)" org.eventb.core.label="act13" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gh|org.eventb.core.action#_0s5_4kHGEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="," org.eventb.core.assignment="published ≔ ∅ ⦂ ℙ(PROGRAMME)" org.eventb.core.label="act14" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gh|org.eventb.core.action#_3ZnrMEgQEeqeqbGZOOBkaQ"/>
<org.eventb.core.scAction name="-" org.eventb.core.assignment="modules ≔ ∅ ⦂ ℙ(MODULE)" org.eventb.core.label="act21" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh|org.eventb.core.action#_LP_gYEHJEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="." org.eventb.core.assignment="contains_module ≔ ∅ ⦂ ℙ(PROGRAMME×MODULE)" org.eventb.core.label="act22" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh|org.eventb.core.action#_LP_gYUHJEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="/" org.eventb.core.assignment="module_leader ≔ ∅ ⦂ ℙ(MODULE×USER)" org.eventb.core.label="act23" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh|org.eventb.core.action#_LQAHcEHJEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="0" org.eventb.core.assignment="credits_awarded ≔ ∅ ⦂ ℙ(MODULE×ℤ)" org.eventb.core.label="act24" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHh|org.eventb.core.action#_5qwvwEgCEeqeqbGZOOBkaQ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leadet" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="create_module" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_n5An4kHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="m∈MODULE" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_n5BO8EHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="c∈credits" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_n5BO8UHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="m∉modules" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_8qbBUUHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="c" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_2BPrYEgCEeqeqbGZOOBkaQ" org.eventb.core.type="ℤ"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_n5An4UHMEeqHd7PiYTbxHg" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_n5An4EHMEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="modules ≔ modules∪{m}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.action#_n5B2AEHMEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="w" org.eventb.core.assignment="module_leader ≔ module_leader{m ↦ u}" org.eventb.core.label="act2" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.action#_n5B2AUHMEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="x" org.eventb.core.assignment="credits_awarded ≔ credits_awarded{m ↦ c}" org.eventb.core.label="act3" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq0TMEHJEeqHd7PiYTbxHg|org.eventb.core.action#_BcveUEgDEeqeqbGZOOBkaQ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leadeu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="delete_module" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QEHJEeqHd7PiYTbxHg">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_uxVxokHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="m∈modules" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_uxWYsEHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="module_leader(m)=u" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_uxWYsUHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="m∉ran(contains_module)" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_xMTiwUHNEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QEHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_uxVxoUHMEeqHd7PiYTbxHg" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QEHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_uxVxoEHMEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="modules ≔ modules ∖ {m}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QEHJEeqHd7PiYTbxHg|org.eventb.core.action#_uxWYskHMEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="w" org.eventb.core.assignment="module_leader ≔ {m} ⩤ module_leader" org.eventb.core.label="act2" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QEHJEeqHd7PiYTbxHg|org.eventb.core.action#_uxW_wEHMEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="x" org.eventb.core.assignment="credits_awarded ≔ {m} ⩤ credits_awarded" org.eventb.core.label="act3" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QEHJEeqHd7PiYTbxHg|org.eventb.core.action#_1tqOwEgHEeqeqbGZOOBkaQ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leadev" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="assign_module" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.guard#_8qaaQEHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="m∈modules" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.guard#_8qaaQUHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.guard#_8qbBUEHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="u∈administrators[{p}]" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.guard#_xMVX8UHNEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd6" org.eventb.core.predicate="m∉contains_module[{p}]" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.guard#_8qboYEHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd7" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.guard#_K8nhAEgiEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_8qZzMUHMEeqHd7PiYTbxHg" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_8qZzMkHMEeqHd7PiYTbxHg" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_8qZzMEHMEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="contains_module ≔ contains_module∪{p ↦ m}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QUHJEeqHd7PiYTbxHg|org.eventb.core.action#_B5a1wEHNEeqHd7PiYTbxHg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leadew" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="unassign_module" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.guard#_xMS7sEHNEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="m∈modules" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.guard#_xMS7sUHNEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.guard#_xMTiwEHNEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="u∈administrators[{p}]" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.guard#_rcwJgEHOEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="m∈contains_module[{p}]" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.guard#_8qbBUkHMEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.guard#_K8pWMEgiEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_xMSUoUHNEeqHd7PiYTbxHg" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_xMSUokHNEeqHd7PiYTbxHg" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_xMSUoEHNEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="contains_module ≔ contains_module ∖ {p ↦ m}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq06QkHJEeqHd7PiYTbxHg|org.eventb.core.action#_xMUJ0EHNEeqHd7PiYTbxHg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leadex" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="transfer_module_ownership" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq1hUEHJEeqHd7PiYTbxHg">
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u1∈logged_in" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq1hUEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_xMUw4UHNEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u2∈registered" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq1hUEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_xMUw4kHNEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="m∈modules" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq1hUEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_xMVX8EHNEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="module_leader(m)=u1" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq1hUEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_5q6gwEgCEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="u1≠u2" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq1hUEHJEeqHd7PiYTbxHg|org.eventb.core.guard#_xMTiwkHNEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq1hUEHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_xMUw4EHNEeqHd7PiYTbxHg" org.eventb.core.type="MODULE"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq1hUEHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_xMUJ0UHNEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq1hUEHJEeqHd7PiYTbxHg|org.eventb.core.parameter#_xMUJ0kHNEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="module_leader ≔ module_leader{m ↦ u2}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_Sq1hUEHJEeqHd7PiYTbxHg|org.eventb.core.action#_1unQUEHNEeqHd7PiYTbxHg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leadey" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="publish_programme" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_uWIKEEgTEeqeqbGZOOBkaQ">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m1_programmes.bcm|org.eventb.core.scMachineFile#m1_programmes|org.eventb.core.scEvent#programme_leadet" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_uWIKEEgTEeqeqbGZOOBkaQ|org.eventb.core.refinesEvent#_uWIxIEgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_JVqzoEHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_JVqzoUHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="u=programme_leader(p)" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_JVqzokHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_sioQokHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="published ≔ published∪{p}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.action#_JVrasEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.parameter#_JVqMkkHHEeqHd7PiYTbxHg" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpYtQEgTEeqeqbGZOOBkaQ|org.eventb.core.parameter#_JVqMkUHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leadez" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="unpublish_programme" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_uWIxIUgTEeqeqbGZOOBkaQ">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m1_programmes.bcm|org.eventb.core.scMachineFile#m1_programmes|org.eventb.core.scEvent#programme_leadeu" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_uWIxIUgTEeqeqbGZOOBkaQ|org.eventb.core.refinesEvent#_uWIxIkgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_g_lrQEHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_g_mSUEHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="u=programme_leader(p)" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_g_mSUUHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="p∈published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.guard#_3BElcEHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="published ≔ published ∖ {p}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.action#_g_m5YEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.parameter#_ROOEQEHHEeqHd7PiYTbxHg" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_gpaicEgTEeqeqbGZOOBkaQ|org.eventb.core.parameter#_RONdMEHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leade{" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="create_programme" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHi">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m1_programmes.bcm|org.eventb.core.scMachineFile#m1_programmes|org.eventb.core.scEvent#programme_leadev" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHi|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_sinpkUHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="p∈PROGRAMME" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_sioQoEHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="p∉programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_sioQoUHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="programmes ≔ programmes∪{p}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.action#_x9OREEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="w" org.eventb.core.assignment="programme_leader ≔ programme_leader{p ↦ u}" org.eventb.core.label="act2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.action#_JVrasUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="x" org.eventb.core.assignment="administrators ≔ administrators∪{p ↦ u}" org.eventb.core.label="act3" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.action#_ROM2IEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_sinpkEHHEeqHd7PiYTbxHg" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVqMkEHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_gpeM0EgTEeqeqbGZOOBkaQ" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leade|" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="delete_programme" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHj">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m1_programmes.bcm|org.eventb.core.scMachineFile#m1_programmes|org.eventb.core.scEvent#programme_leadew" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHj|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_3BD-YEHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_3BD-YUHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="programme_leader(p)=u" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_3BD-YkHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nL08UHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="programmes ≔ programmes ∖ {p}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.action#_3BFMgEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="w" org.eventb.core.assignment="programme_leader ≔ {p} ⩤ programme_leader" org.eventb.core.label="act2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.action#_g_m5YUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scAction name="x" org.eventb.core.assignment="administrators ≔ {p} ⩤ administrators" org.eventb.core.label="act3" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.action#_g_ngcEHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_3BDXUkHHEeqHd7PiYTbxHg" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwEHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_oWwBkEgTEeqeqbGZOOBkaQ" org.eventb.core.type="USER"/>
<org.eventb.core.scAction name="y" org.eventb.core.assignment="contains_module ≔ {p} ⩤ contains_module" org.eventb.core.label="act21" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHj|org.eventb.core.action#_oc4CkEHPEeqHd7PiYTbxHg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leade}" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="add_administrator" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHk">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m1_programmes.bcm|org.eventb.core.scMachineFile#m1_programmes|org.eventb.core.scEvent#programme_leadex" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHk|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u1∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nLN4UHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u2∈registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nLN4kHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nL08EHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="programme_leader(p)=u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_gpmIoEgTEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="u2∉administrators[{p}]" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_sio3sEHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.guard#_cDwN8EHIEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="administrators ≔ administrators∪{p ↦ u2}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.action#_7nMcAUHHEeqHd7PiYTbxHg"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_7nLN4EHHEeqHd7PiYTbxHg" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_sinCgEHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwUHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_sinCgUHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leade~" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="remove_administrator" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHl">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m1_programmes.bcm|org.eventb.core.scMachineFile#m1_programmes|org.eventb.core.scEvent#programme_leadey" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHl|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u1∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_gpk6gEgTEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u2∈registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_gplhkEgTEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_gplhkUgTEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="programme_leader(p)=u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_oW1hIkgTEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="u2∈administrators[{p}]" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_3BElcUHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="u1≠u2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_eZxgUEc9EeqCJoBEKqsuQA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="-" org.eventb.core.label="grd7" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.guard#_WXhJ8EgVEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="administrators ≔ administrators ∖ {p ↦ u2}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.action#_gpmvsUgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_gpmvsEgTEeqeqbGZOOBkaQ" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_3BDXUEHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVsBwkHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_3BDXUUHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leadf'" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="transfer_ownership" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHm">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m1_programmes.bcm|org.eventb.core.scMachineFile#m1_programmes|org.eventb.core.scEvent#programme_leadez" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHm|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u1∈logged_in" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_oW06EEgTEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u2∈registered" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_oW1hIEgTEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="p∈programmes" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_oW1hIUgTEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="programme_leader(p)=u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_aUM3YEgUEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="u2∈administrators[{p}]" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_7nMcAEHHEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="u1≠u2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_bx1dkEgVEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="-" org.eventb.core.label="grd7" org.eventb.core.predicate="p∉published" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.guard#_bx1dkUgVEeqeqbGZOOBkaQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="u3" org.eventb.core.assignment="programme_leader ≔ programme_leader{p ↦ u2}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.action#_oW2IMUgTEeqeqbGZOOBkaQ"/>
<org.eventb.core.scParameter name="p" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_oW2IMEgTEeqeqbGZOOBkaQ" org.eventb.core.type="PROGRAMME"/>
<org.eventb.core.scParameter name="u1" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_7nKm0EHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
<org.eventb.core.scParameter name="u2" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_JVso0EHHEeqHd7PiYTbxHg|org.eventb.core.parameter#_7nKm0UHHEeqHd7PiYTbxHg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leadf(" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="register" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHn">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m1_programmes.bcm|org.eventb.core.scMachineFile#m1_programmes|org.eventb.core.scEvent#programme_leade{" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHn|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈USER" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKGUEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_eQiLYUHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u∉registered" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKGUEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_eQiycEHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="registered ≔ registered∪{u}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKGUEHEEeqKzaOTi1o2gg|org.eventb.core.action#_eQiycUHEEeqKzaOTi1o2gg"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKGUEHEEeqKzaOTi1o2gg|org.eventb.core.parameter#_eQiLYEHEEeqKzaOTi1o2gg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leadf)" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="unregister" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHo">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m1_programmes.bcm|org.eventb.core.scMachineFile#m1_programmes|org.eventb.core.scEvent#programme_leade\|" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHo|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈registered" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKtYEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_eQjZgUHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u∉logged_in" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKtYEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_eQkAkEHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="w" org.eventb.core.label="grd11" org.eventb.core.predicate="u∉ran(programme_leader)" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gj|org.eventb.core.guard#_CWPG4EHIEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="x" org.eventb.core.label="grd12" org.eventb.core.predicate="u∉ran(administrators)" org.eventb.core.source="/progmanmodel/m1_programmes.bum|org.eventb.core.machineFile#m1_programmes|org.eventb.core.event#_MTJYwEHEEeqKzaOTi1o2gj|org.eventb.core.guard#_CWPG4UHIEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="registered ≔ registered ∖ {u}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKtYEHEEeqKzaOTi1o2gg|org.eventb.core.action#_eQknoEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnKtYEHEEeqKzaOTi1o2gg|org.eventb.core.parameter#_eQjZgEHEEeqKzaOTi1o2gg" org.eventb.core.type="USER"/>
<org.eventb.core.scGuard name="y" org.eventb.core.label="grd21" org.eventb.core.predicate="u∉ran(module_leader)" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHo|org.eventb.core.guard#_mWA5MEHOEeqHd7PiYTbxHg" org.eventb.core.theorem="false"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leadf*" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="login" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHp">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m1_programmes.bcm|org.eventb.core.scMachineFile#m1_programmes|org.eventb.core.scEvent#programme_leade}" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHp|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈registered" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnL7gEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_iqZHkUHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u∉logged_in" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnL7gEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_iqZuoEHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="logged_in ≔ logged_in∪{u}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnL7gEHEEeqKzaOTi1o2gg|org.eventb.core.action#_iqZuoUHEEeqKzaOTi1o2gg"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnL7gEHEEeqKzaOTi1o2gg|org.eventb.core.parameter#_iqZHkEHEEeqKzaOTi1o2gg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="programme_leadf+" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="logout" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHq">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/progmanmodel/m1_programmes.bcm|org.eventb.core.scMachineFile#m1_programmes|org.eventb.core.scEvent#programme_leade~" org.eventb.core.source="/progmanmodel/m2_modules.bum|org.eventb.core.machineFile#m2_modules|org.eventb.core.event#_vN_gIUHGEeqHd7PiYTbxHq|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="u∈registered" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnMikEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_iqaVsUHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="u∈logged_in" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnMikEHEEeqKzaOTi1o2gg|org.eventb.core.guard#_iqaVskHEEeqKzaOTi1o2gg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="v" org.eventb.core.assignment="logged_in ≔ logged_in ∖ {u}" org.eventb.core.label="act1" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnMikEHEEeqKzaOTi1o2gg|org.eventb.core.action#_iqa8wEHEEeqKzaOTi1o2gg"/>
<org.eventb.core.scParameter name="u" org.eventb.core.source="/progmanmodel/m0_users.bum|org.eventb.core.machineFile#m0_users|org.eventb.core.event#_GnMikEHEEeqKzaOTi1o2gg|org.eventb.core.parameter#_iqaVsEHEEeqKzaOTi1o2gg" org.eventb.core.type="USER"/>
</org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>