-
Notifications
You must be signed in to change notification settings - Fork 1
/
m3_door_context.bcc
41 lines (41 loc) · 9.33 KB
/
m3_door_context.bcc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scContextFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd">
<org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/MULTI-Elevator/m2_motor_context.bcc|org.eventb.core.scContextFile#m2_motor_context" org.eventb.core.source="/MULTI-Elevator/m3_door_context.buc|org.eventb.core.contextFile#m3_door_context|org.eventb.core.extendsContext#'"/>
<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)<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.scInternalContext name="m1_shafts_context">
<org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/MULTI-Elevator/m0_cabins_context.bcc|org.eventb.core.scContextFile#m0_cabins_context" org.eventb.core.source="/MULTI-Elevator/m1_shafts_context.buc|org.eventb.core.contextFile#m1_shafts_context|org.eventb.core.extendsContext#_IuJPsJ6EEeq9QKfOiT4EOw"/>
<org.eventb.core.scAxiom name="m0_cabins_contexu" org.eventb.core.label="shaft_finite" org.eventb.core.predicate="finite(SHAFTS)" org.eventb.core.source="/MULTI-Elevator/m1_shafts_context.buc|org.eventb.core.contextFile#m1_shafts_context|org.eventb.core.axiom#_Zy9zQKFQEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="m0_cabins_contexv" org.eventb.core.label="shafts" org.eventb.core.predicate="partition(SHAFTS,{UP},{DOWN})" org.eventb.core.source="/MULTI-Elevator/m1_shafts_context.buc|org.eventb.core.contextFile#m1_shafts_context|org.eventb.core.axiom#_Zy-aUKFQEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scConstant name="DOWN" org.eventb.core.source="/MULTI-Elevator/m1_shafts_context.buc|org.eventb.core.contextFile#m1_shafts_context|org.eventb.core.constant#_A8RWIp9FEeq6js3PozKjqQ" org.eventb.core.type="SHAFTS"/>
<org.eventb.core.scCarrierSet name="SHAFTS" org.eventb.core.source="/MULTI-Elevator/m1_shafts_context.buc|org.eventb.core.contextFile#m1_shafts_context|org.eventb.core.carrierSet#_A8RWIJ9FEeq6js3PozKjqQ" org.eventb.core.type="ℙ(SHAFTS)"/>
<org.eventb.core.scConstant name="UP" org.eventb.core.source="/MULTI-Elevator/m1_shafts_context.buc|org.eventb.core.contextFile#m1_shafts_context|org.eventb.core.constant#_A8RWIZ9FEeq6js3PozKjqQ" org.eventb.core.type="SHAFTS"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInternalContext name="m2_motor_context">
<org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/MULTI-Elevator/m1_shafts_context.bcc|org.eventb.core.scContextFile#m1_shafts_context" org.eventb.core.source="/MULTI-Elevator/m2_motor_context.buc|org.eventb.core.contextFile#m2_motor_context|org.eventb.core.extendsContext#_LAqS8J-XEeq6js3PozKjqQ"/>
<org.eventb.core.scAxiom name="m1_shafts_contexu" org.eventb.core.label="motor_finite" org.eventb.core.predicate="finite(MOTOR_STATE)" org.eventb.core.source="/MULTI-Elevator/m2_motor_context.buc|org.eventb.core.contextFile#m2_motor_context|org.eventb.core.axiom#_brXfUKFQEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="m1_shafts_contexv" org.eventb.core.label="motor" org.eventb.core.predicate="partition(MOTOR_STATE,{ON},{OFF})" org.eventb.core.source="/MULTI-Elevator/m2_motor_context.buc|org.eventb.core.contextFile#m2_motor_context|org.eventb.core.axiom#_brXfUaFQEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scCarrierSet name="MOTOR_STATE" org.eventb.core.source="/MULTI-Elevator/m2_motor_context.buc|org.eventb.core.contextFile#m2_motor_context|org.eventb.core.carrierSet#__eDggJ-YEeq6js3PozKjqQ" org.eventb.core.type="ℙ(MOTOR_STATE)"/>
<org.eventb.core.scConstant name="OFF" org.eventb.core.source="/MULTI-Elevator/m2_motor_context.buc|org.eventb.core.contextFile#m2_motor_context|org.eventb.core.constant#__eEHkZ-YEeq6js3PozKjqQ" org.eventb.core.type="MOTOR_STATE"/>
<org.eventb.core.scConstant name="ON" org.eventb.core.source="/MULTI-Elevator/m2_motor_context.buc|org.eventb.core.contextFile#m2_motor_context|org.eventb.core.constant#__eEHkJ-YEeq6js3PozKjqQ" org.eventb.core.type="MOTOR_STATE"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scAxiom name="m1_shafts_contexu" org.eventb.core.label="door_finite" org.eventb.core.predicate="finite(DOOR_STATE)" org.eventb.core.source="/MULTI-Elevator/m3_door_context.buc|org.eventb.core.contextFile#m3_door_context|org.eventb.core.axiom#_dFdewKFQEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="m1_shafts_contexv" org.eventb.core.label="door" org.eventb.core.predicate="partition(DOOR_STATE,{OPEN},{HALF},{CLOSED})" org.eventb.core.source="/MULTI-Elevator/m3_door_context.buc|org.eventb.core.contextFile#m3_door_context|org.eventb.core.axiom#_dFeF0KFQEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scConstant name="CLOSED" org.eventb.core.source="/MULTI-Elevator/m3_door_context.buc|org.eventb.core.contextFile#m3_door_context|org.eventb.core.constant#_Gf1u8J-eEeq6js3PozKjqQ" org.eventb.core.type="DOOR_STATE"/>
<org.eventb.core.scCarrierSet name="DOOR_STATE" org.eventb.core.source="/MULTI-Elevator/m3_door_context.buc|org.eventb.core.contextFile#m3_door_context|org.eventb.core.carrierSet#_Gf0g0J-eEeq6js3PozKjqQ" org.eventb.core.type="ℙ(DOOR_STATE)"/>
<org.eventb.core.scConstant name="HALF" org.eventb.core.source="/MULTI-Elevator/m3_door_context.buc|org.eventb.core.contextFile#m3_door_context|org.eventb.core.constant#_Gf1H4Z-eEeq6js3PozKjqQ" org.eventb.core.type="DOOR_STATE"/>
<org.eventb.core.scConstant name="OPEN" org.eventb.core.source="/MULTI-Elevator/m3_door_context.buc|org.eventb.core.contextFile#m3_door_context|org.eventb.core.constant#_Gf1H4J-eEeq6js3PozKjqQ" org.eventb.core.type="DOOR_STATE"/>
</org.eventb.core.scContextFile>