-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathm3_door.bcm
132 lines (132 loc) · 33.9 KB
/
m3_door.bcm
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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
<?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.scRefinesMachine name="'" org.eventb.core.scTarget="/MULTI-Elevator/m2_motor.bcm" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.refinesMachine#'"/>
<org.eventb.core.scSeesContext name="(" org.eventb.core.scTarget="/MULTI-Elevator/m3_door_context.bcc" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.seesContext#_bEAogJ-cEeq6js3PozKjqQ"/>
<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.scInternalContext name="m3_door_context">
<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.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.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.scInvariant name="m1_shafts_contexu" org.eventb.core.label="shaft_type" org.eventb.core.predicate="shaft∈CABINS → SHAFTS" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.invariant#_G2fpUJ97Eeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="m1_shafts_contexv" org.eventb.core.label="motor_type" org.eventb.core.predicate="motor∈CABINS → MOTOR_STATE" org.eventb.core.source="/MULTI-Elevator/m2_motor.bum|org.eventb.core.machineFile#m2_motor|org.eventb.core.invariant#_OtKD0KFNEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="m1_shafts_contexw" org.eventb.core.label="door_type" org.eventb.core.predicate="door∈CABINS → DOOR_STATE" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.invariant#_UN69sKFNEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="m1_shafts_contexx" org.eventb.core.label="SAF10" org.eventb.core.predicate="∀c⦂CABINS·c∈CABINS∧motor(c)=ON⇒door(c)=CLOSED" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.invariant#_AsXfAJ-fEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="m1_shafts_contexy" org.eventb.core.label="SAF10thm" org.eventb.core.predicate="∀c⦂CABINS·c∈CABINS∧door(c)∈{OPEN,HALF}⇒motor(c)=OFF" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.invariant#_GOxI4J-lEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scVariable name="door" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.variable#_OtiJIJ-eEeq6js3PozKjqQ" org.eventb.core.type="ℙ(CABINS×DOOR_STATE)"/>
<org.eventb.core.scVariable name="floor" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.variable#_ez5z8J-XEeq6js3PozKjqQ" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
<org.eventb.core.scVariable name="motor" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.variable#_VKszIJ-ZEeq6js3PozKjqQ" org.eventb.core.type="ℙ(CABINS×MOTOR_STATE)"/>
<org.eventb.core.scVariable name="shaft" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.variable#_ez6bAJ-XEeq6js3PozKjqQ" org.eventb.core.type="ℙ(CABINS×SHAFTS)"/>
<org.eventb.core.scEvent name="m1_shafts_contexz" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_hmScAJ-XEeq6js3PozKjqR">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/MULTI-Elevator/m2_motor.bcm|org.eventb.core.scMachineFile#m2_motor|org.eventb.core.scEvent#m1_shafts_contexw" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_hmScAJ-XEeq6js3PozKjqR"/>
<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.scAction name="(" org.eventb.core.assignment="shaft ≔ CABINS × {UP}" org.eventb.core.label="shafts_init" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#'|org.eventb.core.action#_oghbUJ94Eeq6js3PozKjqQ"/>
<org.eventb.core.scAction name=")" org.eventb.core.assignment="motor ≔ CABINS × {OFF}" org.eventb.core.label="motor_init" org.eventb.core.source="/MULTI-Elevator/m2_motor.bum|org.eventb.core.machineFile#m2_motor|org.eventb.core.event#'|org.eventb.core.action#_OtD9MKFNEeq6js3PozKjqQ"/>
<org.eventb.core.scAction name="*" org.eventb.core.assignment="door ≔ CABINS × {CLOSED}" org.eventb.core.label="door_type" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_hmScAJ-XEeq6js3PozKjqR|org.eventb.core.action#_dx8jgJ-eEeq6js3PozKjqQ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="m1_shafts_contex{" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="CabinMovesUp" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_hmScAJ-XEeq6js3PozKjqS">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/MULTI-Elevator/m2_motor.bcm|org.eventb.core.scMachineFile#m2_motor|org.eventb.core.scEvent#m1_shafts_contexx" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_hmScAJ-XEeq6js3PozKjqS|org.eventb.core.refinesEvent#'"/>
<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.scGuard name="cabip" org.eventb.core.label="upper_floor_free" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(floor)∧shaft(c)=UP⇒floor(cabin)+1≠floor(c)" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogkeoJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_r7KEQJ96Eeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="cabiq" org.eventb.core.label="shaft_up" org.eventb.core.predicate="shaft(cabin)=UP" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogkeoJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_oglswZ94Eeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="cabir" org.eventb.core.label="is_motor_on" org.eventb.core.predicate="motor(cabin)=ON" org.eventb.core.source="/MULTI-Elevator/m2_motor.bum|org.eventb.core.machineFile#m2_motor|org.eventb.core.event#_dgJtEJ-XEeq6js3PozKjqQ|org.eventb.core.guard#_54oToJ-ZEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<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.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.scEvent>
<org.eventb.core.scEvent name="m1_shafts_contex|" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="CabinMovesDown" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_hmScAJ-XEeq6js3PozKjqT">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/MULTI-Elevator/m2_motor.bcm|org.eventb.core.scMachineFile#m2_motor|org.eventb.core.scEvent#m1_shafts_contexy" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_hmScAJ-XEeq6js3PozKjqT|org.eventb.core.refinesEvent#'"/>
<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.scGuard name="cabip" org.eventb.core.label="lower_floor_free" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(floor)∧shaft(c)=DOWN⇒floor(cabin) − 1≠floor(c)" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogipcJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_r7I2IJ96Eeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="cabiq" org.eventb.core.label="shaft_down" org.eventb.core.predicate="shaft(cabin)=DOWN" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogipcJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_ogj3kJ94Eeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="cabir" org.eventb.core.label="is_motor_on" org.eventb.core.predicate="motor(cabin)=ON" org.eventb.core.source="/MULTI-Elevator/m2_motor.bum|org.eventb.core.machineFile#m2_motor|org.eventb.core.event#_dgK7MJ-XEeq6js3PozKjqQ|org.eventb.core.guard#_54o6sJ-ZEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<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.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.scEvent>
<org.eventb.core.scEvent name="m1_shafts_contex}" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="CabinDownToUp" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_hmScAJ-XEeq6js3PozKjqU">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/MULTI-Elevator/m2_motor.bcm|org.eventb.core.scMachineFile#m2_motor|org.eventb.core.scEvent#m1_shafts_contexz" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_hmScAJ-XEeq6js3PozKjqU|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="at_ground_floor" org.eventb.core.predicate="floor(cabin)=0" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogowEJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DOt4J-WEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="in_down_shaft" org.eventb.core.predicate="shaft(cabin)=DOWN" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogowEJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DPU8J-WEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="ground_left_free" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(shaft)∧shaft(c)=UP⇒floor(c)≠0" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogowEJ94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DP8AJ-WEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="cabip" org.eventb.core.label="is_motor_on" org.eventb.core.predicate="motor(cabin)=ON" org.eventb.core.source="/MULTI-Elevator/m2_motor.bum|org.eventb.core.machineFile#m2_motor|org.eventb.core.event#_dgLiQJ-XEeq6js3PozKjqQ|org.eventb.core.guard#_54qI0J-ZEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="cabio" org.eventb.core.assignment="shaft ≔ shaft{cabin ↦ UP}" org.eventb.core.label="down_to_up" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogowEJ94Eeq6js3PozKjqQ|org.eventb.core.action#_0DQjEJ-WEeq6js3PozKjqQ"/>
<org.eventb.core.scParameter name="cabin" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogowEJ94Eeq6js3PozKjqQ|org.eventb.core.parameter#_ogp-MJ94Eeq6js3PozKjqQ" org.eventb.core.type="CABINS"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="m1_shafts_contex~" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="CabinUpToDown" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_hmScAJ-XEeq6js3PozKjqV">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/MULTI-Elevator/m2_motor.bcm|org.eventb.core.scMachineFile#m2_motor|org.eventb.core.scEvent#m1_shafts_contex{" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_hmScAJ-XEeq6js3PozKjqV|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="at_top_floor" org.eventb.core.predicate="floor(cabin)=TOP_FLOOR" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogmT0J94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DMRoJ-WEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="in_up_shaft" org.eventb.core.predicate="shaft(cabin)=UP" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogmT0J94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DM4sJ-WEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="top_right_free" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(shaft)∧shaft(c)=DOWN⇒floor(c)≠TOP_FLOOR" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogmT0J94Eeq6js3PozKjqQ|org.eventb.core.guard#_0DNfwJ-WEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="cabip" org.eventb.core.label="is_motor_on" org.eventb.core.predicate="motor(cabin)=ON" org.eventb.core.source="/MULTI-Elevator/m2_motor.bum|org.eventb.core.machineFile#m2_motor|org.eventb.core.event#_dgMJUJ-XEeq6js3PozKjqQ|org.eventb.core.guard#_54rW8J-ZEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="cabio" org.eventb.core.assignment="shaft ≔ shaft{cabin ↦ DOWN}" org.eventb.core.label="up_to_down" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogmT0J94Eeq6js3PozKjqQ|org.eventb.core.action#_0DNfwZ-WEeq6js3PozKjqQ"/>
<org.eventb.core.scParameter name="cabin" org.eventb.core.source="/MULTI-Elevator/m1_shafts.bum|org.eventb.core.machineFile#m1_shafts|org.eventb.core.event#_ogmT0J94Eeq6js3PozKjqQ|org.eventb.core.parameter#_ogm64J94Eeq6js3PozKjqQ" org.eventb.core.type="CABINS"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="m1_shafts_contey'" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="MotorStarts" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_hmScAJ-XEeq6js3PozKjqW">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/MULTI-Elevator/m2_motor.bcm|org.eventb.core.scMachineFile#m2_motor|org.eventb.core.scEvent#m1_shafts_contex\|" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_hmScAJ-XEeq6js3PozKjqW|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="is_off" org.eventb.core.predicate="motor(cabin)=OFF" org.eventb.core.source="/MULTI-Elevator/m2_motor.bum|org.eventb.core.machineFile#m2_motor|org.eventb.core.event#_sL6W4J-XEeq6js3PozKjqQ|org.eventb.core.guard#_lSEfUJ-ZEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="cabio" org.eventb.core.assignment="motor ≔ motor{cabin ↦ ON}" org.eventb.core.label="turn_on" org.eventb.core.source="/MULTI-Elevator/m2_motor.bum|org.eventb.core.machineFile#m2_motor|org.eventb.core.event#_sL6W4J-XEeq6js3PozKjqQ|org.eventb.core.action#_lSEfUZ-ZEeq6js3PozKjqQ"/>
<org.eventb.core.scParameter name="cabin" org.eventb.core.source="/MULTI-Elevator/m2_motor.bum|org.eventb.core.machineFile#m2_motor|org.eventb.core.event#_sL6W4J-XEeq6js3PozKjqQ|org.eventb.core.parameter#_lSD4QJ-ZEeq6js3PozKjqQ" org.eventb.core.type="CABINS"/>
<org.eventb.core.scGuard name="cabip" org.eventb.core.label="door_is_closed" org.eventb.core.predicate="door(cabin)=CLOSED" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_hmScAJ-XEeq6js3PozKjqW|org.eventb.core.guard#_wz0KkJ-hEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="m1_shafts_contey(" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="MotorStops" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_hmScAJ-XEeq6js3PozKjqX">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/MULTI-Elevator/m2_motor.bcm|org.eventb.core.scMachineFile#m2_motor|org.eventb.core.scEvent#m1_shafts_contex}" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_hmScAJ-XEeq6js3PozKjqX|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="is_on" org.eventb.core.predicate="motor(cabin)=ON" org.eventb.core.source="/MULTI-Elevator/m2_motor.bum|org.eventb.core.machineFile#m2_motor|org.eventb.core.event#_sL698Z-XEeq6js3PozKjqQ|org.eventb.core.guard#_lSFGYZ-ZEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="cabio" org.eventb.core.assignment="motor ≔ motor{cabin ↦ OFF}" org.eventb.core.label="turn_off" org.eventb.core.source="/MULTI-Elevator/m2_motor.bum|org.eventb.core.machineFile#m2_motor|org.eventb.core.event#_sL698Z-XEeq6js3PozKjqQ|org.eventb.core.action#_lSFtcJ-ZEeq6js3PozKjqQ"/>
<org.eventb.core.scParameter name="cabin" org.eventb.core.source="/MULTI-Elevator/m2_motor.bum|org.eventb.core.machineFile#m2_motor|org.eventb.core.event#_sL698Z-XEeq6js3PozKjqQ|org.eventb.core.parameter#_lSFGYJ-ZEeq6js3PozKjqQ" org.eventb.core.type="CABINS"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="m1_shafts_contey)" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="DoorClosedToHalf" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_sWF-4J-dEeq6js3PozKjqQ">
<org.eventb.core.scGuard name="'" org.eventb.core.label="door_closed" org.eventb.core.predicate="door(cabin)=CLOSED" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_sWF-4J-dEeq6js3PozKjqQ|org.eventb.core.guard#_bOP64J-iEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="motor_off" org.eventb.core.predicate="motor(cabin)=OFF" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_sWF-4J-dEeq6js3PozKjqQ|org.eventb.core.guard#_9W1w0J-iEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="cabin" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_sWF-4J-dEeq6js3PozKjqQ|org.eventb.core.parameter#_bOPT0J-iEeq6js3PozKjqQ" org.eventb.core.type="CABINS"/>
<org.eventb.core.scAction name="cabio" org.eventb.core.assignment="door ≔ door{cabin ↦ HALF}" org.eventb.core.label="half" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_sWF-4J-dEeq6js3PozKjqQ|org.eventb.core.action#_bOP64Z-iEeq6js3PozKjqQ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="m1_shafts_contey*" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="DoorHalfToOpen" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_sWGl8J-dEeq6js3PozKjqQ">
<org.eventb.core.scGuard name="'" org.eventb.core.label="door_half" org.eventb.core.predicate="door(cabin)=HALF" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_sWGl8J-dEeq6js3PozKjqQ|org.eventb.core.guard#_bORJAZ-iEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="cabin" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_sWGl8J-dEeq6js3PozKjqQ|org.eventb.core.parameter#_bORJAJ-iEeq6js3PozKjqQ" org.eventb.core.type="CABINS"/>
<org.eventb.core.scAction name="cabio" org.eventb.core.assignment="door ≔ door{cabin ↦ OPEN}" org.eventb.core.label="open" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_sWGl8J-dEeq6js3PozKjqQ|org.eventb.core.action#_bORwEJ-iEeq6js3PozKjqQ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="m1_shafts_contey+" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="DoorOpenToHalf" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_sWHNAJ-dEeq6js3PozKjqQ">
<org.eventb.core.scGuard name="'" org.eventb.core.label="door_open" org.eventb.core.predicate="door(cabin)=OPEN" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_sWHNAJ-dEeq6js3PozKjqQ|org.eventb.core.guard#_bOSXIZ-iEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="cabin" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_sWHNAJ-dEeq6js3PozKjqQ|org.eventb.core.parameter#_bOSXIJ-iEeq6js3PozKjqQ" org.eventb.core.type="CABINS"/>
<org.eventb.core.scAction name="cabio" org.eventb.core.assignment="door ≔ door{cabin ↦ HALF}" org.eventb.core.label="half" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_sWHNAJ-dEeq6js3PozKjqQ|org.eventb.core.action#_bOS-MJ-iEeq6js3PozKjqQ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="m1_shafts_contey," org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="DoorHalfToClosed" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_sWH0EJ-dEeq6js3PozKjqQ">
<org.eventb.core.scGuard name="'" org.eventb.core.label="door_half" org.eventb.core.predicate="door(cabin)=HALF" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_sWH0EJ-dEeq6js3PozKjqQ|org.eventb.core.guard#_bOUMUJ-iEeq6js3PozKjqQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scParameter name="cabin" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_sWH0EJ-dEeq6js3PozKjqQ|org.eventb.core.parameter#_bOTlQJ-iEeq6js3PozKjqQ" org.eventb.core.type="CABINS"/>
<org.eventb.core.scAction name="cabio" org.eventb.core.assignment="door ≔ door{cabin ↦ CLOSED}" org.eventb.core.label="closed" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_sWH0EJ-dEeq6js3PozKjqQ|org.eventb.core.action#_bOUMUZ-iEeq6js3PozKjqQ"/>
</org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>