-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathm4_buttons.bpo
311 lines (311 loc) · 57 KB
/
m4_buttons.bpo
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
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="CABINS" org.eventb.core.type="ℙ(CABINS)"/>
<org.eventb.core.poIdentifier name="CABIN_FLOOR" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
<org.eventb.core.poIdentifier name="FLOORS" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.poIdentifier name="TOP_FLOOR" org.eventb.core.type="ℤ"/>
<org.eventb.core.poPredicate name="CABIN_FLOOS" 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.poPredicate name="CABIN_FLOOT" 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.poPredicate name="CABIN_FLOOU" 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.poPredicate name="CABIN_FLOOV" 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.poPredicate name="CABIN_FLOOW" 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.poPredicate name="CABIN_FLOOX" 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.poPredicate name="CABIN_FLOOY" 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.poPredicate name="CABIN_FLOOZ" 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.poPredicate name="CABIN_FLOO[" 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.poIdentifier name="SHAFTS" org.eventb.core.type="ℙ(SHAFTS)"/>
<org.eventb.core.poIdentifier name="DOWN" org.eventb.core.type="SHAFTS"/>
<org.eventb.core.poIdentifier name="UP" org.eventb.core.type="SHAFTS"/>
<org.eventb.core.poPredicate name="CABIN_FLOO\" 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.poPredicate name="CABIN_FLOO]" 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.poIdentifier name="MOTOR_STATE" org.eventb.core.type="ℙ(MOTOR_STATE)"/>
<org.eventb.core.poIdentifier name="OFF" org.eventb.core.type="MOTOR_STATE"/>
<org.eventb.core.poIdentifier name="ON" org.eventb.core.type="MOTOR_STATE"/>
<org.eventb.core.poPredicate name="MOTOR_STATF" 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.poPredicate name="MOTOR_STATG" 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.poIdentifier name="DOOR_STATE" org.eventb.core.type="ℙ(DOOR_STATE)"/>
<org.eventb.core.poIdentifier name="CLOSED" org.eventb.core.type="DOOR_STATE"/>
<org.eventb.core.poIdentifier name="HALF" org.eventb.core.type="DOOR_STATE"/>
<org.eventb.core.poIdentifier name="OPEN" org.eventb.core.type="DOOR_STATE"/>
<org.eventb.core.poPredicate name="MOTOR_STATH" 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.poPredicate name="MOTOR_STATI" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="cabin_schedule" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
<org.eventb.core.poIdentifier name="door" org.eventb.core.type="ℙ(CABINS×DOOR_STATE)"/>
<org.eventb.core.poIdentifier name="floor" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
<org.eventb.core.poIdentifier name="floor_schedule" org.eventb.core.type="ℙ(ℤ×SHAFTS)"/>
<org.eventb.core.poIdentifier name="motor" org.eventb.core.type="ℙ(CABINS×MOTOR_STATE)"/>
<org.eventb.core.poIdentifier name="shaft" org.eventb.core.type="ℙ(CABINS×SHAFTS)"/>
<org.eventb.core.poPredicate name="floor_schedulf" 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.poPredicate name="floor_schedulg" 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.poPredicate name="floor_schedulh" 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.poPredicate name="floor_scheduli" 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.poPredicate name="floor_schedulj" 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.poPredicate name="floor_schedulk" 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.poPredicateSet>
<org.eventb.core.poSequent name="INITIALISATION/cabin_schedule_type/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTALLHYPm4_buttons_contexw"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(CABINS×ℤ))∈CABINS ↔ FLOORS" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.invariant#_i3IHkKDxEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_hmScAJ-XEeq6js3PozKjqR"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqR"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.invariant#_i3IHkKDxEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poSequent#INITIALISATION\/cabin_schedule_type\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/floor_schedule_type/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTALLHYPm4_buttons_contexw"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(ℤ×SHAFTS))∈FLOORS ↔ SHAFTS" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.invariant#_i3IHkaDxEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/MULTI-Elevator/m3_door.bum|org.eventb.core.machineFile#m3_door|org.eventb.core.event#_hmScAJ-XEeq6js3PozKjqR"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqR"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.invariant#_i3IHkaDxEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poSequent#INITIALISATION\/floor_schedule_type\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTm4_buttons_contexw" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="door'" org.eventb.core.type="ℙ(CABINS×DOOR_STATE)"/>
<org.eventb.core.poIdentifier name="cabin_schedule'" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
<org.eventb.core.poIdentifier name="floor_schedule'" org.eventb.core.type="ℙ(ℤ×SHAFTS)"/>
<org.eventb.core.poIdentifier name="shaft'" org.eventb.core.type="ℙ(CABINS×SHAFTS)"/>
<org.eventb.core.poIdentifier name="motor'" org.eventb.core.type="ℙ(CABINS×MOTOR_STATE)"/>
<org.eventb.core.poIdentifier name="floor'" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPm4_buttons_contexw" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTIDENTm4_buttons_contexw" org.eventb.core.poStamp="0"/>
<org.eventb.core.poSequent name="CabinMovesUp/REQ14/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contexxcabis"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="cabin∈dom(floor)∧floor∈CABINS ⇸ ℤ∧(floor(cabin)∉cabin_schedule[{cabin}]⇒(∃f⦂ℤ·f=floor(cabin)∧UP∉floor_schedule[{f}])∨(∀c⦂CABINS·c∈dom(cabin_schedule)⇒(∀f⦂ℤ·f∈cabin_schedule[{c}]⇒cabin∈dom(floor)∧floor∈CABINS ⇸ ℤ)))" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqS|org.eventb.core.guard#_ZILxQKGaEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqS|org.eventb.core.guard#_ZILxQKGaEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contexxcabis"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTm4_buttons_contexx" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="cabin" org.eventb.core.type="CABINS"/>
<org.eventb.core.poIdentifier name="floor'" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPm4_buttons_contexxcabis" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTIDENTm4_buttons_contexx" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicate name="PRD4" org.eventb.core.predicate="cabin_schedule≠(∅ ⦂ ℙ(CABINS×ℤ))∨floor_schedule≠(∅ ⦂ ℙ(ℤ×SHAFTS))" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqS|org.eventb.core.guard#_GiNrwKGGEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPm4_buttons_contexx" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contexxcabis" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="floor(cabin)∉cabin_schedule[{cabin}]∧((∃f⦂ℤ·f=floor(cabin)∧UP∉floor_schedule[{f}])∨(∃c⦂CABINS·c∈dom(cabin_schedule)∧(∃f⦂ℤ·f∈cabin_schedule[{c}]∧f≥floor(cabin))))" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqS|org.eventb.core.guard#_ZILxQKGaEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="CabinMovesDown/REQ14/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contexycabis"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="cabin∈dom(floor)∧floor∈CABINS ⇸ ℤ∧(floor(cabin)∉cabin_schedule[{cabin}]⇒(∃f⦂ℤ·f=floor(cabin)∧DOWN∉floor_schedule[{f}])∨(∀c⦂CABINS·c∈dom(cabin_schedule)⇒(∀f⦂ℤ·f∈cabin_schedule[{c}]⇒cabin∈dom(floor)∧floor∈CABINS ⇸ ℤ)))" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqT|org.eventb.core.guard#_ZILxQaGaEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqT|org.eventb.core.guard#_ZILxQaGaEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contexycabis"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTm4_buttons_contexy" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="cabin" org.eventb.core.type="CABINS"/>
<org.eventb.core.poIdentifier name="floor'" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPm4_buttons_contexycabis" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTIDENTm4_buttons_contexy" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicate name="PRD4" org.eventb.core.predicate="cabin_schedule≠(∅ ⦂ ℙ(CABINS×ℤ))∨floor_schedule≠(∅ ⦂ ℙ(ℤ×SHAFTS))" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqT|org.eventb.core.guard#_GiNrwqGGEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPm4_buttons_contexy" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contexycabis" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="floor(cabin)∉cabin_schedule[{cabin}]∧((∃f⦂ℤ·f=floor(cabin)∧DOWN∉floor_schedule[{f}])∨(∃c⦂CABINS·c∈dom(cabin_schedule)∧(∃f⦂ℤ·f∈cabin_schedule[{c}]∧f≤floor(cabin))))" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqT|org.eventb.core.guard#_ZILxQaGaEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="CabinDownToUp/REQ14/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contexzcabip"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(cabin_schedule)⇒c∈dom(shaft)∧shaft∈CABINS ⇸ SHAFTS" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqU|org.eventb.core.guard#_ZILxQqGaEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqU|org.eventb.core.guard#_ZILxQqGaEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contexzcabip"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTm4_buttons_contexz" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="cabin" org.eventb.core.type="CABINS"/>
<org.eventb.core.poIdentifier name="shaft'" org.eventb.core.type="ℙ(CABINS×SHAFTS)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPm4_buttons_contexzcabip" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTIDENTm4_buttons_contexz" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPm4_buttons_contexz" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contexzcabip" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(cabin_schedule)∧shaft(c)=DOWN⇒0∉cabin_schedule[{c}]" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqU|org.eventb.core.guard#_ZILxQqGaEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="CabinUpToDown/REQ14/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contex{cabip"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(cabin_schedule)⇒c∈dom(shaft)∧shaft∈CABINS ⇸ SHAFTS" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqV|org.eventb.core.guard#_ZILxQ6GaEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqV|org.eventb.core.guard#_ZILxQ6GaEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contex{cabip"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTm4_buttons_contex{" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="cabin" org.eventb.core.type="CABINS"/>
<org.eventb.core.poIdentifier name="shaft'" org.eventb.core.type="ℙ(CABINS×SHAFTS)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPm4_buttons_contex{cabip" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTIDENTm4_buttons_contex{" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPm4_buttons_contex{" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contex{cabip" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="∀c⦂CABINS·c∈dom(cabin_schedule)∧shaft(c)=UP⇒TOP_FLOOR∉cabin_schedule[{c}]" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqV|org.eventb.core.guard#_ZILxQ6GaEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTm4_buttons_contex|" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="cabin" org.eventb.core.type="CABINS"/>
<org.eventb.core.poIdentifier name="motor'" org.eventb.core.type="ℙ(CABINS×MOTOR_STATE)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPm4_buttons_contex|" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTIDENTm4_buttons_contex\|" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTm4_buttons_contex}" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="cabin" org.eventb.core.type="CABINS"/>
<org.eventb.core.poIdentifier name="motor'" org.eventb.core.type="ℙ(CABINS×MOTOR_STATE)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPm4_buttons_contex}" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTIDENTm4_buttons_contex}" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicateSet>
<org.eventb.core.poSequent name="DoorClosedToHalf/cabin_schedule_type/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTALLHYPm4_buttons_contex~"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="cabin_schedule ∖ {cabin ↦ floor(cabin)}∈CABINS ↔ FLOORS" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.invariant#_i3IHkKDxEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" 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.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqY"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.invariant#_i3IHkKDxEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poSequent#DoorClosedToHalf\/cabin_schedule_type\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="DoorClosedToHalf/floor_schedule_type/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTALLHYPm4_buttons_contex~"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="floor_schedule ∖ {floor(cabin) ↦ shaft(cabin)}∈FLOORS ↔ SHAFTS" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.invariant#_i3IHkaDxEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" 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.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqY"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.invariant#_i3IHkaDxEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poSequent#DoorClosedToHalf\/floor_schedule_type\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="DoorClosedToHalf/remove_floor_request/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of action" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTALLHYPm4_buttons_contex~"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="cabin∈dom(floor)∧floor∈CABINS ⇸ ℤ∧cabin∈dom(shaft)∧shaft∈CABINS ⇸ SHAFTS" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqY|org.eventb.core.action#_BKSoQKDrEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqY|org.eventb.core.action#_BKSoQKDrEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTALLHYPm4_buttons_contex~"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="DoorClosedToHalf/remove_cabin_floor_request/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of action" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTALLHYPm4_buttons_contex~"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="cabin∈dom(floor)∧floor∈CABINS ⇸ ℤ" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqY|org.eventb.core.action#_N9FlUKDrEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_ez6bAJ-XEeq6js3PozKjqY|org.eventb.core.action#_N9FlUKDrEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTALLHYPm4_buttons_contex~"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTm4_buttons_contex~" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="door'" org.eventb.core.type="ℙ(CABINS×DOOR_STATE)"/>
<org.eventb.core.poIdentifier name="cabin_schedule'" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
<org.eventb.core.poIdentifier name="cabin" org.eventb.core.type="CABINS"/>
<org.eventb.core.poIdentifier name="floor_schedule'" org.eventb.core.type="ℙ(ℤ×SHAFTS)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPm4_buttons_contex~" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTIDENTm4_buttons_contex~" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTm4_buttons_contey'" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="door'" org.eventb.core.type="ℙ(CABINS×DOOR_STATE)"/>
<org.eventb.core.poIdentifier name="cabin" org.eventb.core.type="CABINS"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPm4_buttons_contey'" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTIDENTm4_buttons_contey'" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTm4_buttons_contey(" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="door'" org.eventb.core.type="ℙ(CABINS×DOOR_STATE)"/>
<org.eventb.core.poIdentifier name="cabin" org.eventb.core.type="CABINS"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPm4_buttons_contey(" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTIDENTm4_buttons_contey(" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTIDENTm4_buttons_contey)" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="door'" org.eventb.core.type="ℙ(CABINS×DOOR_STATE)"/>
<org.eventb.core.poIdentifier name="cabin" org.eventb.core.type="CABINS"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPm4_buttons_contey)" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTIDENTm4_buttons_contey)" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" 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.poPredicateSet>
<org.eventb.core.poSequent name="UserPressesUpButton/no_cabin_on_floor/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contey*)"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀c⦂CABINS·c∈CABINS⇒c∈dom(floor)∧floor∈CABINS ⇸ ℤ" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvZhsJ-kEeq6js3PozKjqQ|org.eventb.core.guard#_DQnN0KDmEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvZhsJ-kEeq6js3PozKjqQ|org.eventb.core.guard#_DQnN0KDmEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contey*)"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="UserPressesUpButton/floor_schedule_type/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTALLHYPm4_buttons_contey*"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="floor_schedule∪{any_floor ↦ UP}∈FLOORS ↔ SHAFTS" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.invariant#_i3IHkaDxEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvZhsJ-kEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.invariant#_i3IHkaDxEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poSequent#UserPressesUpButton\/floor_schedule_type\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTm4_buttons_contey*" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="any_floor" org.eventb.core.type="ℤ"/>
<org.eventb.core.poIdentifier name="floor_schedule'" org.eventb.core.type="ℙ(ℤ×SHAFTS)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPm4_buttons_contey*)" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTIDENTm4_buttons_contey*" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="any_floor∈FLOORS" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvZhsJ-kEeq6js3PozKjqQ|org.eventb.core.guard#_Ac_d4Z-tEeq6js3PozKjqQ"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="UP∉floor_schedule[{any_floor}]" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvZhsJ-kEeq6js3PozKjqQ|org.eventb.core.guard#_5ah7gKDPEeq6js3PozKjqQ"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="any_floor≠TOP_FLOOR" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvZhsJ-kEeq6js3PozKjqQ|org.eventb.core.guard#_y762IaDLEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPm4_buttons_contey*" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contey*)" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="∀c⦂CABINS·c∈CABINS⇒floor(c)≠any_floor" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvZhsJ-kEeq6js3PozKjqQ|org.eventb.core.guard#_DQnN0KDmEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="UserPressesDownButton/no_cabin_on_floor/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contey+)"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀c⦂CABINS·c∈CABINS⇒c∈dom(floor)∧floor∈CABINS ⇸ ℤ" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvaIwJ-kEeq6js3PozKjqQ|org.eventb.core.guard#_DQxl4KDmEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvaIwJ-kEeq6js3PozKjqQ|org.eventb.core.guard#_DQxl4KDmEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contey+)"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="UserPressesDownButton/floor_schedule_type/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTALLHYPm4_buttons_contey+"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="floor_schedule∪{any_floor ↦ DOWN}∈FLOORS ↔ SHAFTS" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.invariant#_i3IHkaDxEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvaIwJ-kEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.invariant#_i3IHkaDxEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poSequent#UserPressesDownButton\/floor_schedule_type\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTm4_buttons_contey+" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="any_floor" org.eventb.core.type="ℤ"/>
<org.eventb.core.poIdentifier name="floor_schedule'" org.eventb.core.type="ℙ(ℤ×SHAFTS)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPm4_buttons_contey+)" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTIDENTm4_buttons_contey+" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="any_floor∈FLOORS" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvaIwJ-kEeq6js3PozKjqQ|org.eventb.core.guard#_dnLJUKDPEeq6js3PozKjqQ"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="DOWN∉floor_schedule[{any_floor}]" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvaIwJ-kEeq6js3PozKjqQ|org.eventb.core.guard#_HJpW4KDQEeq6js3PozKjqQ"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="any_floor≠0" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvaIwJ-kEeq6js3PozKjqQ|org.eventb.core.guard#_nIbkgKDMEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPm4_buttons_contey+" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contey+)" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="∀c⦂CABINS·c∈CABINS⇒floor(c)≠any_floor" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvaIwJ-kEeq6js3PozKjqQ|org.eventb.core.guard#_DQxl4KDmEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="UserPressesFloorButton/not_at_selected_floor/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contey,("/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="cabin∈dom(floor)∧floor∈CABINS ⇸ ℤ" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvav0J-kEeq6js3PozKjqQ|org.eventb.core.guard#_P9YygqDSEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvav0J-kEeq6js3PozKjqQ|org.eventb.core.guard#_P9YygqDSEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contey,("/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="UserPressesFloorButton/cabin_schedule_type/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTALLHYPm4_buttons_contey,"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="cabin_schedule∪{cabin ↦ selected_floor}∈CABINS ↔ FLOORS" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.invariant#_i3IHkKDxEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvav0J-kEeq6js3PozKjqQ"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.invariant#_i3IHkKDxEeq6js3PozKjqQ"/>
<org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poSequent#UserPressesFloorButton\/cabin_schedule_type\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTm4_buttons_contey," org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poIdentifier name="cabin_schedule'" org.eventb.core.type="ℙ(CABINS×ℤ)"/>
<org.eventb.core.poIdentifier name="cabin" org.eventb.core.type="CABINS"/>
<org.eventb.core.poIdentifier name="selected_floor" org.eventb.core.type="ℤ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTHYPm4_buttons_contey,(" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTIDENTm4_buttons_contey," org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="selected_floor∈FLOORS" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvav0J-kEeq6js3PozKjqQ|org.eventb.core.guard#_P9YygKDSEeq6js3PozKjqQ"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="selected_floor∉cabin_schedule[{cabin}]" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvav0J-kEeq6js3PozKjqQ|org.eventb.core.guard#_P9YygaDSEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPm4_buttons_contey," org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#EVTHYPm4_buttons_contey,(" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="floor(cabin)≠selected_floor" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.event#_xvav0J-kEeq6js3PozKjqQ|org.eventb.core.guard#_P9YygqDSEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/MULTI-Elevator/m4_buttons.bpo|org.eventb.core.poFile#m4_buttons|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="cabin_schedule∈CABINS ↔ FLOORS" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.invariant#_i3IHkKDxEeq6js3PozKjqQ"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="floor_schedule∈FLOORS ↔ SHAFTS" org.eventb.core.source="/MULTI-Elevator/m4_buttons.bum|org.eventb.core.machineFile#m4_buttons|org.eventb.core.invariant#_i3IHkaDxEeq6js3PozKjqQ"/>
</org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>