<?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="CBTCSensor"/>
<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.event name="evt1" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION">
<org.eventb.core.action name="'" org.eventb.core.assignment="CurrentPosition ≔ ∅" org.eventb.core.label="act3"/>
</org.eventb.core.event>
<org.eventb.core.event name="evt2" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="SetCBTC">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="updateOnCBTC"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="t ∈ TRAIN"/>
<org.eventb.core.action name="+" org.eventb.core.assignment="onCBTC(t) ≔ TRUE" org.eventb.core.label="act1"/>
<org.eventb.core.parameter name=")" org.eventb.core.identifier="t"/>
<org.eventb.core.guard name="(" org.eventb.core.label="grd3" org.eventb.core.predicate="CBTC_EQUIPED(CurrentPosition(t)) = TRUE"/>
<org.eventb.core.witness name="," org.eventb.core.label="v" org.eventb.core.predicate="v = TRUE"/>
</org.eventb.core.event>
<org.eventb.core.variable name="set3" org.eventb.core.identifier="CurrentPosition"/>
<org.eventb.core.invariant name="set4" org.eventb.core.label="inv1" org.eventb.core.predicate="CurrentPosition ∈ TRAIN → POSITION"/>
<org.eventb.core.event name="set5" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="UnsetCBTC">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="updateOnCBTC"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="t"/>
<org.eventb.core.guard name="element1" org.eventb.core.label="grd1" org.eventb.core.predicate="t ∈ TRAIN"/>
<org.eventb.core.witness name="element2" org.eventb.core.label="v" org.eventb.core.predicate="v = FALSE"/>
<org.eventb.core.guard name="element3" org.eventb.core.label="grd2" org.eventb.core.predicate="CBTC_EQUIPED(CurrentPosition(t)) = FALSE"/>
<org.eventb.core.action name="element4" org.eventb.core.assignment="onCBTC(t) ≔ FALSE" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.seesContext name="set6" org.eventb.core.target="CBTCSensorsNetwork"/>
</org.eventb.core.machineFile>
