<?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.seesContext name="(" org.eventb.core.target="MineContext"/>
<org.eventb.core.variable ch.ethz.eventb.decomposition.nature="1" name="set1" org.eventb.core.comment="Shared variable, DO NOT REFINE" org.eventb.core.identifier="methane"/>
<org.eventb.core.variable ch.ethz.eventb.decomposition.nature="1" name="set2" org.eventb.core.comment="Shared variable, DO NOT REFINE" org.eventb.core.identifier="waterLevel"/>
<org.eventb.core.variable name="set3" org.eventb.core.comment="Shared variable, DO NOT REFINE" org.eventb.core.identifier="pump"/>
<org.eventb.core.variable ch.ethz.eventb.decomposition.nature="1" name="set4" org.eventb.core.comment="Shared variable, DO NOT REFINE" org.eventb.core.identifier="MINE"/>
<org.eventb.core.invariant name="inv5" org.eventb.core.label="MinePump_inv1" org.eventb.core.predicate="MINE ∈ ℙ(MINE_SET)"/>
<org.eventb.core.invariant name="inv6" org.eventb.core.label="MinePump_inv2" org.eventb.core.predicate="pump ∈ MINE → ONOFF"/>
<org.eventb.core.invariant name="inv7" org.eventb.core.label="MinePump_inv4" org.eventb.core.predicate="methane ∈ MINE → BOOL"/>
<org.eventb.core.invariant name="inv8" org.eventb.core.label="MinePump_inv5" org.eventb.core.predicate="waterLevel ∈ MINE → LEVEL"/>
<org.eventb.core.invariant name="inv9" org.eventb.core.label="MinePump_inv6" org.eventb.core.predicate="dom(pump) = MINE" org.eventb.core.theorem="true"/>
<org.eventb.core.invariant name="inv10" org.eventb.core.label="MinePump_inv8" org.eventb.core.predicate="dom(methane) = MINE" org.eventb.core.theorem="true"/>
<org.eventb.core.invariant name="inv11" org.eventb.core.label="MinePump_inv9" org.eventb.core.predicate="dom(waterLevel) = MINE" org.eventb.core.theorem="true"/>
<org.eventb.core.event name="evt1" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION">
<org.eventb.core.action name="'" org.eventb.core.assignment="MINE ≔ ∅" org.eventb.core.label="act1"/>
<org.eventb.core.action name="(" org.eventb.core.assignment="pump ≔ ∅" org.eventb.core.label="act2"/>
<org.eventb.core.action name=")" org.eventb.core.assignment="methane ≔ ∅" org.eventb.core.label="act4"/>
<org.eventb.core.action name="*" org.eventb.core.assignment="waterLevel ≔ ∅" org.eventb.core.label="act5"/>
</org.eventb.core.event>
<org.eventb.core.event name="evt6" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="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.action name="+" org.eventb.core.assignment="pump :∣ (pump(m) = OFF ∧ pump'=(pump  {m ↦ ON}) )&#13;&#10;  ∨ (pump(m) = ON ∧ pump'=(pump  {m ↦ OFF}))" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="," org.eventb.core.label="grd2" org.eventb.core.predicate="pump(m) = ON ∨ pump(m) = OFF" org.eventb.core.theorem="true"/>
</org.eventb.core.event>
<org.eventb.core.event ch.ethz.eventb.decomposition.external="true" name="evt7" org.eventb.core.comment="External event, DO NOT REFINE" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="updateMethane">
<org.eventb.core.parameter name="'" org.eventb.core.identifier="m"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="status"/>
<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="status ∈ BOOL"/>
<org.eventb.core.action name="+" org.eventb.core.assignment="methane(m) ≔ status" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event ch.ethz.eventb.decomposition.external="true" name="evt8" org.eventb.core.comment="External event, DO NOT REFINE" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="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 :∣ &#13;&#10;( waterLevel(m) = HIGH ∧ waterLevel'=(waterLevel  {m ↦ MEDIUM}))&#13;&#10;∨ ( waterLevel(m) = MEDIUM ∧ waterLevel'=(waterLevel  {m ↦ LOW}))&#13;&#10;∨ ( waterLevel(m) = MEDIUM ∧ waterLevel'=(waterLevel  {m ↦ HIGH}))&#13;&#10;∨ ( waterLevel(m) = LOW ∧ waterLevel'=(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 ∨&#13;&#10;waterLevel(m) = MEDIUM ∨&#13;&#10;waterLevel(m) = HIGH" org.eventb.core.theorem="true"/>
</org.eventb.core.event>
<org.eventb.core.event ch.ethz.eventb.decomposition.external="true" name="evt5" org.eventb.core.comment="External event, DO NOT REFINE" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="addMine">
<org.eventb.core.guard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="MINE = ∅"/>
<org.eventb.core.action name="(" org.eventb.core.assignment="MINE ≔ {M}" org.eventb.core.label="act1"/>
<org.eventb.core.action name=")" org.eventb.core.assignment="pump(M) ≔ OFF" org.eventb.core.label="act2"/>
<org.eventb.core.action name="*" org.eventb.core.assignment="methane(M) ≔ FALSE" org.eventb.core.label="act4"/>
<org.eventb.core.action name="+" org.eventb.core.assignment="waterLevel(M) ≔ LOW" org.eventb.core.label="act5"/>
</org.eventb.core.event>
</org.eventb.core.machineFile>
