<?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.event name="'" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION">
<org.eventb.core.action name="'" org.eventb.core.assignment="TRAIN ≔ ∅" org.eventb.core.label="act1"/>
<org.eventb.core.action name="(" org.eventb.core.assignment="onCBTC ≔ ∅" org.eventb.core.label="act2"/>
<org.eventb.core.action name=")" org.eventb.core.assignment="effectiveTrainMode ≔ ∅" org.eventb.core.label="act3"/>
<org.eventb.core.action name="*" org.eventb.core.assignment="emergencyBrake ≔ ∅" org.eventb.core.label="act4"/>
<org.eventb.core.action name="+" org.eventb.core.assignment="desiredTrainMode ≔ ∅" org.eventb.core.label="act5"/>
</org.eventb.core.event>
<org.eventb.core.seesContext name="(" org.eventb.core.target="TrainModelInitialContext"/>
<org.eventb.core.variable name=")" org.eventb.core.identifier="TRAIN"/>
<org.eventb.core.invariant name="*" org.eventb.core.label="inv1" org.eventb.core.predicate="TRAIN ∈ ℙ(TRAIN_SET)"/>
<org.eventb.core.variable name="+" org.eventb.core.identifier="onCBTC"/>
<org.eventb.core.invariant name="," org.eventb.core.label="inv2" org.eventb.core.predicate="onCBTC ∈ TRAIN → BOOL"/>
<org.eventb.core.variable name="-" org.eventb.core.identifier="effectiveTrainMode"/>
<org.eventb.core.invariant name="." org.eventb.core.label="inv3" org.eventb.core.predicate="effectiveTrainMode ∈ TRAIN → TRAIN_MODE"/>
<org.eventb.core.variable name="/" org.eventb.core.identifier="emergencyBrake"/>
<org.eventb.core.invariant name="0" org.eventb.core.label="inv4" org.eventb.core.predicate="emergencyBrake ∈ TRAIN → BOOL"/>
<org.eventb.core.variable name="1" org.eventb.core.identifier="desiredTrainMode"/>
<org.eventb.core.invariant name="2" org.eventb.core.label="inv5" org.eventb.core.predicate="desiredTrainMode ∈ TRAIN → TRAIN_MODE"/>
<org.eventb.core.event name="3" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="updateOnCBTC">
<org.eventb.core.parameter name="'" org.eventb.core.identifier="t"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="v"/>
<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="v ∈ BOOL"/>
<org.eventb.core.action name="+" org.eventb.core.assignment="onCBTC(t) ≔ v" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="4" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="updateEffectiveTrainMode">
<org.eventb.core.parameter name="'" org.eventb.core.identifier="t"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="mode"/>
<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="mode ∈ TRAIN_MODE"/>
<org.eventb.core.action name="+" org.eventb.core.assignment="effectiveTrainMode(t) ≔ mode" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="5" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="updateEmergencyBrake">
<org.eventb.core.parameter name="'" org.eventb.core.identifier="t"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="v"/>
<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="v ∈ BOOL"/>
<org.eventb.core.action name="+" org.eventb.core.assignment="emergencyBrake(t) ≔ v" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.event name="6" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="updateDesiredTrainMode">
<org.eventb.core.parameter name="'" org.eventb.core.identifier="t"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="mode"/>
<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="mode ∈ TRAIN_MODE"/>
<org.eventb.core.action name="+" org.eventb.core.assignment="desiredTrainMode(t) ≔ mode" org.eventb.core.label="act1"/>
</org.eventb.core.event>
</org.eventb.core.machineFile>
