<?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.scSeesContext name="SEES0" org.eventb.core.scTarget="/Exemple_Mine_pump/MineContext.bcc" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|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/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.invariant#inv4" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV1" org.eventb.core.label="MinePump_inv3" org.eventb.core.predicate="bell∈MINE → BOOL" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.invariant#inv5" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV2" org.eventb.core.label="MinePump_inv4" org.eventb.core.predicate="methane∈MINE → BOOL" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.invariant#inv6" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV3" org.eventb.core.label="MinePump_inv7" org.eventb.core.predicate="dom(bell)=MINE" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.invariant#inv7" org.eventb.core.theorem="true"/>
<org.eventb.core.scInvariant name="INV4" org.eventb.core.label="MinePump_inv8" org.eventb.core.predicate="dom(methane)=MINE" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.invariant#inv8" org.eventb.core.theorem="true"/>
<org.eventb.core.scVariable name="MINE" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.variable#set3" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.scVariable name="bell" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.variable#set1" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<org.eventb.core.scVariable name="methane" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.variable#set2" org.eventb.core.type="ℙ(MINE_SET×BOOL)"/>
<org.eventb.core.scEvent name="EVT0" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|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/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.event#evt1|org.eventb.core.action#'"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="bell ≔ (∅ ⦂ ℙ(MINE_SET×BOOL))" org.eventb.core.label="act3" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.event#evt1|org.eventb.core.action#("/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="methane ≔ (∅ ⦂ ℙ(MINE_SET×BOOL))" org.eventb.core.label="act4" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|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="updateBell" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.event#evt2">
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="m∈MINE" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.event#evt2|org.eventb.core.guard#(" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="status∈BOOL" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.event#evt2|org.eventb.core.guard#element1" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.event#evt2|org.eventb.core.parameter#'" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.scParameter name="status" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.event#evt2|org.eventb.core.parameter#element1" org.eventb.core.type="BOOL"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="bell ≔ bell{m ↦ status}" org.eventb.core.label="act1" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.event#evt2|org.eventb.core.action#element3"/>
</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="updateMethane" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.event#evt3">
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="m∈MINE" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.event#evt3|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="status∈BOOL" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.event#evt3|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="m" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.event#evt3|org.eventb.core.parameter#'" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.scParameter name="status" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.event#evt3|org.eventb.core.parameter#(" org.eventb.core.type="BOOL"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="methane ≔ methane{m ↦ status}" org.eventb.core.label="act1" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.event#evt3|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="addMine" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.event#evt4">
<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/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.event#evt4|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/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.event#evt4|org.eventb.core.action#("/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="bell ≔ bell{M ↦ FALSE}" org.eventb.core.label="act3" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.event#evt4|org.eventb.core.action#)"/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="methane ≔ methane{M ↦ FALSE}" org.eventb.core.label="act4" org.eventb.core.source="/Exemple_Mine_pump/AlarmController.bum|org.eventb.core.machineFile#AlarmController|org.eventb.core.event#evt4|org.eventb.core.action#*"/>
</org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>
