m0_cabins.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="1590527933901" org.eventb.texttools.text_representation="machine m0_cabins sees m0_cabins_context&#10;&#10;variables floor&#10;&#10;invariants&#10;  @up_type floor ∈ CABINS → FLOORS&#10;  // @unique_floors ∀c·c ∈ dom(floor) ⇒  floor(c) ∉ ran({c} ⩤ floor)&#10;&#10;events&#10;  event INITIALISATION&#10;    then&#10;      @up_init floor ≔ CABIN_FLOOR&#10;  end&#10;&#10;  event CabinMovesUp&#10;    any cabin&#10;    where&#10;      @not_at_top_floor TOP_FLOOR ≥ floor(cabin) + 1&#10;      // @upper_floor_free (floor(cabin) + 1) ∉ ran(floor)&#10;    then&#10;      @move_up floor(cabin) ≔ floor(cabin) + 1&#10;  end&#10;&#10;  event CabinMovesDown&#10;    any cabin&#10;    where&#10;      @not_at_ground_floor 0 ≤ floor(cabin) − 1&#10;      // @lower_floor_free (floor(cabin) − 1) ∉ ran(floor)&#10;    then&#10;      @move_down floor(cabin) ≔ floor(cabin) − 1&#10;  end&#10;end&#10;" version="5">
<org.eventb.core.seesContext name="_awcWoJ94Eeq6js3PozKjqQ" org.eventb.core.target="m0_cabins_context"/>
<org.eventb.core.event name="'" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="INITIALISATION">
<org.eventb.core.action name="_awc9sJ94Eeq6js3PozKjqQ" org.eventb.core.assignment="floor ≔ CABIN_FLOOR" org.eventb.core.generated="false" org.eventb.core.label="up_init"/>
</org.eventb.core.event>
<org.eventb.core.variable name="_awdkwJ94Eeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="floor"/>
<org.eventb.core.invariant name="_aweL0J94Eeq6js3PozKjqQ" org.eventb.core.comment="@unique_floors ∀c·c ∈ dom(floor) ⇒  floor(c) ∉ ran({c} ⩤ floor)" org.eventb.core.generated="false" org.eventb.core.label="up_type" org.eventb.core.predicate="floor ∈ CABINS → FLOORS"/>
<org.eventb.core.event name="_aweL0Z94Eeq6js3PozKjqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="CabinMovesUp">
<org.eventb.core.parameter name="_awey4J94Eeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cabin"/>
<org.eventb.core.guard name="_awey4Z94Eeq6js3PozKjqQ" org.eventb.core.comment="@upper_floor_free (floor(cabin) + 1) ∉ ran(floor)" org.eventb.core.generated="false" org.eventb.core.label="not_at_top_floor" org.eventb.core.predicate="TOP_FLOOR ≥ floor(cabin) + 1"/>
<org.eventb.core.action name="_awfZ8J94Eeq6js3PozKjqQ" org.eventb.core.assignment="floor(cabin) ≔ floor(cabin) + 1" org.eventb.core.generated="false" org.eventb.core.label="move_up"/>
</org.eventb.core.event>
<org.eventb.core.event name="_awgBAJ94Eeq6js3PozKjqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="CabinMovesDown">
<org.eventb.core.parameter name="_awgoEJ94Eeq6js3PozKjqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cabin"/>
<org.eventb.core.guard name="_awgoEZ94Eeq6js3PozKjqQ" org.eventb.core.comment="@lower_floor_free (floor(cabin) − 1) ∉ ran(floor)" org.eventb.core.generated="false" org.eventb.core.label="not_at_ground_floor" org.eventb.core.predicate="0 ≤ floor(cabin) − 1"/>
<org.eventb.core.action name="_awhPIJ94Eeq6js3PozKjqQ" org.eventb.core.assignment="floor(cabin) ≔ floor(cabin) − 1" org.eventb.core.generated="false" org.eventb.core.label="move_down"/>
</org.eventb.core.event>
</org.eventb.core.machineFile>