<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="16">
<org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="0">
<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.poPredicateSet>
<org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="TRAIN" org.eventb.core.type="ℙ(TRAIN_SET)"/>
<org.eventb.core.poIdentifier name="desiredTrainMode" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<org.eventb.core.poIdentifier name="effectiveTrainMode" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<org.eventb.core.poIdentifier name="emergencyBrake" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.poIdentifier name="onCBTC" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="TRAIN∈ℙ(TRAIN_SET)" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.invariant#inv1"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="onCBTC∈TRAIN → BOOL" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.invariant#inv2"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="effectiveTrainMode∈TRAIN → TRAIN_MODE" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.invariant#inv3"/>
<org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="emergencyBrake∈TRAIN → BOOL" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.invariant#inv4"/>
<org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="desiredTrainMode∈TRAIN → TRAIN_MODE" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.invariant#inv5"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT0" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="onCBTC'" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.poIdentifier name="effectiveTrainMode'" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<org.eventb.core.poIdentifier name="desiredTrainMode'" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<org.eventb.core.poIdentifier name="emergencyBrake'" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.poIdentifier name="TRAIN'" org.eventb.core.type="ℙ(TRAIN_SET)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT0" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#EVTIDENTEVT0" org.eventb.core.poStamp="0"/>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT1" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="8">
<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="EVTALLHYPEVT1" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#EVTIDENTEVT1" org.eventb.core.poStamp="8">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="t∈TRAIN" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt2|org.eventb.core.guard#)"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="v∈BOOL" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt2|org.eventb.core.guard#*"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT2" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="9">
<org.eventb.core.poIdentifier name="t" org.eventb.core.type="TRAIN_SET"/>
<org.eventb.core.poIdentifier name="desiredTrainMode'" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<org.eventb.core.poIdentifier name="mode" org.eventb.core.type="TRAIN_MODE"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT2" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#EVTIDENTEVT2" org.eventb.core.poStamp="9">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="t∈TRAIN" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt5|org.eventb.core.guard#)"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="mode∈TRAIN_MODE" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt5|org.eventb.core.guard#*"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="ATPRModeSelected/grd2/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="9">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT3GRD0"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="t∈dom(desiredTrainMode)∧desiredTrainMode∈TRAIN_SET ⇸ TRAIN_MODE" org.eventb.core.source="/Train_Mode_Example/ModeSelector_refinement.bum|org.eventb.core.machineFile#ModeSelector_refinement|org.eventb.core.event#set7|org.eventb.core.guard#+"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Train_Mode_Example/ModeSelector_refinement.bum|org.eventb.core.machineFile#ModeSelector_refinement|org.eventb.core.event#set7|org.eventb.core.guard#+"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT3GRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="ATPRModeSelected/act1/SIM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Action simulation" org.eventb.core.poStamp="9">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#EVTALLHYPEVT3"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="effectiveTrainMode{t ↦ ATPR}=effectiveTrainMode{t ↦ ATPR}" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt3|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt3"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt3|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC2" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/Train_Mode_Example/ModeSelector_refinement.bum|org.eventb.core.machineFile#ModeSelector_refinement|org.eventb.core.event#set7"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poSequent#ATPRModeSelected\/act1\/SIM|org.eventb.core.poPredicateSet#SEQHYP"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT3" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="t" org.eventb.core.type="TRAIN_SET"/>
<org.eventb.core.poIdentifier name="effectiveTrainMode'" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<org.eventb.core.poIdentifier name="mode" org.eventb.core.type="TRAIN_MODE"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPEVT3GRD0" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#EVTIDENTEVT3" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="t∈TRAIN" org.eventb.core.source="/Train_Mode_Example/ModeSelector_refinement.bum|org.eventb.core.machineFile#ModeSelector_refinement|org.eventb.core.event#set7|org.eventb.core.guard#*"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT3" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT3GRD0" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="desiredTrainMode(t)=ATPR" org.eventb.core.source="/Train_Mode_Example/ModeSelector_refinement.bum|org.eventb.core.machineFile#ModeSelector_refinement|org.eventb.core.event#set7|org.eventb.core.guard#+"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="ATPModeSelectedOnCBTCTrack/grd2/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="14">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT4GRD0"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="t∈dom(onCBTC)∧onCBTC∈TRAIN_SET ⇸ BOOL" org.eventb.core.source="/Train_Mode_Example/ModeSelector_refinement.bum|org.eventb.core.machineFile#ModeSelector_refinement|org.eventb.core.event#set8|org.eventb.core.guard#,"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Train_Mode_Example/ModeSelector_refinement.bum|org.eventb.core.machineFile#ModeSelector_refinement|org.eventb.core.event#set8|org.eventb.core.guard#,"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT4GRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="ATPModeSelectedOnCBTCTrack/grd3/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="14">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT4GRD1"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="t∈dom(desiredTrainMode)∧desiredTrainMode∈TRAIN_SET ⇸ TRAIN_MODE" org.eventb.core.source="/Train_Mode_Example/ModeSelector_refinement.bum|org.eventb.core.machineFile#ModeSelector_refinement|org.eventb.core.event#set8|org.eventb.core.guard#-"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Train_Mode_Example/ModeSelector_refinement.bum|org.eventb.core.machineFile#ModeSelector_refinement|org.eventb.core.event#set8|org.eventb.core.guard#-"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT4GRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="ATPModeSelectedOnCBTCTrack/act1/SIM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Action simulation" org.eventb.core.poStamp="14">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#EVTALLHYPEVT4"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="effectiveTrainMode{t ↦ ATP}=effectiveTrainMode{t ↦ ATP}" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt3|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt3"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt3|org.eventb.core.action#+"/>
<org.eventb.core.poSource name="SRC2" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/Train_Mode_Example/ModeSelector_refinement.bum|org.eventb.core.machineFile#ModeSelector_refinement|org.eventb.core.event#set8"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poSequent#ATPModeSelectedOnCBTCTrack\/act1\/SIM|org.eventb.core.poPredicateSet#SEQHYP"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT4" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="t" org.eventb.core.type="TRAIN_SET"/>
<org.eventb.core.poIdentifier name="effectiveTrainMode'" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<org.eventb.core.poIdentifier name="mode" org.eventb.core.type="TRAIN_MODE"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPEVT4GRD0" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#EVTIDENTEVT4" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="t∈TRAIN" org.eventb.core.source="/Train_Mode_Example/ModeSelector_refinement.bum|org.eventb.core.machineFile#ModeSelector_refinement|org.eventb.core.event#set8|org.eventb.core.guard#)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPEVT4GRD1" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT4GRD0" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="onCBTC(t)=TRUE" org.eventb.core.source="/Train_Mode_Example/ModeSelector_refinement.bum|org.eventb.core.machineFile#ModeSelector_refinement|org.eventb.core.event#set8|org.eventb.core.guard#,"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPEVT4" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#EVTHYPEVT4GRD1" org.eventb.core.poStamp="13">
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="desiredTrainMode(t)=ATP" org.eventb.core.source="/Train_Mode_Example/ModeSelector_refinement.bum|org.eventb.core.machineFile#ModeSelector_refinement|org.eventb.core.event#set8|org.eventb.core.guard#-"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/Train_Mode_Example/ModeSelector_refinement.bpo|org.eventb.core.poFile#ModeSelector_refinement|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="0"/>
</org.eventb.core.poFile>
