<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="6">
<org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="6">
<org.eventb.core.poIdentifier name="LEVEL" org.eventb.core.type="ℙ(LEVEL)"/>
<org.eventb.core.poIdentifier name="MINE_SET" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.poIdentifier name="ONOFF" org.eventb.core.type="ℙ(ONOFF)"/>
<org.eventb.core.poIdentifier name="HIGH" org.eventb.core.type="LEVEL"/>
<org.eventb.core.poIdentifier name="LOW" org.eventb.core.type="LEVEL"/>
<org.eventb.core.poIdentifier name="M" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.poIdentifier name="MEDIUM" org.eventb.core.type="LEVEL"/>
<org.eventb.core.poIdentifier name="OFF" org.eventb.core.type="ONOFF"/>
<org.eventb.core.poIdentifier name="ON" org.eventb.core.type="ONOFF"/>
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="6">
<org.eventb.core.poIdentifier name="MINE" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.poIdentifier name="waterLevel" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
<org.eventb.core.poPredicate name="PRD3" 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.poPredicate name="PRD4" 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.poPredicate name="PRD5" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT0" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="6">
<org.eventb.core.poIdentifier name="MINE'" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.poIdentifier name="waterLevel'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT0" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTIDENTEVT0" org.eventb.core.poStamp="6"/>
<org.eventb.core.poSequent name="high_to_medium/grd2/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="6">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT1GRD0"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL" 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.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT1GRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="high_to_medium/act1/SIM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Action simulation" org.eventb.core.poStamp="6">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTALLHYPEVT1"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ MEDIUM})∨(waterLevel(m)=MEDIUM∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ LOW})∨(waterLevel(m)=MEDIUM∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ HIGH})∨(waterLevel(m)=LOW∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ MEDIUM})" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|org.eventb.core.event#evt4|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|org.eventb.core.event#evt4"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|org.eventb.core.event#evt4|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC2" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt4"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poSequent#high_to_medium\/act1\/SIM|org.eventb.core.poPredicateSet#SEQHYP"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT1" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="6">
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.poIdentifier name="waterLevel'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPEVT1GRD0" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTIDENTEVT1" org.eventb.core.poStamp="6">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT1" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT1GRD0" org.eventb.core.poStamp="6">
<org.eventb.core.poPredicate name="PRD1" 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.poPredicateSet>
<org.eventb.core.poSequent name="medium_to_low/grd2/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="6">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT2GRD0"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL" 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.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT2GRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="medium_to_low/act1/SIM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Action simulation" org.eventb.core.poStamp="6">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTALLHYPEVT2"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel{m ↦ LOW}=waterLevel{m ↦ MEDIUM})∨(waterLevel(m)=MEDIUM∧waterLevel{m ↦ LOW}=waterLevel{m ↦ LOW})∨(waterLevel(m)=MEDIUM∧waterLevel{m ↦ LOW}=waterLevel{m ↦ HIGH})∨(waterLevel(m)=LOW∧waterLevel{m ↦ LOW}=waterLevel{m ↦ MEDIUM})" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|org.eventb.core.event#evt4|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|org.eventb.core.event#evt4"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|org.eventb.core.event#evt4|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC2" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt5"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poSequent#medium_to_low\/act1\/SIM|org.eventb.core.poPredicateSet#SEQHYP"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT2" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="6">
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.poIdentifier name="waterLevel'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPEVT2GRD0" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTIDENTEVT2" org.eventb.core.poStamp="6">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT2" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT2GRD0" org.eventb.core.poStamp="6">
<org.eventb.core.poPredicate name="PRD1" 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.poPredicateSet>
<org.eventb.core.poSequent name="low_to_medium/grd2/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="6">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT3GRD0"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL" 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.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT3GRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="low_to_medium/act1/SIM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Action simulation" org.eventb.core.poStamp="6">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTALLHYPEVT3"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ MEDIUM})∨(waterLevel(m)=MEDIUM∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ LOW})∨(waterLevel(m)=MEDIUM∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ HIGH})∨(waterLevel(m)=LOW∧waterLevel{m ↦ MEDIUM}=waterLevel{m ↦ MEDIUM})" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|org.eventb.core.event#evt4|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|org.eventb.core.event#evt4"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|org.eventb.core.event#evt4|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC2" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt6"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poSequent#low_to_medium\/act1\/SIM|org.eventb.core.poPredicateSet#SEQHYP"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT3" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="6">
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.poIdentifier name="waterLevel'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPEVT3GRD0" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTIDENTEVT3" org.eventb.core.poStamp="6">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT3" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT3GRD0" org.eventb.core.poStamp="6">
<org.eventb.core.poPredicate name="PRD1" 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.poPredicateSet>
<org.eventb.core.poSequent name="medium_to_high/grd2/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="6">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT4GRD0"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="m∈dom(waterLevel)∧waterLevel∈MINE_SET ⇸ LEVEL" 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.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT4GRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="medium_to_high/act1/SIM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Action simulation" org.eventb.core.poStamp="6">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTALLHYPEVT4"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="(waterLevel(m)=HIGH∧waterLevel{m ↦ HIGH}=waterLevel{m ↦ MEDIUM})∨(waterLevel(m)=MEDIUM∧waterLevel{m ↦ HIGH}=waterLevel{m ↦ LOW})∨(waterLevel(m)=MEDIUM∧waterLevel{m ↦ HIGH}=waterLevel{m ↦ HIGH})∨(waterLevel(m)=LOW∧waterLevel{m ↦ HIGH}=waterLevel{m ↦ MEDIUM})" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|org.eventb.core.event#evt4|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|org.eventb.core.event#evt4"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor.bum|org.eventb.core.machineFile#WaterLevelSensor|org.eventb.core.event#evt4|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC2" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/Exemple_Mine_pump/WaterLevelSensor_refinement.bum|org.eventb.core.machineFile#WaterLevelSensor_refinement|org.eventb.core.event#evt7"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poSequent#medium_to_high\/act1\/SIM|org.eventb.core.poPredicateSet#SEQHYP"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT4" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="6">
<org.eventb.core.poIdentifier name="m" org.eventb.core.type="MINE_SET"/>
<org.eventb.core.poIdentifier name="waterLevel'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPEVT4GRD0" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTIDENTEVT4" org.eventb.core.poStamp="6">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT4" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT4GRD0" org.eventb.core.poStamp="6">
<org.eventb.core.poPredicate name="PRD1" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT5" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="6">
<org.eventb.core.poIdentifier name="MINE'" org.eventb.core.type="ℙ(MINE_SET)"/>
<org.eventb.core.poIdentifier name="waterLevel'" org.eventb.core.type="ℙ(MINE_SET×LEVEL)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT5" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#EVTIDENTEVT5" org.eventb.core.poStamp="6">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/Exemple_Mine_pump/WaterLevelSensor_refinement.bpo|org.eventb.core.poFile#WaterLevelSensor_refinement|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="6"/>
</org.eventb.core.poFile>
