<?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="1">
<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/Driver.bpo|org.eventb.core.poFile#Driver|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="2">
<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.poPredicateSet>
<org.eventb.core.poSequent name="INITIALISATION/inv5/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="2">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Train_Mode_Example/Driver.bpo|org.eventb.core.poFile#Driver|org.eventb.core.poPredicateSet#EVTALLHYPEVT0"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="(∅ ⦂ ℙ(TRAIN_SET×TRAIN_MODE))∈(∅ ⦂ ℙ(TRAIN_SET)) → TRAIN_MODE" org.eventb.core.source="/Train_Mode_Example/Driver.bum|org.eventb.core.machineFile#Driver|org.eventb.core.invariant#inv2"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Train_Mode_Example/Driver.bum|org.eventb.core.machineFile#Driver|org.eventb.core.event#evt1"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Train_Mode_Example/Driver.bum|org.eventb.core.machineFile#Driver|org.eventb.core.invariant#inv2"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Train_Mode_Example/Driver.bpo|org.eventb.core.poFile#Driver|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/Train_Mode_Example/Driver.bpo|org.eventb.core.poFile#Driver|org.eventb.core.poSequent#INITIALISATION\/inv5\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="HINT1" org.eventb.core.poSelHintFst="/Train_Mode_Example/Driver.bpo|org.eventb.core.poFile#Driver|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT0" org.eventb.core.parentSet="/Train_Mode_Example/Driver.bpo|org.eventb.core.poFile#Driver|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="desiredTrainMode'" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<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/Driver.bpo|org.eventb.core.poFile#Driver|org.eventb.core.poPredicateSet#EVTIDENTEVT0" org.eventb.core.poStamp="2"/>
<org.eventb.core.poSequent name="updateDesiredTrainMode/inv5/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="6">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/Train_Mode_Example/Driver.bpo|org.eventb.core.poFile#Driver|org.eventb.core.poPredicateSet#EVTALLHYPEVT1"/>
<org.eventb.core.poPredicate name="GOAL" org.eventb.core.predicate="desiredTrainMode{t ↦ mode}∈TRAIN → TRAIN_MODE" org.eventb.core.source="/Train_Mode_Example/Driver.bum|org.eventb.core.machineFile#Driver|org.eventb.core.invariant#inv2"/>
<org.eventb.core.poSource name="SRC0" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Train_Mode_Example/Driver.bum|org.eventb.core.machineFile#Driver|org.eventb.core.event#evt2"/>
<org.eventb.core.poSource name="SRC1" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/Train_Mode_Example/Driver.bum|org.eventb.core.machineFile#Driver|org.eventb.core.invariant#inv2"/>
<org.eventb.core.poSelHint name="HINT0" org.eventb.core.poSelHintFst="/Train_Mode_Example/Driver.bpo|org.eventb.core.poFile#Driver|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/Train_Mode_Example/Driver.bpo|org.eventb.core.poFile#Driver|org.eventb.core.poSequent#updateDesiredTrainMode\/inv5\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="HINT1" org.eventb.core.poSelHintFst="/Train_Mode_Example/Driver.bpo|org.eventb.core.poFile#Driver|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTEVT1" org.eventb.core.parentSet="/Train_Mode_Example/Driver.bpo|org.eventb.core.poFile#Driver|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="6">
<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="EVTALLHYPEVT1" org.eventb.core.parentSet="/Train_Mode_Example/Driver.bpo|org.eventb.core.poFile#Driver|org.eventb.core.poPredicateSet#EVTIDENTEVT1" org.eventb.core.poStamp="6">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="t∈TRAIN" org.eventb.core.source="/Train_Mode_Example/Driver.bum|org.eventb.core.machineFile#Driver|org.eventb.core.event#evt2|org.eventb.core.guard#)"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="mode∈TRAIN_MODE" org.eventb.core.source="/Train_Mode_Example/Driver.bum|org.eventb.core.machineFile#Driver|org.eventb.core.event#evt2|org.eventb.core.guard#*"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/Train_Mode_Example/Driver.bpo|org.eventb.core.poFile#Driver|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="2">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="TRAIN∈ℙ(TRAIN_SET)" org.eventb.core.source="/Train_Mode_Example/Driver.bum|org.eventb.core.machineFile#Driver|org.eventb.core.invariant#inv1"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="desiredTrainMode∈TRAIN → TRAIN_MODE" org.eventb.core.source="/Train_Mode_Example/Driver.bum|org.eventb.core.machineFile#Driver|org.eventb.core.invariant#inv2"/>
</org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>
