m0_cabins.bcm

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scMachineFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd">
<org.eventb.core.scSeesContext name="'" org.eventb.core.scTarget="/MULTI-Elevator/m0_cabins_context.bcc" org.eventb.core.source="/MULTI-Elevator/m0_cabins.bum|org.eventb.core.machineFile#m0_cabins|org.eventb.core.seesContext#_awcWoJ94Eeq6js3PozKjqQ"/>
<org.eventb.core.scInternalContext name="m0_cabins_context">
<org.eventb.core.scAxiom name="'" org.eventb.core.label="top_floor_INT" org.eventb.core.predicate="TOP_FLOOR∈ℕ1" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_MsxEwJ6tEeqVQ6qy3MLSjQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="(" org.eventb.core.label="proB_no_timeout" org.eventb.core.predicate="TOP_FLOOR=7" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_Msxr0J6tEeqVQ6qy3MLSjQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name=")" org.eventb.core.label="floor_enum" org.eventb.core.predicate="FLOORS=0 ‥ TOP_FLOOR" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_MsyS4J6tEeqVQ6qy3MLSjQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="*" org.eventb.core.label="fixed_num_cabins" org.eventb.core.predicate="finite(CABINS)" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_M9xTMJ7DEeqVQ6qy3MLSjQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="+" org.eventb.core.label="num_floors" org.eventb.core.predicate="card(FLOORS)=TOP_FLOOR+1" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_MszhAJ6tEeqVQ6qy3MLSjQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="," org.eventb.core.label="fixed_num_floors" org.eventb.core.predicate="finite(FLOORS)" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_MszhAZ6tEeqVQ6qy3MLSjQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="-" org.eventb.core.label="max_num_cabins" org.eventb.core.predicate="card(CABINS)&lt;card(FLOORS)∗2" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_Rn7VMJ7DEeqVQ6qy3MLSjQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="." org.eventb.core.label="init_cabin_floor" org.eventb.core.predicate="CABIN_FLOOR∈CABINS → FLOORS" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_Ms0vIJ6tEeqVQ6qy3MLSjQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="/" org.eventb.core.label="avoid_collisions" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(CABIN_FLOOR)⇒CABIN_FLOOR(c)∉ran({c} ⩤ CABIN_FLOOR)" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.axiom#_Ms1WMJ6tEeqVQ6qy3MLSjQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scCarrierSet name="CABINS" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.carrierSet#_dp-v4J4VEeq9QKfOiT4EOw" org.eventb.core.type="ℙ(CABINS)"/>
<org.eventb.core.scConstant name="CABIN_FLOOR" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.constant#_kbFmIJ6rEeqVQ6qy3MLSjQ" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
<org.eventb.core.scConstant name="FLOORS" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.constant#_dp_W8Z4VEeq9QKfOiT4EOw" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scConstant name="TOP_FLOOR" org.eventb.core.source="/MULTI-Elevator/m0_cabins_context.buc|org.eventb.core.contextFile#m0_cabins_context|org.eventb.core.constant#_dp_-AJ4VEeq9QKfOiT4EOw" org.eventb.core.type="ℤ"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInvariant name="m0_cabins_contexu" org.eventb.core.label="up_type" org.eventb.core.predicate="floor∈CABINS → FLOORS" org.eventb.core.source="/MULTI-Elevator/m0_cabins.bum|org.eventb.core.machineFile#m0_cabins|org.eventb.core.invariant#_aweL0J94Eeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scVariable name="floor" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/MULTI-Elevator/m0_cabins.bum|org.eventb.core.machineFile#m0_cabins|org.eventb.core.variable#_awdkwJ94Eeq6js3PozKjqQ" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
<org.eventb.core.scEvent name="m0_cabins_contexv" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/MULTI-Elevator/m0_cabins.bum|org.eventb.core.machineFile#m0_cabins|org.eventb.core.event#'">
<org.eventb.core.scAction name="'" org.eventb.core.assignment="floor ≔ CABIN_FLOOR" org.eventb.core.label="up_init" org.eventb.core.source="/MULTI-Elevator/m0_cabins.bum|org.eventb.core.machineFile#m0_cabins|org.eventb.core.event#'|org.eventb.core.action#_awc9sJ94Eeq6js3PozKjqQ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="m0_cabins_contexw" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="CabinMovesUp" org.eventb.core.source="/MULTI-Elevator/m0_cabins.bum|org.eventb.core.machineFile#m0_cabins|org.eventb.core.event#_aweL0Z94Eeq6js3PozKjqQ">
<org.eventb.core.scGuard name="'" org.eventb.core.label="not_at_top_floor" org.eventb.core.predicate="TOP_FLOOR≥floor(cabin)+1" org.eventb.core.source="/MULTI-Elevator/m0_cabins.bum|org.eventb.core.machineFile#m0_cabins|org.eventb.core.event#_aweL0Z94Eeq6js3PozKjqQ|org.eventb.core.guard#_awey4Z94Eeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="cabin" org.eventb.core.source="/MULTI-Elevator/m0_cabins.bum|org.eventb.core.machineFile#m0_cabins|org.eventb.core.event#_aweL0Z94Eeq6js3PozKjqQ|org.eventb.core.parameter#_awey4J94Eeq6js3PozKjqQ" org.eventb.core.type="CABINS"/>
<org.eventb.core.scAction name="cabio" org.eventb.core.assignment="floor ≔ floor{cabin ↦ floor(cabin)+1}" org.eventb.core.label="move_up" org.eventb.core.source="/MULTI-Elevator/m0_cabins.bum|org.eventb.core.machineFile#m0_cabins|org.eventb.core.event#_aweL0Z94Eeq6js3PozKjqQ|org.eventb.core.action#_awfZ8J94Eeq6js3PozKjqQ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="m0_cabins_contexx" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="CabinMovesDown" org.eventb.core.source="/MULTI-Elevator/m0_cabins.bum|org.eventb.core.machineFile#m0_cabins|org.eventb.core.event#_awgBAJ94Eeq6js3PozKjqQ">
<org.eventb.core.scGuard name="'" org.eventb.core.label="not_at_ground_floor" org.eventb.core.predicate="0≤floor(cabin) − 1" org.eventb.core.source="/MULTI-Elevator/m0_cabins.bum|org.eventb.core.machineFile#m0_cabins|org.eventb.core.event#_awgBAJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_awgoEZ94Eeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="cabin" org.eventb.core.source="/MULTI-Elevator/m0_cabins.bum|org.eventb.core.machineFile#m0_cabins|org.eventb.core.event#_awgBAJ94Eeq6js3PozKjqQ|org.eventb.core.parameter#_awgoEJ94Eeq6js3PozKjqQ" org.eventb.core.type="CABINS"/>
<org.eventb.core.scAction name="cabio" org.eventb.core.assignment="floor ≔ floor{cabin ↦ floor(cabin) − 1}" org.eventb.core.label="move_down" org.eventb.core.source="/MULTI-Elevator/m0_cabins.bum|org.eventb.core.machineFile#m0_cabins|org.eventb.core.event#_awgBAJ94Eeq6js3PozKjqQ|org.eventb.core.action#_awhPIJ94Eeq6js3PozKjqQ"/>
</org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>