<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" version="5">
<org.eventb.core.refinesMachine name="'" org.eventb.core.target="ModeSelector"/>
<org.eventb.core.seesContext name="(" org.eventb.core.target="TrainModelInitialContext"/>
<org.eventb.core.variable ch.ethz.eventb.decomposition.nature="1" name="set1" org.eventb.core.identifier="TRAIN"/>
<org.eventb.core.variable ch.ethz.eventb.decomposition.nature="1" name="set2" org.eventb.core.identifier="onCBTC"/>
<org.eventb.core.variable ch.ethz.eventb.decomposition.nature="1" name="set3" org.eventb.core.identifier="effectiveTrainMode"/>
<org.eventb.core.variable ch.ethz.eventb.decomposition.nature="1" name="set4" org.eventb.core.identifier="emergencyBrake"/>
<org.eventb.core.variable ch.ethz.eventb.decomposition.nature="1" name="set5" org.eventb.core.identifier="desiredTrainMode"/>
<org.eventb.core.event name="evt1" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION"/>
<org.eventb.core.event ch.ethz.eventb.decomposition.external="true" name="evt2" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="updateOnCBTC">
<org.eventb.core.refinesEvent name="," org.eventb.core.target="updateOnCBTC"/>
</org.eventb.core.event>
<org.eventb.core.event ch.ethz.eventb.decomposition.external="true" name="evt3" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="updateDesiredTrainMode">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="updateDesiredTrainMode"/>
</org.eventb.core.event>
<org.eventb.core.event name="set6" org.eventb.core.comment="Achieve[Bypass Mode Selected WHEN &#13;&#10;   Driver Desire Bypass Mode]&#13;&#10;AND&#13;&#10;Achieve[Emergency Brakes On WHEN &#13;&#10;   Bypass Mode Selected]" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="BypassModeSelected">
<org.eventb.core.refinesEvent name="(" org.eventb.core.target="updateEmergencyBrake"/>
<org.eventb.core.parameter name=")" org.eventb.core.identifier="t"/>
<org.eventb.core.guard name="*" org.eventb.core.label="grd1" org.eventb.core.predicate="t ∈ TRAIN"/>
<org.eventb.core.witness name="-" org.eventb.core.label="v" org.eventb.core.predicate="v = TRUE"/>
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="updateEffectiveTrainMode"/>
<org.eventb.core.guard name="." org.eventb.core.label="grd2" org.eventb.core.predicate="desiredTrainMode(t) = BYPASS"/>
<org.eventb.core.action name="/" org.eventb.core.assignment="effectiveTrainMode(t) ≔ BYPASS" org.eventb.core.label="act1"/>
<org.eventb.core.action name="0" org.eventb.core.assignment="emergencyBrake(t) ≔ TRUE" org.eventb.core.label="act2"/>
<org.eventb.core.witness name="1" org.eventb.core.label="mode" org.eventb.core.predicate="mode = BYPASS"/>
</org.eventb.core.event>
<org.eventb.core.event name="set7" org.eventb.core.comment="Achieve[ATPR Mode Selected WHEN &#13;&#10;   Driver Desires ATPR]" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="ATPRModeSelected">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="updateEffectiveTrainMode"/>
<org.eventb.core.witness name="(" org.eventb.core.label="mode" org.eventb.core.predicate="mode = ATPR"/>
<org.eventb.core.parameter name=")" org.eventb.core.identifier="t"/>
<org.eventb.core.guard name="*" org.eventb.core.label="grd1" org.eventb.core.predicate="t ∈ TRAIN"/>
<org.eventb.core.guard name="+" org.eventb.core.label="grd2" org.eventb.core.predicate="desiredTrainMode(t) = ATPR"/>
<org.eventb.core.action name="," org.eventb.core.assignment="effectiveTrainMode(t) ≔ ATPR" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="set8" org.eventb.core.comment="Achieve[ATP Mode Selected When &#13;&#10;   Driver Desires ATP &#13;&#10;   EXCEPT If Currently On Non CBTC Track]" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="ATPModeSelectedOnCBTCTrack">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="updateEffectiveTrainMode"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="t"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="t ∈ TRAIN"/>
<org.eventb.core.witness name="*" org.eventb.core.label="mode" org.eventb.core.predicate="mode = ATP"/>
<org.eventb.core.action name="+" org.eventb.core.assignment="effectiveTrainMode(t) ≔ ATP" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="," org.eventb.core.label="grd2" org.eventb.core.predicate="onCBTC(t) = TRUE"/>
<org.eventb.core.guard name="-" org.eventb.core.label="grd3" org.eventb.core.predicate="desiredTrainMode(t) = ATP"/>
</org.eventb.core.event>
<org.eventb.core.event name="set9" org.eventb.core.comment="Achieve[Emergency Brakes On WHEN &#13;&#10;   ATP selected By Driver On Non CBTC Track]&#13;&#10;AND&#13;&#10;Achieve[ATPR Mode Selected WHEN &#13;&#10;   Driver Desires ATP on non CBTC]" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="ATPModeSelectedOnNonCBTCTrack">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="updateEmergencyBrake"/>
<org.eventb.core.refinesEvent name="(" org.eventb.core.target="updateEffectiveTrainMode"/>
<org.eventb.core.parameter name=")" org.eventb.core.identifier="t"/>
<org.eventb.core.guard name="*" org.eventb.core.label="grd1" org.eventb.core.predicate="t ∈ TRAIN"/>
<org.eventb.core.guard name="+" org.eventb.core.label="grd2" org.eventb.core.predicate="onCBTC(t) = FALSE"/>
<org.eventb.core.guard name="," org.eventb.core.label="grd3" org.eventb.core.predicate="desiredTrainMode(t) = ATP"/>
<org.eventb.core.witness name="-" org.eventb.core.label="v" org.eventb.core.predicate="v = TRUE"/>
<org.eventb.core.witness name="." org.eventb.core.label="mode" org.eventb.core.predicate="mode = ATPR"/>
<org.eventb.core.action name="/" org.eventb.core.assignment="effectiveTrainMode(t) ≔ ATPR" org.eventb.core.label="act1"/>
<org.eventb.core.action name="0" org.eventb.core.assignment="emergencyBrake(t) ≔ TRUE" org.eventb.core.label="act2"/>
</org.eventb.core.event>
</org.eventb.core.machineFile>
