m1_shafts.bum

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.core.generated="false" org.eventb.texttools.text_lastmodified="1590749135266" org.eventb.texttools.text_representation="machine m1_shafts refines m0_cabins sees m1_shafts_context&#10;&#10;variables floor shaft&#10;&#10;invariants&#10;  @shaft_type shaft ∈ CABINS → SHAFTS&#10;&#10;events&#10;  event INITIALISATION extends INITIALISATION&#10;    then&#10;      @shafts_init shaft ≔ CABINS × {UP}&#10;  end&#10;&#10;  event CabinMovesDown extends CabinMovesDown&#10;    where&#10;      @lower_floor_free ∀c·c ∈ dom(floor) ∧ shaft(c) = DOWN ⇒ (floor(cabin) − 1) ≠ floor(c) //SAF 8&#10;      @shaft_down shaft(cabin) = DOWN&#10;  end&#10;&#10;  event CabinMovesUp extends CabinMovesUp&#10;    where&#10;      @upper_floor_free ∀c·c ∈ dom(floor) ∧ shaft(c) = UP ⇒ (floor(cabin) + 1) ≠ floor(c) //SAF 8&#10;      @shaft_up shaft(cabin) = UP&#10;  end&#10;&#10;  event CabinUpToDown&#10;    any cabin&#10;    where&#10;      @at_top_floor floor(cabin) = TOP_FLOOR //REQ 4&#10;      @in_up_shaft shaft(cabin) = UP&#10;      @top_right_free ∀c·c ∈ dom(shaft) ∧ shaft(c) = DOWN ⇒ floor(c) ≠ TOP_FLOOR //SAF 8&#10;    then&#10;      @up_to_down shaft(cabin) ≔ DOWN&#10;  end&#10;&#10;  event CabinDownToUp&#10;    any cabin&#10;    where&#10;      @at_ground_floor floor(cabin) = 0 //REQ 5&#10;      @in_down_shaft shaft(cabin) = DOWN&#10;      @ground_left_free ∀c·c ∈ dom(shaft) ∧ shaft(c) = UP ⇒ floor(c) ≠ 0 //SAF 8&#10;    then&#10;      @down_to_up shaft(cabin) ≔ UP&#10;  end&#10;end&#10;" version="5">
<org.eventb.core.refinesMachine name="_oggNMJ94Eeq6js3PozKjqQ" org.eventb.core.target="m0_cabins"/>
<org.eventb.core.seesContext name="_oggNMZ94Eeq6js3PozKjqQ" org.eventb.core.target="m1_shafts_context"/>
<org.eventb.core.event name="'" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIALISATION">
<org.eventb.core.action name="_oghbUJ94Eeq6js3PozKjqQ" org.eventb.core.assignment="shaft ≔ CABINS × {UP}" org.eventb.core.generated="false" org.eventb.core.label="shafts_init"/>
</org.eventb.core.event>
<org.eventb.core.variable name="_oghbUZ94Eeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="floor"/>
<org.eventb.core.variable name="_ogiCYJ94Eeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="shaft"/>
<org.eventb.core.event name="_ogipcJ94Eeq6js3PozKjqQ" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="CabinMovesDown">
<org.eventb.core.refinesEvent name="_ogjQgJ94Eeq6js3PozKjqQ" org.eventb.core.target="CabinMovesDown"/>
<org.eventb.core.guard name="_r7I2IJ96Eeq6js3PozKjqQ" org.eventb.core.comment="SAF 8" org.eventb.core.generated="false" org.eventb.core.label="lower_floor_free" org.eventb.core.predicate="∀c·c ∈ dom(floor) ∧ shaft(c) = DOWN ⇒ (floor(cabin) − 1) ≠ floor(c)"/>
<org.eventb.core.guard name="_ogj3kJ94Eeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="shaft_down" org.eventb.core.predicate="shaft(cabin) = DOWN"/>
</org.eventb.core.event>
<org.eventb.core.event name="_ogkeoJ94Eeq6js3PozKjqQ" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="CabinMovesUp">
<org.eventb.core.refinesEvent name="_oglFsJ94Eeq6js3PozKjqQ" org.eventb.core.target="CabinMovesUp"/>
<org.eventb.core.guard name="_r7KEQJ96Eeq6js3PozKjqQ" org.eventb.core.comment="SAF 8" org.eventb.core.generated="false" org.eventb.core.label="upper_floor_free" org.eventb.core.predicate="∀c·c ∈ dom(floor) ∧ shaft(c) = UP ⇒ (floor(cabin) + 1) ≠ floor(c)"/>
<org.eventb.core.guard name="_oglswZ94Eeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="shaft_up" org.eventb.core.predicate="shaft(cabin) = UP"/>
</org.eventb.core.event>
<org.eventb.core.event name="_ogmT0J94Eeq6js3PozKjqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="CabinUpToDown">
<org.eventb.core.parameter name="_ogm64J94Eeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cabin"/>
<org.eventb.core.guard name="_0DMRoJ-WEeq6js3PozKjqQ" org.eventb.core.comment="REQ 4" org.eventb.core.generated="false" org.eventb.core.label="at_top_floor" org.eventb.core.predicate="floor(cabin) = TOP_FLOOR"/>
<org.eventb.core.guard name="_0DM4sJ-WEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="in_up_shaft" org.eventb.core.predicate="shaft(cabin) = UP"/>
<org.eventb.core.guard name="_0DNfwJ-WEeq6js3PozKjqQ" org.eventb.core.comment="SAF 8" org.eventb.core.generated="false" org.eventb.core.label="top_right_free" org.eventb.core.predicate="∀c·c ∈ dom(shaft) ∧ shaft(c) = DOWN ⇒ floor(c) ≠ TOP_FLOOR"/>
<org.eventb.core.action name="_0DNfwZ-WEeq6js3PozKjqQ" org.eventb.core.assignment="shaft(cabin) ≔ DOWN" org.eventb.core.generated="false" org.eventb.core.label="up_to_down"/>
</org.eventb.core.event>
<org.eventb.core.event name="_ogowEJ94Eeq6js3PozKjqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="CabinDownToUp">
<org.eventb.core.parameter name="_ogp-MJ94Eeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cabin"/>
<org.eventb.core.guard name="_0DOt4J-WEeq6js3PozKjqQ" org.eventb.core.comment="REQ 5" org.eventb.core.generated="false" org.eventb.core.label="at_ground_floor" org.eventb.core.predicate="floor(cabin) = 0"/>
<org.eventb.core.guard name="_0DPU8J-WEeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="in_down_shaft" org.eventb.core.predicate="shaft(cabin) = DOWN"/>
<org.eventb.core.guard name="_0DP8AJ-WEeq6js3PozKjqQ" org.eventb.core.comment="SAF 8" org.eventb.core.generated="false" org.eventb.core.label="ground_left_free" org.eventb.core.predicate="∀c·c ∈ dom(shaft) ∧ shaft(c) = UP ⇒ floor(c) ≠ 0"/>
<org.eventb.core.action name="_0DQjEJ-WEeq6js3PozKjqQ" org.eventb.core.assignment="shaft(cabin) ≔ UP" org.eventb.core.generated="false" org.eventb.core.label="down_to_up"/>
</org.eventb.core.event>
<org.eventb.core.invariant name="_G2fpUJ97Eeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.label="shaft_type" org.eventb.core.predicate="shaft ∈ CABINS → SHAFTS"/>
</org.eventb.core.machineFile>