<?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.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="desiredTrainMode"/>
<org.eventb.core.invariant name="inv1" org.eventb.core.label="inv1" org.eventb.core.predicate="TRAIN ∈ ℙ(TRAIN_SET)"/>
<org.eventb.core.invariant name="inv2" org.eventb.core.label="inv5" org.eventb.core.predicate="desiredTrainMode ∈ TRAIN → TRAIN_MODE"/>
<org.eventb.core.event name="evt1" 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="desiredTrainMode ≔ ∅" org.eventb.core.label="act2"/>
</org.eventb.core.event>
<org.eventb.core.event name="evt2" 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="element1" org.eventb.core.assignment="desiredTrainMode(t) ≔ mode" org.eventb.core.label="act1"/>
</org.eventb.core.event>
</org.eventb.core.machineFile>
