<?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="REF" org.eventb.core.scTarget="/Exemple_Mine_pump/MinePump.bcm" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.refinesMachine#'"/>
<org.eventb.core.scSeesContext name="SEES0" org.eventb.core.scTarget="/Exemple_Mine_pump/MineContext.bcc" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.seesContext#("/>
<org.eventb.core.scInternalContext name="MineContext">
<org.eventb.core.scAxiom name="AXM0" org.eventb.core.label="axm1" org.eventb.core.predicate="partition(ONOFF,{ON},{OFF})" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.axiom#axm1" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="AXM1" org.eventb.core.label="axm2" org.eventb.core.predicate="partition(LEVEL,{LOW},{MEDIUM},{HIGH})" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.axiom#axm2" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="AXM2" org.eventb.core.label="axm3" org.eventb.core.predicate="partition(MINE_SET,{M})" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.axiom#axm3" org.eventb.core.theorem="false"/>
<org.eventb.core.scConstant name="HIGH" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.constant#cst5" org.eventb.core.type="LEVEL"/>
<org.eventb.core.scCarrierSet name="LEVEL" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.carrierSet#set2" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.scConstant name="LOW" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.constant#cst3" org.eventb.core.type="LEVEL"/>
<org.eventb.core.scConstant name="M" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.constant#cst6" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.scConstant name="MEDIUM" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.constant#cst4" org.eventb.core.type="LEVEL"/>
<org.eventb.core.scCarrierSet name="MINE_SET" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.carrierSet#set3" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.scConstant name="OFF" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.constant#cst2" org.eventb.core.type="ONOFF"/>
<org.eventb.core.scConstant name="ON" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.constant#cst1" org.eventb.core.type="ONOFF"/>
<org.eventb.core.scCarrierSet name="ONOFF" org.eventb.core.source="/Exemple_Mine_pump/MineContext.buc|org.eventb.core.contextFile#MineContext|org.eventb.core.carrierSet#set1" org.eventb.core.type="ℙ(ONOFF)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInvariant name="INV0" org.eventb.core.label="inv1" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv1" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV1" org.eventb.core.label="inv2" org.eventb.core.predicate="pump∈MINE → ONOFF" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv2" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV2" org.eventb.core.label="inv3" org.eventb.core.predicate="bell∈MINE → BOOL" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv3" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV3" org.eventb.core.label="inv4" org.eventb.core.predicate="methane∈MINE → BOOL" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv4" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV4" org.eventb.core.label="inv5" org.eventb.core.predicate="waterLevel∈MINE → LEVEL" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv5" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV5" org.eventb.core.label="inv6" org.eventb.core.predicate="dom(pump)=MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv6" org.eventb.core.theorem="true"/>
<org.eventb.core.scInvariant name="INV6" org.eventb.core.label="inv7" org.eventb.core.predicate="dom(bell)=MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv7" org.eventb.core.theorem="true"/>
<org.eventb.core.scInvariant name="INV7" org.eventb.core.label="inv8" org.eventb.core.predicate="dom(methane)=MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv8" org.eventb.core.theorem="true"/>
<org.eventb.core.scInvariant name="INV8" org.eventb.core.label="inv9" org.eventb.core.predicate="dom(waterLevel)=MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#inv9" org.eventb.core.theorem="true"/>
<org.eventb.core.scInvariant name="INV9" org.eventb.core.label="inv10" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒pump(m)=ON∨pump(m)=OFF" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#set6" org.eventb.core.theorem="true"/>
<org.eventb.core.scInvariant name="INV10" org.eventb.core.label="inv11" org.eventb.core.predicate="MINE⊆MINE_SET" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#set7" org.eventb.core.theorem="true"/>
<org.eventb.core.scInvariant name="INV11" org.eventb.core.label="inv12" org.eventb.core.predicate="∀m⦂MINE_SET·m∈MINE⇒waterLevel(m)=LOW∨waterLevel(m)=MEDIUM∨waterLevel(m)=HIGH" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.invariant#set8" org.eventb.core.theorem="true"/>
<org.eventb.core.scVariable name="MINE" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.variable#set1" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.scVariable name="bell" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.variable#set3" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<org.eventb.core.scVariable name="methane" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.variable#set4" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<org.eventb.core.scVariable name="pump" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.variable#set2" org.eventb.core.type="ℙ(MINE_SET×ONOFF)"/>
<org.eventb.core.scVariable name="waterLevel" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.variable#set5" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
<org.eventb.core.scEvent name="EVT0" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt1">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/Exemple_Mine_pump/MinePump.bcm|org.eventb.core.scMachineFile#MinePump|org.eventb.core.scEvent#EVT0" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt1"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="MINE ≔ (∅ ⦂ ℙ(MINE_SET))" org.eventb.core.label="act1" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt1|org.eventb.core.action#'"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="pump ≔ (∅ ⦂ ℙ(MINE_SET×ONOFF))" org.eventb.core.label="act2" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt1|org.eventb.core.action#("/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="bell ≔ (∅ ⦂ ℙ(MINE_SET×BOOL))" org.eventb.core.label="act3" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt1|org.eventb.core.action#)"/>
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="methane ≔ (∅ ⦂ ℙ(MINE_SET×BOOL))" org.eventb.core.label="act4" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt1|org.eventb.core.action#*"/>
<org.eventb.core.scAction name="ACT4" org.eventb.core.assignment="waterLevel ≔ (∅ ⦂ ℙ(MINE_SET×LEVEL))" org.eventb.core.label="act5" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt1|org.eventb.core.action#+"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT1" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="addMine" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt6">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/Exemple_Mine_pump/MinePump.bcm|org.eventb.core.scMachineFile#MinePump|org.eventb.core.scEvent#EVT5" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt6|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="MINE=(∅ ⦂ ℙ(MINE_SET))" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt6|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="MINE ≔ {M}" org.eventb.core.label="act1" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt6|org.eventb.core.action#'"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="pump ≔ pump{M ↦ OFF}" org.eventb.core.label="act2" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt6|org.eventb.core.action#("/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="bell ≔ bell{M ↦ FALSE}" org.eventb.core.label="act3" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt6|org.eventb.core.action#)"/>
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="methane ≔ methane{M ↦ FALSE}" org.eventb.core.label="act4" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt6|org.eventb.core.action#*"/>
<org.eventb.core.scAction name="ACT4" org.eventb.core.assignment="waterLevel ≔ waterLevel{M ↦ LOW}" org.eventb.core.label="act5" org.eventb.core.source="/Exemple_Mine_pump/MinePump.bum|org.eventb.core.machineFile#MinePump|org.eventb.core.event#evt6|org.eventb.core.action#+"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT2" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="trigger_alarm" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt7">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/Exemple_Mine_pump/MinePump.bcm|org.eventb.core.scMachineFile#MinePump|org.eventb.core.scEvent#EVT2" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt7|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="m∈MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt7|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="methane(m)=TRUE" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt7|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd3" org.eventb.core.predicate="bell(m)=FALSE" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt7|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt7|org.eventb.core.parameter#(" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="bell ≔ bell{m ↦ TRUE}" org.eventb.core.label="act1" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt7|org.eventb.core.action#-"/>
<org.eventb.core.scWitness name="WIT0" org.eventb.core.label="status" org.eventb.core.predicate="status=TRUE" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt7|org.eventb.core.witness#*"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT3" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="methane_leak" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt8">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/Exemple_Mine_pump/MinePump.bcm|org.eventb.core.scMachineFile#MinePump|org.eventb.core.scEvent#EVT3" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt8|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="m∈MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt8|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt8|org.eventb.core.parameter#(" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="methane ≔ methane{m ↦ TRUE}" org.eventb.core.label="act1" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt8|org.eventb.core.action#+"/>
<org.eventb.core.scWitness name="WIT0" org.eventb.core.label="status" org.eventb.core.predicate="status=TRUE" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt8|org.eventb.core.witness#*"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT4" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="high_water_detected" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt9">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/Exemple_Mine_pump/MinePump.bcm|org.eventb.core.scMachineFile#MinePump|org.eventb.core.scEvent#EVT1" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt9|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd2" org.eventb.core.predicate="m∈MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt9|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd1" org.eventb.core.predicate="waterLevel(m)=HIGH" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt9|org.eventb.core.guard#(" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd3" org.eventb.core.predicate="methane(m)=FALSE" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt9|org.eventb.core.guard#\/" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd4" org.eventb.core.predicate="pump(m)=OFF" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt9|org.eventb.core.guard#0" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt9|org.eventb.core.parameter#)" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="pump ≔ pump{m ↦ ON}" org.eventb.core.label="act1" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt9|org.eventb.core.action#+"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT5" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="low_water_detected" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt10">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/Exemple_Mine_pump/MinePump.bcm|org.eventb.core.scMachineFile#MinePump|org.eventb.core.scEvent#EVT1" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt10|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="m∈MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt10|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="waterLevel(m)=LOW" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt10|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd3" org.eventb.core.predicate="pump(m)=ON" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt10|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt10|org.eventb.core.parameter#(" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="pump ≔ pump{m ↦ OFF}" org.eventb.core.label="act1" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt10|org.eventb.core.action#,"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT6" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="methane_detected" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt11">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/Exemple_Mine_pump/MinePump.bcm|org.eventb.core.scMachineFile#MinePump|org.eventb.core.scEvent#EVT1" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt11|org.eventb.core.refinesEvent#("/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="m∈MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt11|org.eventb.core.guard#element1" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd3" org.eventb.core.predicate="pump(m)=ON" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt11|org.eventb.core.guard#element3" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd4" org.eventb.core.predicate="methane(m)=TRUE" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt11|org.eventb.core.guard#element4" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt11|org.eventb.core.parameter#'" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="pump ≔ pump{m ↦ OFF}" org.eventb.core.label="act1" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt11|org.eventb.core.action#element5"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT7" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="high_to_medium" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt12">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/Exemple_Mine_pump/MinePump.bcm|org.eventb.core.scMachineFile#MinePump|org.eventb.core.scEvent#EVT4" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt12|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="m∈MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt12|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="waterLevel(m)=HIGH" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt12|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt12|org.eventb.core.parameter#)" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="waterLevel ≔ waterLevel{m ↦ MEDIUM}" org.eventb.core.label="act1" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt12|org.eventb.core.action#,"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT8" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="medium_to_low" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt13">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/Exemple_Mine_pump/MinePump.bcm|org.eventb.core.scMachineFile#MinePump|org.eventb.core.scEvent#EVT4" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt13|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="m∈MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt13|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="waterLevel(m)=MEDIUM" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt13|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt13|org.eventb.core.parameter#(" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="waterLevel ≔ waterLevel{m ↦ LOW}" org.eventb.core.label="act1" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt13|org.eventb.core.action#,"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT9" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="low_to_medium" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt14">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/Exemple_Mine_pump/MinePump.bcm|org.eventb.core.scMachineFile#MinePump|org.eventb.core.scEvent#EVT4" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt14|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="m∈MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt14|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="waterLevel(m)=LOW" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt14|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt14|org.eventb.core.parameter#(" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="waterLevel ≔ waterLevel{m ↦ MEDIUM}" org.eventb.core.label="act1" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt14|org.eventb.core.action#+"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT10" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="medium_to_high" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt15">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/Exemple_Mine_pump/MinePump.bcm|org.eventb.core.scMachineFile#MinePump|org.eventb.core.scEvent#EVT4" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt15|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="m∈MINE" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt15|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="waterLevel(m)=MEDIUM" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt15|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt15|org.eventb.core.parameter#(" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="waterLevel ≔ waterLevel{m ↦ HIGH}" org.eventb.core.label="act1" org.eventb.core.source="/Exemple_Mine_pump/MinePumpReunification.bum|org.eventb.core.machineFile#MinePumpReunification|org.eventb.core.event#evt15|org.eventb.core.action#,"/>
</org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>
