<?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/WaterLevelSensor.bcm" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|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/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|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="MinePump_inv1" org.eventb.core.predicate="MINE∈ℙ(MINE_SET)" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|org.eventb.core.invariant#inv3" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV1" org.eventb.core.label="MinePump_inv5" org.eventb.core.predicate="waterLevel∈MINE → LEVEL" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|org.eventb.core.invariant#inv4" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV2" org.eventb.core.label="MinePump_inv9" org.eventb.core.predicate="dom(waterLevel)=MINE" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|org.eventb.core.invariant#inv5" 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/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.variable#set2" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.scVariable name="waterLevel" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.variable#set1" 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/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt1">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/Exemple_Mine_pump/WaterLevelSensor.bcm|org.eventb.core.scMachineFile#WaterLevelSensor|org.eventb.core.scEvent#EVT0" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|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/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|org.eventb.core.event#evt1|org.eventb.core.action#'"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="waterLevel ≔ (∅ ⦂ ℙ(MINE_SET×LEVEL))" org.eventb.core.label="act5" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|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="false" org.eventb.core.label="high_to_medium" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt4">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/Exemple_Mine_pump/WaterLevelSensor.bcm|org.eventb.core.scMachineFile#WaterLevelSensor|org.eventb.core.scEvent#EVT1" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt4|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/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt4|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/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt4|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt4|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/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt4|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="medium_to_low" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt5">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/Exemple_Mine_pump/WaterLevelSensor.bcm|org.eventb.core.scMachineFile#WaterLevelSensor|org.eventb.core.scEvent#EVT1" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt5|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/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt5|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/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt5|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt5|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/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt5|org.eventb.core.action#,"/>
</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="low_to_medium" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt6">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/Exemple_Mine_pump/WaterLevelSensor.bcm|org.eventb.core.scMachineFile#WaterLevelSensor|org.eventb.core.scEvent#EVT1" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt6|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/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt6|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/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt6|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt6|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/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt6|org.eventb.core.action#+"/>
</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="medium_to_high" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt7">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/Exemple_Mine_pump/WaterLevelSensor.bcm|org.eventb.core.scMachineFile#WaterLevelSensor|org.eventb.core.scEvent#EVT1" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|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/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|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="waterLevel(m)=MEDIUM" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|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/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|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="waterLevel ≔ waterLevel{m ↦ HIGH}" org.eventb.core.label="act1" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt7|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="true" org.eventb.core.label="addMine" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt3">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/Exemple_Mine_pump/WaterLevelSensor.bcm|org.eventb.core.scMachineFile#WaterLevelSensor|org.eventb.core.scEvent#EVT2" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt3|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/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|org.eventb.core.event#evt3|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/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|org.eventb.core.event#evt3|org.eventb.core.action#("/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="waterLevel ≔ waterLevel{M ↦ LOW}" org.eventb.core.label="act5" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|org.eventb.core.event#evt3|org.eventb.core.action#)"/>
</org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>
