<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scMachineFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd">
<org.eventb.core.scSeesContext name="SEES0" org.eventb.core.scTarget="/Train_Mode_Example/TrainModelInitialContext.bcc" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.seesContext#("/>
<org.eventb.core.scInternalContext name="TrainModelInitialContext">
<org.eventb.core.scAxiom name="AXM0" org.eventb.core.label="axm1" 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.theorem="false"/>
<org.eventb.core.scConstant name="ATP" org.eventb.core.source="/Train_Mode_Example/TrainModelInitialContext.buc|org.eventb.core.contextFile#TrainModelInitialContext|org.eventb.core.constant#(" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.scConstant name="ATPR" org.eventb.core.source="/Train_Mode_Example/TrainModelInitialContext.buc|org.eventb.core.contextFile#TrainModelInitialContext|org.eventb.core.constant#)" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.scConstant name="BYPASS" org.eventb.core.source="/Train_Mode_Example/TrainModelInitialContext.buc|org.eventb.core.contextFile#TrainModelInitialContext|org.eventb.core.constant#*" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.scCarrierSet name="TRAIN_MODE" org.eventb.core.source="/Train_Mode_Example/TrainModelInitialContext.buc|org.eventb.core.contextFile#TrainModelInitialContext|org.eventb.core.carrierSet#'" org.eventb.core.type="ℙ(TRAIN_MODE)"/>
<org.eventb.core.scCarrierSet name="TRAIN_SET" org.eventb.core.source="/Train_Mode_Example/TrainModelInitialContext.buc|org.eventb.core.contextFile#TrainModelInitialContext|org.eventb.core.carrierSet#," org.eventb.core.type="ℙ(TRAIN_SET)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInvariant name="INV0" org.eventb.core.label="inv1" 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.theorem="false"/>
<org.eventb.core.scInvariant name="INV1" org.eventb.core.label="inv2" 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.theorem="false"/>
<org.eventb.core.scInvariant name="INV2" org.eventb.core.label="inv3" 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.theorem="false"/>
<org.eventb.core.scInvariant name="INV3" org.eventb.core.label="inv4" 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.theorem="false"/>
<org.eventb.core.scInvariant name="INV4" org.eventb.core.label="inv5" 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.theorem="false"/>
<org.eventb.core.scVariable name="TRAIN" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.variable#set1" org.eventb.core.type="ℙ(TRAIN_SET)"/>
<org.eventb.core.scVariable name="desiredTrainMode" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.variable#set5" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<org.eventb.core.scVariable name="effectiveTrainMode" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.variable#set3" org.eventb.core.type="ℙ(TRAIN_SET×TRAIN_MODE)"/>
<org.eventb.core.scVariable name="emergencyBrake" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.variable#set4" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.scVariable name="onCBTC" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.variable#set2" org.eventb.core.type="ℙ(TRAIN_SET×BOOL)"/>
<org.eventb.core.scEvent name="EVT0" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt1">
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="TRAIN ≔ (∅ ⦂ ℙ(TRAIN_SET))" org.eventb.core.label="act1" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt1|org.eventb.core.action#'"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="onCBTC ≔ (∅ ⦂ ℙ(TRAIN_SET×BOOL))" org.eventb.core.label="act2" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt1|org.eventb.core.action#("/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="effectiveTrainMode ≔ (∅ ⦂ ℙ(TRAIN_SET×TRAIN_MODE))" org.eventb.core.label="act3" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt1|org.eventb.core.action#)"/>
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="emergencyBrake ≔ (∅ ⦂ ℙ(TRAIN_SET×BOOL))" org.eventb.core.label="act4" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt1|org.eventb.core.action#*"/>
<org.eventb.core.scAction name="ACT4" org.eventb.core.assignment="desiredTrainMode ≔ (∅ ⦂ ℙ(TRAIN_SET×TRAIN_MODE))" org.eventb.core.label="act5" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt1|org.eventb.core.action#+"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT1" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="updateOnCBTC" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt2">
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" 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.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" 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.theorem="false"/>
<org.eventb.core.scParameter name="t" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt2|org.eventb.core.parameter#'" org.eventb.core.type="TRAIN_SET"/>
<org.eventb.core.scParameter name="v" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt2|org.eventb.core.parameter#(" org.eventb.core.type="BOOL"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="onCBTC ≔ onCBTC{t ↦ v}" org.eventb.core.label="act1" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt2|org.eventb.core.action#+"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT2" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="updateDesiredTrainMode" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt5">
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" 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.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" 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.theorem="false"/>
<org.eventb.core.scParameter name="mode" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt5|org.eventb.core.parameter#(" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.scParameter name="t" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt5|org.eventb.core.parameter#'" org.eventb.core.type="TRAIN_SET"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="desiredTrainMode ≔ desiredTrainMode{t ↦ mode}" org.eventb.core.label="act1" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt5|org.eventb.core.action#element1"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT3" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="updateEffectiveTrainMode" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt3">
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="t∈TRAIN" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt3|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" 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#evt3|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="mode" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt3|org.eventb.core.parameter#(" org.eventb.core.type="TRAIN_MODE"/>
<org.eventb.core.scParameter name="t" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt3|org.eventb.core.parameter#'" org.eventb.core.type="TRAIN_SET"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="effectiveTrainMode ≔ effectiveTrainMode{t ↦ mode}" org.eventb.core.label="act1" 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.scEvent>
<org.eventb.core.scEvent name="EVT4" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="updateEmergencyBrake" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt4">
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="t∈TRAIN" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt4|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="v∈BOOL" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt4|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="t" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt4|org.eventb.core.parameter#'" org.eventb.core.type="TRAIN_SET"/>
<org.eventb.core.scParameter name="v" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt4|org.eventb.core.parameter#(" org.eventb.core.type="BOOL"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="emergencyBrake ≔ emergencyBrake{t ↦ v}" org.eventb.core.label="act1" org.eventb.core.source="/Train_Mode_Example/ModeSelector.bum|org.eventb.core.machineFile#ModeSelector|org.eventb.core.event#evt4|org.eventb.core.action#+"/>
</org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>
