<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" version="5">
<org.eventb.core.refinesMachine name="'" org.eventb.core.target="MinePump"/>
<org.eventb.core.seesContext name="(" org.eventb.core.target="MineContext"/>
<org.eventb.core.variable name="set1" org.eventb.core.identifier="MINE"/>
<org.eventb.core.variable name="set2" org.eventb.core.identifier="pump"/>
<org.eventb.core.variable name="set3" org.eventb.core.identifier="bell"/>
<org.eventb.core.variable name="set4" org.eventb.core.identifier="methane"/>
<org.eventb.core.variable name="set5" org.eventb.core.identifier="waterLevel"/>
<org.eventb.core.event name="evt1" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION"/>
<org.eventb.core.event name="evt6" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="addMine">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="addMine"/>
</org.eventb.core.event>
<org.eventb.core.event name="evt7" org.eventb.core.comment="Internal Event" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="trigger_alarm">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="updateBell"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="m"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="m ∈ MINE"/>
<org.eventb.core.witness name="*" org.eventb.core.label="status" org.eventb.core.predicate="status = TRUE"/>
<org.eventb.core.guard name="+" org.eventb.core.label="grd2" org.eventb.core.predicate="methane(m) = TRUE"/>
<org.eventb.core.guard name="," org.eventb.core.label="grd3" org.eventb.core.predicate="bell(m) = FALSE"/>
<org.eventb.core.action name="-" org.eventb.core.assignment="bell(m) ≔ TRUE" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="evt8" org.eventb.core.comment="Internal Event" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="methane_leak">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="updateMethane"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="m"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="m ∈ MINE"/>
<org.eventb.core.witness name="*" org.eventb.core.label="status" org.eventb.core.predicate="status = TRUE"/>
<org.eventb.core.action name="+" org.eventb.core.assignment="methane(m) ≔ TRUE" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="evt9" org.eventb.core.comment="Internal Event" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="high_water_detected">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="updatePump"/>
<org.eventb.core.parameter name=")" org.eventb.core.identifier="m"/>
<org.eventb.core.guard name="*" org.eventb.core.label="grd2" org.eventb.core.predicate="m ∈ MINE"/>
<org.eventb.core.action name="+" org.eventb.core.assignment="pump(m) ≔ ON" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="waterLevel(m) = HIGH"/>
<org.eventb.core.guard name="/" org.eventb.core.label="grd3" org.eventb.core.predicate="methane(m) = FALSE"/>
<org.eventb.core.guard name="0" org.eventb.core.label="grd4" org.eventb.core.predicate="pump(m) = OFF"/>
</org.eventb.core.event>
<org.eventb.core.event name="evt10" org.eventb.core.comment="Internal Event" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="low_water_detected">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="updatePump"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="m"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="m ∈ MINE"/>
<org.eventb.core.guard name="*" org.eventb.core.label="grd2" org.eventb.core.predicate="waterLevel(m) = LOW"/>
<org.eventb.core.action name="," org.eventb.core.assignment="pump(m) ≔ OFF" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="-" org.eventb.core.label="grd3" org.eventb.core.predicate="pump(m) = ON"/>
</org.eventb.core.event>
<org.eventb.core.event name="evt11" org.eventb.core.comment="Internal Event" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="methane_detected">
<org.eventb.core.parameter name="'" org.eventb.core.identifier="m"/>
<org.eventb.core.refinesEvent name="(" org.eventb.core.target="updatePump"/>
<org.eventb.core.guard name="element1" org.eventb.core.label="grd1" org.eventb.core.predicate="m ∈ MINE"/>
<org.eventb.core.guard name="element3" org.eventb.core.label="grd3" org.eventb.core.predicate="pump(m) = ON"/>
<org.eventb.core.guard name="element4" org.eventb.core.label="grd4" org.eventb.core.predicate="methane(m) = TRUE"/>
<org.eventb.core.action name="element5" org.eventb.core.assignment="pump(m) ≔ OFF" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="evt12" org.eventb.core.comment="Internal Event" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="high_to_medium">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="updateWaterLevel"/>
<org.eventb.core.parameter name=")" org.eventb.core.identifier="m"/>
<org.eventb.core.guard name="*" org.eventb.core.label="grd1" org.eventb.core.predicate="m ∈ MINE"/>
<org.eventb.core.guard name="+" org.eventb.core.label="grd2" org.eventb.core.predicate="waterLevel(m) = HIGH"/>
<org.eventb.core.action name="," org.eventb.core.assignment="waterLevel(m) ≔ MEDIUM" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="evt13" org.eventb.core.comment="Internal Event" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="medium_to_low">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="updateWaterLevel"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="m"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="m ∈ MINE"/>
<org.eventb.core.guard name="+" org.eventb.core.label="grd2" org.eventb.core.predicate="waterLevel(m) = MEDIUM"/>
<org.eventb.core.action name="," org.eventb.core.assignment="waterLevel(m) ≔ LOW" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="evt14" org.eventb.core.comment="Internal Event" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="low_to_medium">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="updateWaterLevel"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="m"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="m ∈ MINE"/>
<org.eventb.core.action name="+" org.eventb.core.assignment="waterLevel(m) ≔ MEDIUM" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="," org.eventb.core.label="grd2" org.eventb.core.predicate="waterLevel(m) = LOW"/>
</org.eventb.core.event>
<org.eventb.core.event name="evt15" org.eventb.core.comment="Internal Event" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="medium_to_high">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="updateWaterLevel"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="m"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="m ∈ MINE"/>
<org.eventb.core.guard name="+" org.eventb.core.label="grd2" org.eventb.core.predicate="waterLevel(m) = MEDIUM"/>
<org.eventb.core.action name="," org.eventb.core.assignment="waterLevel(m) ≔ HIGH" org.eventb.core.label="act1"/>
</org.eventb.core.event>
</org.eventb.core.machineFile>
