<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="24">
<org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="20">
<org.eventb.core.poIdentifier name="TRAIN_MODE" org.eventb.core.type="ℙ(TRAIN_MODE)"/>
<org.eventb.core.poIdentifier name="TRAIN_SET" org.eventb.core.type="ℙ(TRAIN_SET)"/>
<org.eventb.core.poIdentifier name="ATP" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.poIdentifier name="ATPR" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.poIdentifier name="BYPASS" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="partition(TRAIN_MODE,{ATP},{ATPR},{BYPASS})" org.eventb.core.source="/Train_Mode_Example/TrainModelInitialContext.buc|org.eventb.core.contextFile#TrainModelInitialContext|org.eventb.core.axiom#+"/>
<org.eventb.core.poIdentifier name="POSITION" org.eventb.core.type="ℙ(POSITION)"/>
<org.eventb.core.poIdentifier name="CBTC_EQUIPED" org.eventb.core.type="ℙ(POSITION×BOOL)"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="CBTC_EQUIPED∈POSITION → BOOL" org.eventb.core.source="/Train_Mode_Example/CBTCSensorsNetwork.buc|org.eventb.core.contextFile#CBTCSensorsNetwork|org.eventb.core.axiom#)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="20">
<org.eventb.core.poIdentifier name="CurrentPosition" org.eventb.core.type="ℙ(TRAIN_SET×POSITION)"/>
<org.eventb.core.poIdentifier name="TRAIN" org.eventb.core.type="ℙ(TRAIN_SET)"/>
<org.eventb.core.poIdentifier name="onCBTC" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="TRAIN∈ℙ(TRAIN_SET)" org.eventb.core.source="/Train_Mode_Example/CBTCSensor.bum|org.eventb.core.machineFile#CBTCSensor|org.eventb.core.invariant#inv1"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="onCBTC∈TRAIN → BOOL" org.eventb.core.source="/Train_Mode_Example/CBTCSensor.bum|org.eventb.core.machineFile#CBTCSensor|org.eventb.core.invariant#inv2"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="INITIALISATION/inv1/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="21">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#EVTALLHYPEVT0"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="(∅ ⦂ ℙ(TRAIN_SET×POSITION))∈(∅ ⦂ ℙ(TRAIN_SET)) → POSITION" org.eventb.core.source="/Train_Mode_Example/CBTCSensor_refinement.bum|org.eventb.core.machineFile#CBTCSensor_refinement|org.eventb.core.invariant#set4"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/Train_Mode_Example/CBTCSensor.bum|org.eventb.core.machineFile#CBTCSensor|org.eventb.core.event#evt1"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/Train_Mode_Example/CBTCSensor_refinement.bum|org.eventb.core.machineFile#CBTCSensor_refinement|org.eventb.core.event#evt1"/>
<org.eventb.core.poSource name="SRC2" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Train_Mode_Example/CBTCSensor_refinement.bum|org.eventb.core.machineFile#CBTCSensor_refinement|org.eventb.core.invariant#set4"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poSequent#INITIALISATION\/inv1\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="HINT1" org.eventb.core.poSelHintFst="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT0" org.eventb.core.parentSet="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="20">
<org.eventb.core.poIdentifier name="onCBTC'" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.poIdentifier name="TRAIN'" org.eventb.core.type="ℙ(TRAIN_SET)"/>
<org.eventb.core.poIdentifier name="CurrentPosition'" org.eventb.core.type="ℙ(TRAIN_SET×POSITION)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT0" org.eventb.core.parentSet="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#EVTIDENTEVT0" org.eventb.core.poStamp="20"/>
<org.eventb.core.poSequent name="SetCBTC/grd3/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="23">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT1GRD0"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="t∈dom(CurrentPosition)∧CurrentPosition∈TRAIN_SET ⇸ POSITION∧CurrentPosition(t)∈dom(CBTC_EQUIPED)∧CBTC_EQUIPED∈POSITION ⇸ BOOL" org.eventb.core.source="/Train_Mode_Example/CBTCSensor_refinement.bum|org.eventb.core.machineFile#CBTCSensor_refinement|org.eventb.core.event#evt2|org.eventb.core.guard#("/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Train_Mode_Example/CBTCSensor_refinement.bum|org.eventb.core.machineFile#CBTCSensor_refinement|org.eventb.core.event#evt2|org.eventb.core.guard#("/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT1GRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="SetCBTC/act1/SIM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Action simulation" org.eventb.core.poStamp="23">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#EVTALLHYPEVT1"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="onCBTC{t ↦ TRUE}=onCBTC{t ↦ TRUE}" org.eventb.core.source="/Train_Mode_Example/CBTCSensor.bum|org.eventb.core.machineFile#CBTCSensor|org.eventb.core.event#evt2|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/Train_Mode_Example/CBTCSensor.bum|org.eventb.core.machineFile#CBTCSensor|org.eventb.core.event#evt2"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/Train_Mode_Example/CBTCSensor.bum|org.eventb.core.machineFile#CBTCSensor|org.eventb.core.event#evt2|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC2" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/Train_Mode_Example/CBTCSensor_refinement.bum|org.eventb.core.machineFile#CBTCSensor_refinement|org.eventb.core.event#evt2"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poSequent#SetCBTC\/act1\/SIM|org.eventb.core.poPredicateSet#SEQHYP"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT1" org.eventb.core.parentSet="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="20">
<org.eventb.core.poIdentifier name="onCBTC'" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.poIdentifier name="t" org.eventb.core.type="TRAIN_SET"/>
<org.eventb.core.poIdentifier name="v" org.eventb.core.type="BOOL"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPEVT1GRD0" org.eventb.core.parentSet="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#EVTIDENTEVT1" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="t∈TRAIN" org.eventb.core.source="/Train_Mode_Example/CBTCSensor_refinement.bum|org.eventb.core.machineFile#CBTCSensor_refinement|org.eventb.core.event#evt2|org.eventb.core.guard#)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT1" org.eventb.core.parentSet="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT1GRD0" org.eventb.core.poStamp="23">
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="CBTC_EQUIPED(CurrentPosition(t))=TRUE" org.eventb.core.source="/Train_Mode_Example/CBTCSensor_refinement.bum|org.eventb.core.machineFile#CBTCSensor_refinement|org.eventb.core.event#evt2|org.eventb.core.guard#("/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="UnsetCBTC/grd2/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="24">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT2GRD0"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="t∈dom(CurrentPosition)∧CurrentPosition∈TRAIN_SET ⇸ POSITION∧CurrentPosition(t)∈dom(CBTC_EQUIPED)∧CBTC_EQUIPED∈POSITION ⇸ BOOL" org.eventb.core.source="/Train_Mode_Example/CBTCSensor_refinement.bum|org.eventb.core.machineFile#CBTCSensor_refinement|org.eventb.core.event#set5|org.eventb.core.guard#element3"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Train_Mode_Example/CBTCSensor_refinement.bum|org.eventb.core.machineFile#CBTCSensor_refinement|org.eventb.core.event#set5|org.eventb.core.guard#element3"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT2GRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="UnsetCBTC/act1/SIM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Action simulation" org.eventb.core.poStamp="24">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#EVTALLHYPEVT2"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="onCBTC{t ↦ FALSE}=onCBTC{t ↦ FALSE}" org.eventb.core.source="/Train_Mode_Example/CBTCSensor.bum|org.eventb.core.machineFile#CBTCSensor|org.eventb.core.event#evt2|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/Train_Mode_Example/CBTCSensor.bum|org.eventb.core.machineFile#CBTCSensor|org.eventb.core.event#evt2"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/Train_Mode_Example/CBTCSensor.bum|org.eventb.core.machineFile#CBTCSensor|org.eventb.core.event#evt2|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC2" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/Train_Mode_Example/CBTCSensor_refinement.bum|org.eventb.core.machineFile#CBTCSensor_refinement|org.eventb.core.event#set5"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poSequent#UnsetCBTC\/act1\/SIM|org.eventb.core.poPredicateSet#SEQHYP"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT2" org.eventb.core.parentSet="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="20">
<org.eventb.core.poIdentifier name="onCBTC'" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.poIdentifier name="t" org.eventb.core.type="TRAIN_SET"/>
<org.eventb.core.poIdentifier name="v" org.eventb.core.type="BOOL"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPEVT2GRD0" org.eventb.core.parentSet="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#EVTIDENTEVT2" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="t∈TRAIN" org.eventb.core.source="/Train_Mode_Example/CBTCSensor_refinement.bum|org.eventb.core.machineFile#CBTCSensor_refinement|org.eventb.core.event#set5|org.eventb.core.guard#element1"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT2" org.eventb.core.parentSet="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT2GRD0" org.eventb.core.poStamp="24">
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="CBTC_EQUIPED(CurrentPosition(t))=FALSE" org.eventb.core.source="/Train_Mode_Example/CBTCSensor_refinement.bum|org.eventb.core.machineFile#CBTCSensor_refinement|org.eventb.core.event#set5|org.eventb.core.guard#element3"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/Train_Mode_Example/CBTCSensor_refinement.bpo|org.eventb.core.poFile#CBTCSensor_refinement|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="20">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="CurrentPosition∈TRAIN → POSITION" org.eventb.core.source="/Train_Mode_Example/CBTCSensor_refinement.bum|org.eventb.core.machineFile#CBTCSensor_refinement|org.eventb.core.invariant#set4"/>
</org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>
