-
Notifications
You must be signed in to change notification settings - Fork 0
/
lift11_conv_lights.bcm
523 lines (523 loc) · 158 KB
/
lift11_conv_lights.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
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
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
<?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="REF" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.refinesMachine#_mbd0oPluEd-1httaBm5m2g"/>
<org.eventb.core.scSeesContext name="SEES0" org.eventb.core.scTarget="/ProvenLift/ctx5_scheduler.bcc" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.seesContext#_mbd0ofluEd-1httaBm5m2g"/>
<org.eventb.core.scInternalContext name="ctx1_floors">
<org.eventb.core.scAxiom name="AXM0" org.eventb.core.label="axm1_1" org.eventb.core.predicate="LAST_FLOOR∈ℕ1" org.eventb.core.source="/ProvenLift/ctx1_floors.buc|org.eventb.core.contextFile#ctx1_floors|org.eventb.core.axiom#_lTa6wdd9Ed-Dle0at0Xgqg" org.eventb.core.theorem="false"/>
<org.eventb.core.scConstant name="LAST_FLOOR" org.eventb.core.source="/ProvenLift/ctx1_floors.buc|org.eventb.core.contextFile#ctx1_floors|org.eventb.core.constant#_lTa6wNd9Ed-Dle0at0Xgqg" org.eventb.core.type="ℤ"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInternalContext name="ctx2_main_engine">
<org.eventb.core.scExtendsContext name="EXTENDS0" org.eventb.core.scTarget="/ProvenLift/ctx1_floors.bcc|org.eventb.core.scContextFile#ctx1_floors" org.eventb.core.source="/ProvenLift/ctx2_main_engine.buc|org.eventb.core.contextFile#ctx2_main_engine|org.eventb.core.extendsContext#_B_rrkeApEd-pAbDae3T1Gg"/>
<org.eventb.core.scAxiom name="AXM0" org.eventb.core.label="axm2_1" org.eventb.core.predicate="b2n∈BOOL ⤖ {0,1}" org.eventb.core.source="/ProvenLift/ctx2_main_engine.buc|org.eventb.core.contextFile#ctx2_main_engine|org.eventb.core.axiom#_v-34INqvEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="AXM1" org.eventb.core.label="axm2_2" org.eventb.core.predicate="b2n(TRUE)=1" org.eventb.core.source="/ProvenLift/ctx2_main_engine.buc|org.eventb.core.contextFile#ctx2_main_engine|org.eventb.core.axiom#_v-4fMNqvEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="AXM2" org.eventb.core.label="axm2_3" org.eventb.core.predicate="b2n(FALSE)=0" org.eventb.core.source="/ProvenLift/ctx2_main_engine.buc|org.eventb.core.contextFile#ctx2_main_engine|org.eventb.core.axiom#_v-4fMdqvEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="AXM3" org.eventb.core.label="axm2_4" org.eventb.core.predicate="partition(CABLE_COMMAND,{CABLE_STOP},{CABLE_WIND},{CABLE_UNWIND})" org.eventb.core.source="/ProvenLift/ctx2_main_engine.buc|org.eventb.core.contextFile#ctx2_main_engine|org.eventb.core.axiom#_V2CJMNq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scCarrierSet name="CABLE_COMMAND" org.eventb.core.source="/ProvenLift/ctx2_main_engine.buc|org.eventb.core.contextFile#ctx2_main_engine|org.eventb.core.carrierSet#_HLX3Mtd_Ed-Dle0at0Xgqg" org.eventb.core.type="ℙ(CABLE_COMMAND)"/>
<org.eventb.core.scConstant name="CABLE_STOP" org.eventb.core.source="/ProvenLift/ctx2_main_engine.buc|org.eventb.core.contextFile#ctx2_main_engine|org.eventb.core.constant#_HLYeQdd_Ed-Dle0at0Xgqg" org.eventb.core.type="CABLE_COMMAND"/>
<org.eventb.core.scConstant name="CABLE_UNWIND" org.eventb.core.source="/ProvenLift/ctx2_main_engine.buc|org.eventb.core.contextFile#ctx2_main_engine|org.eventb.core.constant#_HLYeQ9d_Ed-Dle0at0Xgqg" org.eventb.core.type="CABLE_COMMAND"/>
<org.eventb.core.scConstant name="CABLE_WIND" org.eventb.core.source="/ProvenLift/ctx2_main_engine.buc|org.eventb.core.contextFile#ctx2_main_engine|org.eventb.core.constant#_HLYeQtd_Ed-Dle0at0Xgqg" org.eventb.core.type="CABLE_COMMAND"/>
<org.eventb.core.scConstant name="b2n" org.eventb.core.source="/ProvenLift/ctx2_main_engine.buc|org.eventb.core.contextFile#ctx2_main_engine|org.eventb.core.constant#_v-3RENqvEd-O4vbSPlarTw" org.eventb.core.type="ℙ(BOOL×ℤ)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInternalContext name="ctx3_door_engine">
<org.eventb.core.scExtendsContext name="EXTENDS0" org.eventb.core.scTarget="/ProvenLift/ctx2_main_engine.bcc|org.eventb.core.scContextFile#ctx2_main_engine" org.eventb.core.source="/ProvenLift/ctx3_door_engine.buc|org.eventb.core.contextFile#ctx3_door_engine|org.eventb.core.extendsContext#_ra8a8N0VEd-DHKwvWNa8WQ"/>
<org.eventb.core.scAxiom name="AXM0" org.eventb.core.label="axm3_1" org.eventb.core.predicate="partition(DOOR_COMMAND,{DOOR_STOP},{DOOR_OPEN},{DOOR_CLOSE})" org.eventb.core.source="/ProvenLift/ctx3_door_engine.buc|org.eventb.core.contextFile#ctx3_door_engine|org.eventb.core.axiom#_STnBwNqyEd-7IuFxCL4SWw" org.eventb.core.theorem="false"/>
<org.eventb.core.scConstant name="DOOR_CLOSE" org.eventb.core.source="/ProvenLift/ctx3_door_engine.buc|org.eventb.core.contextFile#ctx3_door_engine|org.eventb.core.constant#_STmas9qyEd-7IuFxCL4SWw" org.eventb.core.type="DOOR_COMMAND"/>
<org.eventb.core.scCarrierSet name="DOOR_COMMAND" org.eventb.core.source="/ProvenLift/ctx3_door_engine.buc|org.eventb.core.contextFile#ctx3_door_engine|org.eventb.core.carrierSet#_STmasdqyEd-7IuFxCL4SWw" org.eventb.core.type="ℙ(DOOR_COMMAND)"/>
<org.eventb.core.scConstant name="DOOR_OPEN" org.eventb.core.source="/ProvenLift/ctx3_door_engine.buc|org.eventb.core.contextFile#ctx3_door_engine|org.eventb.core.constant#_STmastqyEd-7IuFxCL4SWw" org.eventb.core.type="DOOR_COMMAND"/>
<org.eventb.core.scConstant name="DOOR_STOP" org.eventb.core.source="/ProvenLift/ctx3_door_engine.buc|org.eventb.core.contextFile#ctx3_door_engine|org.eventb.core.constant#_bxPu8Nq0Ed-AAt710HomgA" org.eventb.core.type="DOOR_COMMAND"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInternalContext name="ctx4_door_position">
<org.eventb.core.scExtendsContext name="EXTENDS0" org.eventb.core.scTarget="/ProvenLift/ctx3_door_engine.bcc|org.eventb.core.scContextFile#ctx3_door_engine" org.eventb.core.source="/ProvenLift/ctx4_door_position.buc|org.eventb.core.contextFile#ctx4_door_position|org.eventb.core.extendsContext#_JTwHYeAvEd-73py7lbE8bg"/>
<org.eventb.core.scAxiom name="AXM0" org.eventb.core.label="axm2" org.eventb.core.predicate="partition(DOOR_POSITION,{DOOR_OPENED},{DOOR_HALF},{DOOR_CLOSED})" org.eventb.core.source="/ProvenLift/ctx4_door_position.buc|org.eventb.core.contextFile#ctx4_door_position|org.eventb.core.axiom#_JTwudOAvEd-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scConstant name="DOOR_CLOSED" org.eventb.core.source="/ProvenLift/ctx4_door_position.buc|org.eventb.core.contextFile#ctx4_door_position|org.eventb.core.constant#_JTwucuAvEd-73py7lbE8bg" org.eventb.core.type="DOOR_POSITION"/>
<org.eventb.core.scConstant name="DOOR_HALF" org.eventb.core.source="/ProvenLift/ctx4_door_position.buc|org.eventb.core.contextFile#ctx4_door_position|org.eventb.core.constant#_JTwuceAvEd-73py7lbE8bg" org.eventb.core.type="DOOR_POSITION"/>
<org.eventb.core.scConstant name="DOOR_OPENED" org.eventb.core.source="/ProvenLift/ctx4_door_position.buc|org.eventb.core.contextFile#ctx4_door_position|org.eventb.core.constant#_JTwuc-AvEd-73py7lbE8bg" org.eventb.core.type="DOOR_POSITION"/>
<org.eventb.core.scCarrierSet name="DOOR_POSITION" org.eventb.core.source="/ProvenLift/ctx4_door_position.buc|org.eventb.core.contextFile#ctx4_door_position|org.eventb.core.carrierSet#_JTwucOAvEd-73py7lbE8bg" org.eventb.core.type="ℙ(DOOR_POSITION)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInternalContext name="ctx5_scheduler">
<org.eventb.core.scExtendsContext name="EXTENDS0" org.eventb.core.scTarget="/ProvenLift/ctx4_door_position.bcc|org.eventb.core.scContextFile#ctx4_door_position" org.eventb.core.source="/ProvenLift/ctx5_scheduler.buc|org.eventb.core.contextFile#ctx5_scheduler|org.eventb.core.extendsContext#_G6XFgOW-Ed-64JNDK1TKiQ"/>
<org.eventb.core.scAxiom name="AXM0" org.eventb.core.label="axm5_1" org.eventb.core.predicate="partition(SCHEDULER_STRATEGY,{SCHEDULER_UP},{SCHEDULER_DOWN},{SCHEDULER_WAIT})" org.eventb.core.source="/ProvenLift/ctx5_scheduler.buc|org.eventb.core.contextFile#ctx5_scheduler|org.eventb.core.axiom#_G6XslOW-Ed-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scConstant name="SCHEDULER_DOWN" org.eventb.core.source="/ProvenLift/ctx5_scheduler.buc|org.eventb.core.contextFile#ctx5_scheduler|org.eventb.core.constant#_G6XskuW-Ed-64JNDK1TKiQ" org.eventb.core.type="SCHEDULER_STRATEGY"/>
<org.eventb.core.scCarrierSet name="SCHEDULER_STRATEGY" org.eventb.core.source="/ProvenLift/ctx5_scheduler.buc|org.eventb.core.contextFile#ctx5_scheduler|org.eventb.core.carrierSet#_G6XskOW-Ed-64JNDK1TKiQ" org.eventb.core.type="ℙ(SCHEDULER_STRATEGY)"/>
<org.eventb.core.scConstant name="SCHEDULER_UP" org.eventb.core.source="/ProvenLift/ctx5_scheduler.buc|org.eventb.core.contextFile#ctx5_scheduler|org.eventb.core.constant#_G6XskeW-Ed-64JNDK1TKiQ" org.eventb.core.type="SCHEDULER_STRATEGY"/>
<org.eventb.core.scConstant name="SCHEDULER_WAIT" org.eventb.core.source="/ProvenLift/ctx5_scheduler.buc|org.eventb.core.contextFile#ctx5_scheduler|org.eventb.core.constant#_G6Xsk-W-Ed-64JNDK1TKiQ" org.eventb.core.type="SCHEDULER_STRATEGY"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInvariant name="INV0" org.eventb.core.label="inv1_1" org.eventb.core.predicate="PhyElevatorFloor∈ℕ" org.eventb.core.source="/ProvenLift/lift01_floors.bum|org.eventb.core.machineFile#lift01_floors|org.eventb.core.invariant#_9uEEsdd9Ed-Dle0at0Xgqg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV1" org.eventb.core.label="inv1_2" org.eventb.core.predicate="PhyElevatorFloor≤LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift01_floors.bum|org.eventb.core.machineFile#lift01_floors|org.eventb.core.invariant#_9uEEstd9Ed-Dle0at0Xgqg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV2" org.eventb.core.label="dlf1_1" org.eventb.core.predicate="PhyElevatorFloor<LAST_FLOOR∨0<PhyElevatorFloor" org.eventb.core.source="/ProvenLift/lift01_floors.bum|org.eventb.core.machineFile#lift01_floors|org.eventb.core.invariant#_VO9DcNqwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV3" org.eventb.core.label="inv2_1" org.eventb.core.predicate="ctrlCableCommand∈CABLE_COMMAND" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.invariant#_1cMqQNd_Ed-Dle0at0Xgqg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV4" org.eventb.core.label="inv2_2" org.eventb.core.predicate="last_stop∈0 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.invariant#_yC1egNqwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV5" org.eventb.core.label="inv3_1" org.eventb.core.predicate="ctrlDoorCommand∈DOOR_COMMAND" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.invariant#_HKimINqzEd-7IuFxCL4SWw" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV6" org.eventb.core.label="inv3_2" org.eventb.core.predicate="ctrlCableCommand≠CABLE_STOP⇒ctrlDoorCommand=DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.invariant#_Sjk-INq3Ed-AAt710HomgA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV7" org.eventb.core.label="inv4_1" org.eventb.core.predicate="PhyCableEngine∈CABLE_COMMAND" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.invariant#_aGwXhNq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV8" org.eventb.core.label="inv4_3" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors∈BOOL" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.invariant#_aGwXhtq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV9" org.eventb.core.label="inv4_4" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=TRUE⇒PhyElevatorFloor≠LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.invariant#_aGw-kNq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV10" org.eventb.core.label="inv4_5" org.eventb.core.predicate="snsrCableEngine∈CABLE_COMMAND" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.invariant#_b-ESs90UEd-DHKwvWNa8WQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV11" org.eventb.core.label="inv4_6" org.eventb.core.predicate="snsrCableEngine=PhyCableEngine" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.invariant#_b-ESsd0UEd-DHKwvWNa8WQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV12" org.eventb.core.label="inv4_7" org.eventb.core.predicate="snsrElevatorFloor∈−1 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.invariant#_b-E5wt0UEd-DHKwvWNa8WQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV13" org.eventb.core.label="inv4_8" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=TRUE⇒snsrElevatorFloor=−1" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.invariant#_b-ESst0UEd-DHKwvWNa8WQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV14" org.eventb.core.label="inv4_9" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=FALSE⇒snsrElevatorFloor=PhyElevatorFloor" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.invariant#_b-E5wd0UEd-DHKwvWNa8WQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV15" org.eventb.core.label="inv4_10" org.eventb.core.predicate="snsrElevatorFloor=−1⇒ctrlCableCommand≠CABLE_STOP" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.invariant#_b-Fg0t0UEd-DHKwvWNa8WQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV16" org.eventb.core.label="inv4_11" org.eventb.core.predicate="snsrElevatorFloor=−1⇒PhyCableEngine≠CABLE_STOP" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.invariant#_b-Fg0d0UEd-DHKwvWNa8WQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV17" org.eventb.core.label="inv4_12" org.eventb.core.predicate="snsrCableEngine≠CABLE_STOP⇒ctrlDoorCommand=DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.invariant#_b-ESsN0UEd-DHKwvWNa8WQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV18" org.eventb.core.label="inv4_13" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP⇒PhyElevatorFloor=snsrElevatorFloor" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.invariant#_b-Fg0N0UEd-DHKwvWNa8WQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV19" org.eventb.core.label="inv4_14" org.eventb.core.predicate="snsrCableEngine=CABLE_STOP⇒PhyElevatorFloor=snsrElevatorFloor" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.invariant#_b-E5wN0UEd-DHKwvWNa8WQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV20" org.eventb.core.label="inv5_1" org.eventb.core.predicate="PhyDoorEngine∈DOOR_COMMAND" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.invariant#_F6UpROA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV21" org.eventb.core.label="inv5_2" org.eventb.core.predicate="PhyDoorPosition∈DOOR_POSITION" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.invariant#_F6VQUOA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV22" org.eventb.core.label="inv5_3" org.eventb.core.predicate="snsrDoorEngine∈DOOR_COMMAND" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.invariant#_F6VQUeA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV23" org.eventb.core.label="inv5_4" org.eventb.core.predicate="snsrDoorEngine=PhyDoorEngine" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.invariant#_F6VQUuA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV24" org.eventb.core.label="inv5_5" org.eventb.core.predicate="snsrDoorPosition∈DOOR_POSITION" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.invariant#_F6VQU-A2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV25" org.eventb.core.label="inv5_6" org.eventb.core.predicate="snsrDoorPosition=PhyDoorPosition" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.invariant#_F6VQVOA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV26" org.eventb.core.label="inv5_7" org.eventb.core.predicate="ctrlCableCommand≠CABLE_STOP⇒snsrDoorEngine=DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.invariant#_F6V3YOA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV27" org.eventb.core.label="inv5_8" org.eventb.core.predicate="ctrlCableCommand≠CABLE_STOP⇒snsrDoorPosition=DOOR_CLOSED" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.invariant#_F6V3YeA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV28" org.eventb.core.label="inv5_9" org.eventb.core.predicate="PhyCableEngine≠CABLE_STOP⇒PhyDoorEngine=DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.invariant#_jjwDAPTAEd-43_jmKUh78g" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV29" org.eventb.core.label="inv5_10" org.eventb.core.predicate="PhyCableEngine≠CABLE_STOP⇒PhyDoorPosition=DOOR_CLOSED" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.invariant#_jjwqEPTAEd-43_jmKUh78g" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV30" org.eventb.core.label="inv6_1" org.eventb.core.predicate="PhyFloorButtonsSet⊆0 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.invariant#_tIzr4-A_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV31" org.eventb.core.label="inv6_2" org.eventb.core.predicate="snsrFloorButtonsSet⊆0 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.invariant#_tI0S8OA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV32" org.eventb.core.label="inv6_3" org.eventb.core.predicate="snsrFloorButtonsSet=PhyFloorButtonsSet" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.invariant#_tI0S8eA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV33" org.eventb.core.label="inv6_4" org.eventb.core.predicate="PhyFloorButtonLightsSet⊆0 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.invariant#_tI0S8uA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV34" org.eventb.core.label="inv6_5" org.eventb.core.predicate="ctrlFloorButtonLightsSet⊆0 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.invariant#_tI0S8-A_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV35" org.eventb.core.label="inv7_1" org.eventb.core.predicate="PhyUpButtonsSet⊆0 ‥ (LAST_FLOOR − 1)" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.invariant#_pvUD0eEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV36" org.eventb.core.label="inv7_2" org.eventb.core.predicate="snsrUpButtonsSet⊆0 ‥ (LAST_FLOOR − 1)" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.invariant#_pvUD0uEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV37" org.eventb.core.label="inv7_3" org.eventb.core.predicate="snsrUpButtonsSet=PhyUpButtonsSet" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.invariant#_pvUD0-EsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV38" org.eventb.core.label="inv7_4" org.eventb.core.predicate="PhyUpButtonLightsSet⊆0 ‥ (LAST_FLOOR − 1)" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.invariant#_pvUD1OEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV39" org.eventb.core.label="inv7_5" org.eventb.core.predicate="ctrlUpButtonLightsSet⊆0 ‥ (LAST_FLOOR − 1)" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.invariant#_pvUq4OEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV40" org.eventb.core.label="inv8_1" org.eventb.core.predicate="PhyDownButtonsSet⊆1 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.invariant#_3IjapOWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV41" org.eventb.core.label="inv8_2" org.eventb.core.predicate="snsrDownButtonsSet⊆1 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.invariant#_3IjapeWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV42" org.eventb.core.label="inv8_3" org.eventb.core.predicate="snsrDownButtonsSet=PhyDownButtonsSet" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.invariant#_3IkBsOWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV43" org.eventb.core.label="inv8_4" org.eventb.core.predicate="PhyDownButtonLightsSet⊆1 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.invariant#_3IkBseWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV44" org.eventb.core.label="inv8_5" org.eventb.core.predicate="ctrlDownButtonLightsSet⊆1 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.invariant#_3IkBsuWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV45" org.eventb.core.label="inv8_6" org.eventb.core.predicate="requests⊆0 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.invariant#_yPBqcfk7Ed-WtNZH8d5nSA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV46" org.eventb.core.label="inv8_7" org.eventb.core.predicate="requests=ctrlFloorButtonLightsSet∪ctrlUpButtonLightsSet∪ctrlDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.invariant#_yPBqcvk7Ed-WtNZH8d5nSA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV47" org.eventb.core.label="inv9_1" org.eventb.core.predicate="schedule∈SCHEDULER_STRATEGY" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.invariant#_UthHgO5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV48" org.eventb.core.label="inv9_3" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP∧PhyElevatorFloor=LAST_FLOOR⇒schedule≠SCHEDULER_UP" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.invariant#_UthHge5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV49" org.eventb.core.label="inv9_2" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP∧PhyElevatorFloor=0⇒schedule≠SCHEDULER_DOWN" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.invariant#_UthHgu5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV50" org.eventb.core.label="inv9_4" org.eventb.core.predicate="last_schedule∈{SCHEDULER_UP,SCHEDULER_DOWN}" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.invariant#_UthHg-5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV51" org.eventb.core.label="inv9_5" org.eventb.core.predicate="schedule=SCHEDULER_WAIT⇒ctrlCableCommand=CABLE_STOP" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.invariant#_0m_agO5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV52" org.eventb.core.label="inv9_6" org.eventb.core.predicate="requests=(∅ ⦂ ℙ(ℤ))⇒schedule=SCHEDULER_WAIT" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.invariant#_-x_t0PexEd-p8t79IbuE0Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV53" org.eventb.core.label="inv9_7" org.eventb.core.predicate="schedule≠SCHEDULER_WAIT∧ctrlCableCommand=CABLE_STOP⇒requests ∖ {snsrElevatorFloor}≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.invariant#_-x_t0fexEd-p8t79IbuE0Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV54" org.eventb.core.label="inv9_8" org.eventb.core.predicate="requests=(∅ ⦂ ℙ(ℤ))⇒PhyCableEngine=CABLE_STOP" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.invariant#_-x_t0vexEd-p8t79IbuE0Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV55" org.eventb.core.label="inv9_9" org.eventb.core.predicate="ctrlCableCommand=CABLE_WIND⇒schedule=SCHEDULER_UP" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.invariant#_-x_t0_exEd-p8t79IbuE0Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV56" org.eventb.core.label="inv9_10" org.eventb.core.predicate="ctrlCableCommand=CABLE_UNWIND⇒schedule=SCHEDULER_DOWN" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.invariant#_-x_t1PexEd-p8t79IbuE0Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV57" org.eventb.core.label="inv9_11" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP∧PhyCableEngine≠CABLE_STOP⇒snsrElevatorFloor∈requests" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.invariant#_-yAU4PexEd-p8t79IbuE0Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV58" org.eventb.core.label="inv9_12" org.eventb.core.predicate="schedule≠SCHEDULER_WAIT⇒schedule=last_schedule" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.invariant#_6H4dEPk7Ed-WtNZH8d5nSA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV59" org.eventb.core.label="inv9_13" org.eventb.core.predicate="ctrlCableCommand≠CABLE_STOP⇒schedule=last_schedule" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.invariant#_6H4dEfk7Ed-WtNZH8d5nSA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="INV60" org.eventb.core.label="inv9_14" org.eventb.core.predicate="request_served∈BOOL" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.invariant#_q3de0PluEd-1httaBm5m2g" org.eventb.core.theorem="false"/>
<org.eventb.core.scVariable name="PhyCableEngine" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_aGvwctq-Ed-L_e8_V4iXIg" org.eventb.core.type="CABLE_COMMAND"/>
<org.eventb.core.scVariable name="PhyDoorEngine" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_KgYVwOAzEd-73py7lbE8bg" org.eventb.core.type="DOOR_COMMAND"/>
<org.eventb.core.scVariable name="PhyDoorPosition" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_KgYVweAzEd-73py7lbE8bg" org.eventb.core.type="DOOR_POSITION"/>
<org.eventb.core.scVariable name="PhyDownButtonLightsSet" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_3IjaouWyEd-64JNDK1TKiQ" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scVariable name="PhyDownButtonsSet" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_3IjaoOWyEd-64JNDK1TKiQ" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scVariable name="PhyElevatorBetweenTwoFloors" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_aGwXgNq-Ed-L_e8_V4iXIg" org.eventb.core.type="BOOL"/>
<org.eventb.core.scVariable name="PhyElevatorFloor" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_9uEEsNd9Ed-Dle0at0Xgqg" org.eventb.core.type="ℤ"/>
<org.eventb.core.scVariable name="PhyFloorButtonLightsSet" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_tIzr4eA_Ed-78bCl9yYd-Q" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scVariable name="PhyFloorButtonsSet" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_tIzE0OA_Ed-78bCl9yYd-Q" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scVariable name="PhyUpButtonLightsSet" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_pvTcwuEsEd-bh-7nDQnLgQ" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scVariable name="PhyUpButtonsSet" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_pvTcwOEsEd-bh-7nDQnLgQ" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scVariable name="ctrlCableCommand" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_1cMDMtd_Ed-Dle0at0Xgqg" org.eventb.core.type="CABLE_COMMAND"/>
<org.eventb.core.scVariable name="ctrlDoorCommand" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_HKh_EtqzEd-7IuFxCL4SWw" org.eventb.core.type="DOOR_COMMAND"/>
<org.eventb.core.scVariable name="ctrlDownButtonLightsSet" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_3Ijao-WyEd-64JNDK1TKiQ" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scVariable name="ctrlFloorButtonLightsSet" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_tIzr4uA_Ed-78bCl9yYd-Q" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scVariable name="ctrlUpButtonLightsSet" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_pvUD0OEsEd-bh-7nDQnLgQ" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scVariable name="last_schedule" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_UtggcO5-Ed-dEtybZVK09Q" org.eventb.core.type="SCHEDULER_STRATEGY"/>
<org.eventb.core.scVariable name="last_stop" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_-7fiIPS-Ed-43_jmKUh78g" org.eventb.core.type="ℤ"/>
<org.eventb.core.scVariable name="request_served" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_mbfp0PluEd-1httaBm5m2g" org.eventb.core.type="BOOL"/>
<org.eventb.core.scVariable name="requests" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_8ov3UPk7Ed-WtNZH8d5nSA" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scVariable name="schedule" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_Utggce5-Ed-dEtybZVK09Q" org.eventb.core.type="SCHEDULER_STRATEGY"/>
<org.eventb.core.scVariable name="snsrCableEngine" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_aGwXgtq-Ed-L_e8_V4iXIg" org.eventb.core.type="CABLE_COMMAND"/>
<org.eventb.core.scVariable name="snsrDoorEngine" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_KgY80OAzEd-73py7lbE8bg" org.eventb.core.type="DOOR_COMMAND"/>
<org.eventb.core.scVariable name="snsrDoorPosition" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_KgY80eAzEd-73py7lbE8bg" org.eventb.core.type="DOOR_POSITION"/>
<org.eventb.core.scVariable name="snsrDownButtonsSet" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_3IjaoeWyEd-64JNDK1TKiQ" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scVariable name="snsrElevatorFloor" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_aGwXg9q-Ed-L_e8_V4iXIg" org.eventb.core.type="ℤ"/>
<org.eventb.core.scVariable name="snsrFloorButtonsSet" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_tIzr4OA_Ed-78bCl9yYd-Q" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scVariable name="snsrUpButtonsSet" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variable#_pvTcweEsEd-bh-7nDQnLgQ" org.eventb.core.type="ℙ(ℤ)"/>
<org.eventb.core.scVariant name="VAR0" org.eventb.core.expression="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet" org.eventb.core.label="VARIANT" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.variant#_028ScPk8Ed-hoNTGCqdYog"/>
<org.eventb.core.scEvent name="EVT0" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#'">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT0" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#'"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyElevatorFloor ≔ 0" org.eventb.core.label="act1_1" org.eventb.core.source="/ProvenLift/lift01_floors.bum|org.eventb.core.machineFile#lift01_floors|org.eventb.core.event#'|org.eventb.core.action#_9uErwNd9Ed-Dle0at0Xgqg"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="last_stop ≔ 0" org.eventb.core.label="act2_2" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#'|org.eventb.core.action#_1cMqQtd_Ed-Dle0at0Xgqg"/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="ctrlCableCommand ≔ CABLE_STOP" org.eventb.core.label="act2_1" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#'|org.eventb.core.action#_mweFUN0UEd-DHKwvWNa8WQ"/>
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="ctrlDoorCommand ≔ DOOR_STOP" org.eventb.core.label="act3_1" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#'|org.eventb.core.action#_HKimIdqzEd-7IuFxCL4SWw"/>
<org.eventb.core.scAction name="ACT4" org.eventb.core.assignment="PhyCableEngine ≔ CABLE_STOP" org.eventb.core.label="act4_1" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#'|org.eventb.core.action#_aGxlo9q-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT5" org.eventb.core.assignment="PhyElevatorBetweenTwoFloors ≔ FALSE" org.eventb.core.label="act4_3" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#'|org.eventb.core.action#_aGyMsdq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT6" org.eventb.core.assignment="snsrCableEngine ≔ CABLE_STOP" org.eventb.core.label="act4_4" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#'|org.eventb.core.action#_BGk6wNrCEd-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT7" org.eventb.core.assignment="snsrElevatorFloor ≔ 0" org.eventb.core.label="act4_5" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#'|org.eventb.core.action#_aGyMs9q-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT8" org.eventb.core.assignment="PhyDoorEngine ≔ DOOR_STOP" org.eventb.core.label="act5_1" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#'|org.eventb.core.action#_F6WecOA2Ed-73py7lbE8bg"/>
<org.eventb.core.scAction name="ACT9" org.eventb.core.assignment="PhyDoorPosition ≔ DOOR_CLOSED" org.eventb.core.label="act5_2" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#'|org.eventb.core.action#_F6WeceA2Ed-73py7lbE8bg"/>
<org.eventb.core.scAction name="ACT10" org.eventb.core.assignment="snsrDoorEngine ≔ DOOR_STOP" org.eventb.core.label="act5_3" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#'|org.eventb.core.action#_F6WecuA2Ed-73py7lbE8bg"/>
<org.eventb.core.scAction name="ACT11" org.eventb.core.assignment="snsrDoorPosition ≔ DOOR_CLOSED" org.eventb.core.label="act5_4" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#'|org.eventb.core.action#_F6Wec-A2Ed-73py7lbE8bg"/>
<org.eventb.core.scAction name="ACT12" org.eventb.core.assignment="PhyFloorButtonsSet ≔ (∅ ⦂ ℙ(ℤ))" org.eventb.core.label="act6_1" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#'|org.eventb.core.action#_tI06AeA_Ed-78bCl9yYd-Q"/>
<org.eventb.core.scAction name="ACT13" org.eventb.core.assignment="snsrFloorButtonsSet ≔ (∅ ⦂ ℙ(ℤ))" org.eventb.core.label="act6_2" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#'|org.eventb.core.action#_tI1hEOA_Ed-78bCl9yYd-Q"/>
<org.eventb.core.scAction name="ACT14" org.eventb.core.assignment="PhyFloorButtonLightsSet ≔ (∅ ⦂ ℙ(ℤ))" org.eventb.core.label="act6_3" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#'|org.eventb.core.action#_tI1hEeA_Ed-78bCl9yYd-Q"/>
<org.eventb.core.scAction name="ACT15" org.eventb.core.assignment="ctrlFloorButtonLightsSet ≔ (∅ ⦂ ℙ(ℤ))" org.eventb.core.label="act6_4" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#'|org.eventb.core.action#_tI1hEuA_Ed-78bCl9yYd-Q"/>
<org.eventb.core.scAction name="ACT16" org.eventb.core.assignment="PhyUpButtonsSet ≔ (∅ ⦂ ℙ(ℤ))" org.eventb.core.label="act7_1" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#'|org.eventb.core.action#_pvUq4uEsEd-bh-7nDQnLgQ"/>
<org.eventb.core.scAction name="ACT17" org.eventb.core.assignment="snsrUpButtonsSet ≔ (∅ ⦂ ℙ(ℤ))" org.eventb.core.label="act7_2" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#'|org.eventb.core.action#_pvUq4-EsEd-bh-7nDQnLgQ"/>
<org.eventb.core.scAction name="ACT18" org.eventb.core.assignment="PhyUpButtonLightsSet ≔ (∅ ⦂ ℙ(ℤ))" org.eventb.core.label="act7_3" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#'|org.eventb.core.action#_pvUq5OEsEd-bh-7nDQnLgQ"/>
<org.eventb.core.scAction name="ACT19" org.eventb.core.assignment="ctrlUpButtonLightsSet ≔ (∅ ⦂ ℙ(ℤ))" org.eventb.core.label="act7_4" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#'|org.eventb.core.action#_pvVR8OEsEd-bh-7nDQnLgQ"/>
<org.eventb.core.scAction name="ACT20" org.eventb.core.assignment="PhyDownButtonsSet ≔ (∅ ⦂ ℙ(ℤ))" org.eventb.core.label="act8_1" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#'|org.eventb.core.action#_3IkowOWyEd-64JNDK1TKiQ"/>
<org.eventb.core.scAction name="ACT21" org.eventb.core.assignment="snsrDownButtonsSet ≔ (∅ ⦂ ℙ(ℤ))" org.eventb.core.label="act8_2" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#'|org.eventb.core.action#_3IkoweWyEd-64JNDK1TKiQ"/>
<org.eventb.core.scAction name="ACT22" org.eventb.core.assignment="PhyDownButtonLightsSet ≔ (∅ ⦂ ℙ(ℤ))" org.eventb.core.label="act8_3" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#'|org.eventb.core.action#_3IkowuWyEd-64JNDK1TKiQ"/>
<org.eventb.core.scAction name="ACT23" org.eventb.core.assignment="ctrlDownButtonLightsSet ≔ (∅ ⦂ ℙ(ℤ))" org.eventb.core.label="act8_4" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#'|org.eventb.core.action#_3Ikow-WyEd-64JNDK1TKiQ"/>
<org.eventb.core.scAction name="ACT24" org.eventb.core.assignment="requests ≔ (∅ ⦂ ℙ(ℤ))" org.eventb.core.label="act8_5" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#'|org.eventb.core.action#_yPC4kPk7Ed-WtNZH8d5nSA"/>
<org.eventb.core.scAction name="ACT25" org.eventb.core.assignment="last_schedule ≔ SCHEDULER_UP" org.eventb.core.label="act9_2" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#'|org.eventb.core.action#_Uthuke5-Ed-dEtybZVK09Q"/>
<org.eventb.core.scAction name="ACT26" org.eventb.core.assignment="schedule ≔ SCHEDULER_WAIT" org.eventb.core.label="act9_1" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#'|org.eventb.core.action#_Uthuku5-Ed-dEtybZVK09Q"/>
<org.eventb.core.scAction name="ACT27" org.eventb.core.assignment="request_served ≔ TRUE" org.eventb.core.label="act9_3" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#'|org.eventb.core.action#_q3de0fluEd-1httaBm5m2g"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT1" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_PRESSES_DOWN_BUTTON" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_3IkoxOWyEd-64JNDK1TKiQ">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT1" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_3IkoxOWyEd-64JNDK1TKiQ|org.eventb.core.refinesEvent#_mbfp0fluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd8_1" org.eventb.core.predicate="x∈1 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3IkoxOWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3IlP0eWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd8_2" org.eventb.core.predicate="x∉PhyDownButtonsSet" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3IkoxOWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3IlP0uWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyDownButtonsSet ≔ PhyDownButtonsSet∪{x}" org.eventb.core.label="act8_1" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3IkoxOWyEd-64JNDK1TKiQ|org.eventb.core.action#_3IlP0-WyEd-64JNDK1TKiQ"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="snsrDownButtonsSet ≔ snsrDownButtonsSet∪{x}" org.eventb.core.label="act8_2" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3IkoxOWyEd-64JNDK1TKiQ|org.eventb.core.action#_3IlP1OWyEd-64JNDK1TKiQ"/>
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3IkoxOWyEd-64JNDK1TKiQ|org.eventb.core.parameter#_3IlP0OWyEd-64JNDK1TKiQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT2" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_DOWN_BUTTON" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_mbgQ4PluEd-1httaBm5m2g">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT2" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_mbgQ4PluEd-1httaBm5m2g|org.eventb.core.refinesEvent#_mbgQ4fluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd8_1" org.eventb.core.predicate="x∈1 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_zh0nsPk-Ed-hoNTGCqdYog|org.eventb.core.guard#_3Il24eWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd8_2" org.eventb.core.predicate="x∈PhyDownButtonsSet" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_zh0nsPk-Ed-hoNTGCqdYog|org.eventb.core.guard#_3Il24uWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyDownButtonsSet ≔ PhyDownButtonsSet ∖ {x}" org.eventb.core.label="act8_1" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_zh0nsPk-Ed-hoNTGCqdYog|org.eventb.core.action#_3Il24-WyEd-64JNDK1TKiQ"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="snsrDownButtonsSet ≔ snsrDownButtonsSet ∖ {x}" org.eventb.core.label="act8_2" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_zh0nsPk-Ed-hoNTGCqdYog|org.eventb.core.action#_3Il25OWyEd-64JNDK1TKiQ"/>
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_zh0nsPk-Ed-hoNTGCqdYog|org.eventb.core.parameter#_3Il24OWyEd-64JNDK1TKiQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT3" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="TURNS_ON_DOWN_BUTTON_LIGHT" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_3Il25eWyEd-64JNDK1TKiQ">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT3" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_3Il25eWyEd-64JNDK1TKiQ|org.eventb.core.refinesEvent#_mbgQ4vluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd8_1" org.eventb.core.predicate="x∈1 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3Il25eWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3Imd8eWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd8_2" org.eventb.core.predicate="x∈ctrlDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3Il25eWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3Imd8uWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd8_3" org.eventb.core.predicate="x∉PhyDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3Il25eWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3Imd8-WyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyDownButtonLightsSet ≔ PhyDownButtonLightsSet∪{x}" org.eventb.core.label="act8_1" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3Il25eWyEd-64JNDK1TKiQ|org.eventb.core.action#_3Imd9OWyEd-64JNDK1TKiQ"/>
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3Il25eWyEd-64JNDK1TKiQ|org.eventb.core.parameter#_3Imd8OWyEd-64JNDK1TKiQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT4" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="TURNS_OFF_DOWN_BUTTON_LIGHT" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_3Imd9eWyEd-64JNDK1TKiQ">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT4" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_3Imd9eWyEd-64JNDK1TKiQ|org.eventb.core.refinesEvent#_mbgQ4_luEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd8_1" org.eventb.core.predicate="x∈1 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3Imd9eWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3InFAeWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd8_2" org.eventb.core.predicate="x∉ctrlDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3Imd9eWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3InFAuWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd8_3" org.eventb.core.predicate="x∈PhyDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3Imd9eWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3InsEOWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyDownButtonLightsSet ≔ PhyDownButtonLightsSet ∖ {x}" org.eventb.core.label="act8_1" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3Imd9eWyEd-64JNDK1TKiQ|org.eventb.core.action#_3InsEeWyEd-64JNDK1TKiQ"/>
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3Imd9eWyEd-64JNDK1TKiQ|org.eventb.core.parameter#_3InFAOWyEd-64JNDK1TKiQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT5" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="turn_down_button_light_on" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_3InsEuWyEd-64JNDK1TKiQ">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT5" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_3InsEuWyEd-64JNDK1TKiQ|org.eventb.core.refinesEvent#_mbgQ5PluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd8_1" org.eventb.core.predicate="x∈1 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3InsEuWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3InsFOWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd8_2" org.eventb.core.predicate="x∈snsrDownButtonsSet" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3InsEuWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3InsFeWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd8_3" org.eventb.core.predicate="x∉ctrlDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3InsEuWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3IoTIOWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd8_4" org.eventb.core.predicate="¬(snsrElevatorFloor=x∧snsrDoorPosition=DOOR_OPENED)" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3InsEuWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3IoTIeWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="ctrlDownButtonLightsSet ≔ ctrlDownButtonLightsSet∪{x}" org.eventb.core.label="act8_1" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3InsEuWyEd-64JNDK1TKiQ|org.eventb.core.action#_3IoTIuWyEd-64JNDK1TKiQ"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="requests ≔ requests∪{x}" org.eventb.core.label="act8_2" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3InsEuWyEd-64JNDK1TKiQ|org.eventb.core.action#_yPFU0Pk7Ed-WtNZH8d5nSA"/>
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3InsEuWyEd-64JNDK1TKiQ|org.eventb.core.parameter#_3InsE-WyEd-64JNDK1TKiQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT6" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="turn_down_button_light_off" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_3IoTI-WyEd-64JNDK1TKiQ">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT6" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_3IoTI-WyEd-64JNDK1TKiQ|org.eventb.core.refinesEvent#_mbg38PluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd8_1" org.eventb.core.predicate="snsrDoorPosition=DOOR_OPENED" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3IoTI-WyEd-64JNDK1TKiQ|org.eventb.core.guard#_3IoTJeWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd8_2" org.eventb.core.predicate="snsrElevatorFloor∈ctrlDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3IoTI-WyEd-64JNDK1TKiQ|org.eventb.core.guard#_3Io6MOWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd8_3" org.eventb.core.predicate="snsrElevatorFloor∉snsrDownButtonsSet" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3IoTI-WyEd-64JNDK1TKiQ|org.eventb.core.guard#_gHXcoPfqEd-vgams47i3xA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd9_1" org.eventb.core.predicate="last_schedule=SCHEDULER_UP⇒snsrElevatorFloor+1 ‥ LAST_FLOOR∩(ctrlFloorButtonLightsSet∪ctrlUpButtonLightsSet∪ctrlDownButtonLightsSet)=(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_3IoTI-WyEd-64JNDK1TKiQ|org.eventb.core.guard#_Uti8su5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="ctrlDownButtonLightsSet ≔ ctrlDownButtonLightsSet ∖ {snsrElevatorFloor}" org.eventb.core.label="act8_1" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3IoTI-WyEd-64JNDK1TKiQ|org.eventb.core.action#_3Io6MeWyEd-64JNDK1TKiQ"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="requests ≔ ctrlFloorButtonLightsSet∪ctrlUpButtonLightsSet∪(ctrlDownButtonLightsSet ∖ {snsrElevatorFloor})" org.eventb.core.label="act8_2" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_3IoTI-WyEd-64JNDK1TKiQ|org.eventb.core.action#_yPFU0fk7Ed-WtNZH8d5nSA"/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="request_served ≔ TRUE" org.eventb.core.label="act9_1" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_3IoTI-WyEd-64JNDK1TKiQ|org.eventb.core.action#_q3es8_luEd-1httaBm5m2g"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT7" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_PRESSES_UP_BUTTON" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_pvVR8eEsEd-bh-7nDQnLgQ">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT7" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_pvVR8eEsEd-bh-7nDQnLgQ|org.eventb.core.refinesEvent#_mbg38fluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd7_1" org.eventb.core.predicate="x∈0 ‥ (LAST_FLOOR − 1)" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvVR8eEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvVR8-EsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd7_2" org.eventb.core.predicate="x∉PhyUpButtonsSet" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvVR8eEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvVR9OEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyUpButtonsSet ≔ PhyUpButtonsSet∪{x}" org.eventb.core.label="act7_1" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvVR8eEsEd-bh-7nDQnLgQ|org.eventb.core.action#_pvVR9eEsEd-bh-7nDQnLgQ"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="snsrUpButtonsSet ≔ snsrUpButtonsSet∪{x}" org.eventb.core.label="act7_2" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvVR8eEsEd-bh-7nDQnLgQ|org.eventb.core.action#_pvVR9uEsEd-bh-7nDQnLgQ"/>
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvVR8eEsEd-bh-7nDQnLgQ|org.eventb.core.parameter#_pvVR8uEsEd-bh-7nDQnLgQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT8" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_UP_BUTTON" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_3Io6M-WyEd-64JNDK1TKiQ">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT8" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_3Io6M-WyEd-64JNDK1TKiQ|org.eventb.core.refinesEvent#_mbg38vluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd7_1" org.eventb.core.predicate="x∈0 ‥ (LAST_FLOOR − 1)" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvV5AOEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvV5AuEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd7_2" org.eventb.core.predicate="x∈PhyUpButtonsSet" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvV5AOEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvV5A-EsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyUpButtonsSet ≔ PhyUpButtonsSet ∖ {x}" org.eventb.core.label="act7_1" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvV5AOEsEd-bh-7nDQnLgQ|org.eventb.core.action#_pvV5BOEsEd-bh-7nDQnLgQ"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="snsrUpButtonsSet ≔ snsrUpButtonsSet ∖ {x}" org.eventb.core.label="act7_2" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvV5AOEsEd-bh-7nDQnLgQ|org.eventb.core.action#_pvV5BeEsEd-bh-7nDQnLgQ"/>
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvV5AOEsEd-bh-7nDQnLgQ|org.eventb.core.parameter#_pvV5AeEsEd-bh-7nDQnLgQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT9" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="TURNS_ON_UP_BUTTON_LIGHT" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_pvV5BuEsEd-bh-7nDQnLgQ">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT9" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_pvV5BuEsEd-bh-7nDQnLgQ|org.eventb.core.refinesEvent#_mbhfAPluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd7_1" org.eventb.core.predicate="x∈0 ‥ (LAST_FLOOR − 1)" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvV5BuEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvWgEeEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd7_2" org.eventb.core.predicate="x∈ctrlUpButtonLightsSet" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvV5BuEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvWgEuEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd7_3" org.eventb.core.predicate="x∉PhyUpButtonLightsSet" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvV5BuEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvWgE-EsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyUpButtonLightsSet ≔ PhyUpButtonLightsSet∪{x}" org.eventb.core.label="act7_1" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvV5BuEsEd-bh-7nDQnLgQ|org.eventb.core.action#_pvWgFOEsEd-bh-7nDQnLgQ"/>
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvV5BuEsEd-bh-7nDQnLgQ|org.eventb.core.parameter#_pvWgEOEsEd-bh-7nDQnLgQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT10" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="TURNS_OFF_UP_BUTTON_LIGHT" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_pvWgFeEsEd-bh-7nDQnLgQ">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT10" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_pvWgFeEsEd-bh-7nDQnLgQ|org.eventb.core.refinesEvent#_mbhfAfluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd7_1" org.eventb.core.predicate="x∈0 ‥ (LAST_FLOOR − 1)" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvWgFeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvXHIeEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd7_2" org.eventb.core.predicate="x∉ctrlUpButtonLightsSet" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvWgFeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvXHIuEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd7_3" org.eventb.core.predicate="x∈PhyUpButtonLightsSet" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvWgFeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvXHI-EsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyUpButtonLightsSet ≔ PhyUpButtonLightsSet ∖ {x}" org.eventb.core.label="act7_1" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvWgFeEsEd-bh-7nDQnLgQ|org.eventb.core.action#_pvXHJOEsEd-bh-7nDQnLgQ"/>
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvWgFeEsEd-bh-7nDQnLgQ|org.eventb.core.parameter#_pvXHIOEsEd-bh-7nDQnLgQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT11" org.eventb.core.accurate="true" org.eventb.core.convergence="1" org.eventb.core.extended="true" org.eventb.core.label="turn_up_button_light_on" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_pvXHJeEsEd-bh-7nDQnLgQ">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT11" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_pvXHJeEsEd-bh-7nDQnLgQ|org.eventb.core.refinesEvent#_mbhfAvluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd7_1" org.eventb.core.predicate="x∈0 ‥ (LAST_FLOOR − 1)" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvXHJeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvXuMOEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd7_2" org.eventb.core.predicate="x∈snsrUpButtonsSet" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvXHJeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvXuMeEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd7_3" org.eventb.core.predicate="x∉ctrlUpButtonLightsSet" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvXHJeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvXuMuEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd7_4" org.eventb.core.predicate="¬(snsrElevatorFloor=x∧snsrDoorPosition=DOOR_OPENED)" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvXHJeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvXuM-EsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="ctrlUpButtonLightsSet ≔ ctrlUpButtonLightsSet∪{x}" org.eventb.core.label="act7_1" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvXHJeEsEd-bh-7nDQnLgQ|org.eventb.core.action#_pvXuNOEsEd-bh-7nDQnLgQ"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="requests ≔ requests∪{x}" org.eventb.core.label="act8_1" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_pvXHJeEsEd-bh-7nDQnLgQ|org.eventb.core.action#_yPGi8vk7Ed-WtNZH8d5nSA"/>
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvXHJeEsEd-bh-7nDQnLgQ|org.eventb.core.parameter#_pvXHJuEsEd-bh-7nDQnLgQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT12" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="turn_up_button_light_off" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_pvXuNeEsEd-bh-7nDQnLgQ">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT12" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_pvXuNeEsEd-bh-7nDQnLgQ|org.eventb.core.refinesEvent#_mbhfA_luEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd7_1" org.eventb.core.predicate="snsrDoorPosition=DOOR_OPENED" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvXuNeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvYVQOEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd7_2" org.eventb.core.predicate="snsrElevatorFloor∈ctrlUpButtonLightsSet" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvXuNeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvYVQeEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd7_3" org.eventb.core.predicate="snsrElevatorFloor∉snsrUpButtonsSet" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvXuNeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_bq87sPfqEd-vgams47i3xA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd9_1" org.eventb.core.predicate="last_schedule=SCHEDULER_DOWN⇒0 ‥ (snsrElevatorFloor − 1)∩(ctrlFloorButtonLightsSet∪ctrlUpButtonLightsSet∪ctrlDownButtonLightsSet)=(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_pvXuNeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_UtkK0u5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="ctrlUpButtonLightsSet ≔ ctrlUpButtonLightsSet ∖ {snsrElevatorFloor}" org.eventb.core.label="act7_1" org.eventb.core.source="/ProvenLift/lift07_up_buttons.bum|org.eventb.core.machineFile#lift07_up_buttons|org.eventb.core.event#_pvXuNeEsEd-bh-7nDQnLgQ|org.eventb.core.action#_pvYVQuEsEd-bh-7nDQnLgQ"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="requests ≔ ctrlFloorButtonLightsSet∪(ctrlUpButtonLightsSet ∖ {snsrElevatorFloor})∪ctrlDownButtonLightsSet" org.eventb.core.label="act8_1" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_pvXuNeEsEd-bh-7nDQnLgQ|org.eventb.core.action#_yPGi9Pk7Ed-WtNZH8d5nSA"/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="request_served ≔ TRUE" org.eventb.core.label="act9_1" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_pvXuNeEsEd-bh-7nDQnLgQ|org.eventb.core.action#_q3f7E_luEd-1httaBm5m2g"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT13" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_PRESSES_FLOOR_BUTTON" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_tI1hE-A_Ed-78bCl9yYd-Q">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT13" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_tI1hE-A_Ed-78bCl9yYd-Q|org.eventb.core.refinesEvent#_mbiGEPluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd6_1" org.eventb.core.predicate="x∈0 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI1hE-A_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI1hFeA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd6_2" org.eventb.core.predicate="x∉PhyFloorButtonsSet" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI1hE-A_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI2IIOA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyFloorButtonsSet ≔ PhyFloorButtonsSet∪{x}" org.eventb.core.label="act6_1" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI1hE-A_Ed-78bCl9yYd-Q|org.eventb.core.action#_tI2IIeA_Ed-78bCl9yYd-Q"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="snsrFloorButtonsSet ≔ snsrFloorButtonsSet∪{x}" org.eventb.core.label="act6_2" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI1hE-A_Ed-78bCl9yYd-Q|org.eventb.core.action#_tI2IIuA_Ed-78bCl9yYd-Q"/>
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI1hE-A_Ed-78bCl9yYd-Q|org.eventb.core.parameter#_tI1hFOA_Ed-78bCl9yYd-Q" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT14" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_FLOOR_BUTTON" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_mbiGEfluEd-1httaBm5m2g">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT14" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_mbiGEfluEd-1httaBm5m2g|org.eventb.core.refinesEvent#_mbiGEvluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd6_1" org.eventb.core.predicate="x∈0 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_6NwzMPfpEd-vgams47i3xA|org.eventb.core.guard#_tI2vMeA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd6_2" org.eventb.core.predicate="x∈PhyFloorButtonsSet" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_6NwzMPfpEd-vgams47i3xA|org.eventb.core.guard#_tI2vMuA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyFloorButtonsSet ≔ PhyFloorButtonsSet ∖ {x}" org.eventb.core.label="act6_1" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_6NwzMPfpEd-vgams47i3xA|org.eventb.core.action#_tI2vM-A_Ed-78bCl9yYd-Q"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="snsrFloorButtonsSet ≔ snsrFloorButtonsSet ∖ {x}" org.eventb.core.label="act6_2" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_6NwzMPfpEd-vgams47i3xA|org.eventb.core.action#_tI2vNOA_Ed-78bCl9yYd-Q"/>
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_6NwzMPfpEd-vgams47i3xA|org.eventb.core.parameter#_tI2vMOA_Ed-78bCl9yYd-Q" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT15" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="TURNS_ON_FLOOR_BUTTON_LIGHT" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_tI2vNeA_Ed-78bCl9yYd-Q">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT15" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_tI2vNeA_Ed-78bCl9yYd-Q|org.eventb.core.refinesEvent#_mbiGE_luEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd6_1" org.eventb.core.predicate="x∈0 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI2vNeA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI3WQeA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd6_2" org.eventb.core.predicate="x∈ctrlFloorButtonLightsSet" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI2vNeA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI3WQuA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd6_3" org.eventb.core.predicate="x∉PhyFloorButtonLightsSet" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI2vNeA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI3WQ-A_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyFloorButtonLightsSet ≔ PhyFloorButtonLightsSet∪{x}" org.eventb.core.label="act6_1" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI2vNeA_Ed-78bCl9yYd-Q|org.eventb.core.action#_tI39UOA_Ed-78bCl9yYd-Q"/>
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI2vNeA_Ed-78bCl9yYd-Q|org.eventb.core.parameter#_tI3WQOA_Ed-78bCl9yYd-Q" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT16" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="TURNS_OFF_FLOOR_BUTTON_LIGHT" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_pvY8UuEsEd-bh-7nDQnLgQ">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT16" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_pvY8UuEsEd-bh-7nDQnLgQ|org.eventb.core.refinesEvent#_mbiGFPluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd6_1" org.eventb.core.predicate="x∈0 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI39UeA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI39U-A_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd6_2" org.eventb.core.predicate="x∉ctrlFloorButtonLightsSet" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI39UeA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI39VOA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd6_3" org.eventb.core.predicate="x∈PhyFloorButtonLightsSet" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI39UeA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI4kYOA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyFloorButtonLightsSet ≔ PhyFloorButtonLightsSet ∖ {x}" org.eventb.core.label="act6_1" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI39UeA_Ed-78bCl9yYd-Q|org.eventb.core.action#_tI4kYeA_Ed-78bCl9yYd-Q"/>
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI39UeA_Ed-78bCl9yYd-Q|org.eventb.core.parameter#_tI39UuA_Ed-78bCl9yYd-Q" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT17" org.eventb.core.accurate="true" org.eventb.core.convergence="1" org.eventb.core.extended="true" org.eventb.core.label="turn_floor_button_light_on" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_tI4kYuA_Ed-78bCl9yYd-Q">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT17" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_tI4kYuA_Ed-78bCl9yYd-Q|org.eventb.core.refinesEvent#_mbitIPluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd6_1" org.eventb.core.predicate="x∈0 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI4kYuA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI4kZOA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd6_2" org.eventb.core.predicate="x∈snsrFloorButtonsSet" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI4kYuA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI5LcOA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd6_3" org.eventb.core.predicate="x∉ctrlFloorButtonLightsSet" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI4kYuA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI5LceA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd6_4" org.eventb.core.predicate="¬(snsrElevatorFloor=x∧snsrDoorPosition=DOOR_OPENED)" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI4kYuA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI5LcuA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="ctrlFloorButtonLightsSet ≔ ctrlFloorButtonLightsSet∪{x}" org.eventb.core.label="act6_1" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI4kYuA_Ed-78bCl9yYd-Q|org.eventb.core.action#_tI5Lc-A_Ed-78bCl9yYd-Q"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="requests ≔ requests∪{x}" org.eventb.core.label="act8_1" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_tI4kYuA_Ed-78bCl9yYd-Q|org.eventb.core.action#_yPHxEvk7Ed-WtNZH8d5nSA"/>
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI4kYuA_Ed-78bCl9yYd-Q|org.eventb.core.parameter#_tI4kY-A_Ed-78bCl9yYd-Q" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT18" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="turn_floor_button_light_off" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_tI5ygOA_Ed-78bCl9yYd-Q">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT18" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_tI5ygOA_Ed-78bCl9yYd-Q|org.eventb.core.refinesEvent#_mbitIfluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd6_1" org.eventb.core.predicate="snsrDoorPosition=DOOR_OPENED" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI5ygOA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI5ygeA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd6_2" org.eventb.core.predicate="snsrElevatorFloor∈ctrlFloorButtonLightsSet" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI5ygOA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI5yguA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd6_3" org.eventb.core.predicate="snsrElevatorFloor∉snsrFloorButtonsSet" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI5ygOA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_6NzPcPfpEd-vgams47i3xA" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="ctrlFloorButtonLightsSet ≔ ctrlFloorButtonLightsSet ∖ {snsrElevatorFloor}" org.eventb.core.label="act6_1" org.eventb.core.source="/ProvenLift/lift06_buttons.bum|org.eventb.core.machineFile#lift06_buttons|org.eventb.core.event#_tI5ygOA_Ed-78bCl9yYd-Q|org.eventb.core.action#_J5OP8O6pEd-AmKUrnT9Ziw"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="requests ≔ (ctrlFloorButtonLightsSet ∖ {snsrElevatorFloor})∪ctrlUpButtonLightsSet∪ctrlDownButtonLightsSet" org.eventb.core.label="act8_1" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_tI5ygOA_Ed-78bCl9yYd-Q|org.eventb.core.action#_yPHxFPk7Ed-WtNZH8d5nSA"/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="request_served ≔ TRUE" org.eventb.core.label="act9_1" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_tI5ygOA_Ed-78bCl9yYd-Q|org.eventb.core.action#_q3hJM_luEd-1httaBm5m2g"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT19" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="DOOR_OPENS_WHEN_CLOSED" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_KgayBOAzEd-73py7lbE8bg">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT19" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_KgayBOAzEd-73py7lbE8bg|org.eventb.core.refinesEvent#_mbitIvluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="PhyDoorPosition=DOOR_CLOSED" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6WedOA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6XFgOA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="ctrlDoorCommand=DOOR_OPEN" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6WedOA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6XFgeA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyDoorPosition ≔ DOOR_HALF" org.eventb.core.label="act1" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6WedOA2Ed-73py7lbE8bg|org.eventb.core.action#_F6XFguA2Ed-73py7lbE8bg"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="PhyDoorEngine ≔ DOOR_OPEN" org.eventb.core.label="act2" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6WedOA2Ed-73py7lbE8bg|org.eventb.core.action#_F6XFg-A2Ed-73py7lbE8bg"/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="snsrDoorPosition ≔ DOOR_HALF" org.eventb.core.label="act3" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6WedOA2Ed-73py7lbE8bg|org.eventb.core.action#_F6XFhOA2Ed-73py7lbE8bg"/>
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="snsrDoorEngine ≔ DOOR_OPEN" org.eventb.core.label="act4" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6WedOA2Ed-73py7lbE8bg|org.eventb.core.action#_F6XFheA2Ed-73py7lbE8bg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT20" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="DOOR_OPENS_WHEN_HALF" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_KgcAIOAzEd-73py7lbE8bg">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT20" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_KgcAIOAzEd-73py7lbE8bg|org.eventb.core.refinesEvent#_mbjUMPluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="PhyDoorPosition=DOOR_HALF" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6XskOA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6XskeA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="ctrlDoorCommand=DOOR_OPEN" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6XskOA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6XskuA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyDoorPosition ≔ DOOR_OPENED" org.eventb.core.label="act1" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6XskOA2Ed-73py7lbE8bg|org.eventb.core.action#_F6Xsk-A2Ed-73py7lbE8bg"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="PhyDoorEngine ≔ DOOR_OPEN" org.eventb.core.label="act2" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6XskOA2Ed-73py7lbE8bg|org.eventb.core.action#_F6XslOA2Ed-73py7lbE8bg"/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="snsrDoorPosition ≔ DOOR_OPENED" org.eventb.core.label="act3" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6XskOA2Ed-73py7lbE8bg|org.eventb.core.action#_F6YToOA2Ed-73py7lbE8bg"/>
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="snsrDoorEngine ≔ DOOR_OPEN" org.eventb.core.label="act4" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6XskOA2Ed-73py7lbE8bg|org.eventb.core.action#_F6YToeA2Ed-73py7lbE8bg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT21" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="DOOR_CLOSES_WHEN_OPENED" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_KgcnM-AzEd-73py7lbE8bg">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT21" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_KgcnM-AzEd-73py7lbE8bg|org.eventb.core.refinesEvent#_mbjUMfluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="PhyDoorPosition=DOOR_OPENED" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6YTouA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6YTo-A2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="ctrlDoorCommand=DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6YTouA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6YTpOA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyDoorPosition ≔ DOOR_HALF" org.eventb.core.label="act1" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6YTouA2Ed-73py7lbE8bg|org.eventb.core.action#_F6Y6sOA2Ed-73py7lbE8bg"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="PhyDoorEngine ≔ DOOR_CLOSE" org.eventb.core.label="act2" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6YTouA2Ed-73py7lbE8bg|org.eventb.core.action#_F6Y6seA2Ed-73py7lbE8bg"/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="snsrDoorPosition ≔ DOOR_HALF" org.eventb.core.label="act3" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6YTouA2Ed-73py7lbE8bg|org.eventb.core.action#_F6Y6suA2Ed-73py7lbE8bg"/>
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="snsrDoorEngine ≔ DOOR_CLOSE" org.eventb.core.label="act4" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6YTouA2Ed-73py7lbE8bg|org.eventb.core.action#_F6Y6s-A2Ed-73py7lbE8bg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT22" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="DOOR_CLOSES_WHEN_HALF" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_KgdOReAzEd-73py7lbE8bg">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT22" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_KgdOReAzEd-73py7lbE8bg|org.eventb.core.refinesEvent#_mbjUMvluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="PhyDoorPosition=DOOR_HALF" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6Y6tOA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6Y6teA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="ctrlDoorCommand=DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6Y6tOA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6ZhwOA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyDoorPosition ≔ DOOR_CLOSED" org.eventb.core.label="act1" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6Y6tOA2Ed-73py7lbE8bg|org.eventb.core.action#_F6ZhweA2Ed-73py7lbE8bg"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="PhyDoorEngine ≔ DOOR_CLOSE" org.eventb.core.label="act2" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6Y6tOA2Ed-73py7lbE8bg|org.eventb.core.action#_F6ZhwuA2Ed-73py7lbE8bg"/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="snsrDoorPosition ≔ DOOR_CLOSED" org.eventb.core.label="act3" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6Y6tOA2Ed-73py7lbE8bg|org.eventb.core.action#_F6Zhw-A2Ed-73py7lbE8bg"/>
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="snsrDoorEngine ≔ DOOR_CLOSE" org.eventb.core.label="act4" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6Y6tOA2Ed-73py7lbE8bg|org.eventb.core.action#_F6ZhxOA2Ed-73py7lbE8bg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT23" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="DOOR_CLOSES_WHEN_CLOSED" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_KgecYeAzEd-73py7lbE8bg">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT23" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_KgecYeAzEd-73py7lbE8bg|org.eventb.core.refinesEvent#_mbj7QPluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="PhyDoorPosition=DOOR_CLOSED" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6ZhxeA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6aI0OA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="ctrlDoorCommand=DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6ZhxeA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6aI0eA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd3" org.eventb.core.predicate="PhyDoorEngine≠DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6ZhxeA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6aI0uA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyDoorEngine ≔ DOOR_CLOSE" org.eventb.core.label="act1" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6ZhxeA2Ed-73py7lbE8bg|org.eventb.core.action#_F6aI0-A2Ed-73py7lbE8bg"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="snsrDoorEngine ≔ DOOR_CLOSE" org.eventb.core.label="act2" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6ZhxeA2Ed-73py7lbE8bg|org.eventb.core.action#_F6aI1OA2Ed-73py7lbE8bg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT24" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="STOP_DOOR_ENGINE" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_KgfDcuAzEd-73py7lbE8bg">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT24" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_KgfDcuAzEd-73py7lbE8bg|org.eventb.core.refinesEvent#_mbj7QfluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="PhyDoorEngine≠DOOR_STOP" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6aI1eA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6av4OA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="ctrlDoorCommand=DOOR_STOP" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6aI1eA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6av4eA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyDoorEngine ≔ DOOR_STOP" org.eventb.core.label="act1" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6aI1eA2Ed-73py7lbE8bg|org.eventb.core.action#_F6av4uA2Ed-73py7lbE8bg"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="snsrDoorEngine ≔ DOOR_STOP" org.eventb.core.label="act2" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_F6aI1eA2Ed-73py7lbE8bg|org.eventb.core.action#_F6av4-A2Ed-73py7lbE8bg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT25" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_UP" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_mbj7QvluEd-1httaBm5m2g">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT25" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_mbj7QvluEd-1httaBm5m2g|org.eventb.core.refinesEvent#_mbj7Q_luEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd4_1" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=FALSE" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMx7cPeyEd-p8t79IbuE0Q|org.eventb.core.guard#_aGyMttq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd4_2" org.eventb.core.predicate="PhyElevatorFloor≠LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMx7cPeyEd-p8t79IbuE0Q|org.eventb.core.guard#_aGyzwNq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd4_3" org.eventb.core.predicate="ctrlCableCommand=CABLE_WIND" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMx7cPeyEd-p8t79IbuE0Q|org.eventb.core.guard#_aGyzwdq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyElevatorBetweenTwoFloors ≔ TRUE" org.eventb.core.label="act4_1" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMx7cPeyEd-p8t79IbuE0Q|org.eventb.core.action#_aGyzwtq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="PhyCableEngine ≔ CABLE_WIND" org.eventb.core.label="act4_2" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMx7cPeyEd-p8t79IbuE0Q|org.eventb.core.action#_aGyzw9q-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="snsrElevatorFloor ≔ −1" org.eventb.core.label="act4_3" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMx7cPeyEd-p8t79IbuE0Q|org.eventb.core.action#_aGyzxNq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="snsrCableEngine ≔ CABLE_WIND" org.eventb.core.label="act4_4" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMx7cPeyEd-p8t79IbuE0Q|org.eventb.core.action#_aGyzxdq-Ed-L_e8_V4iXIg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT26" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_UP" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_mbj7RPluEd-1httaBm5m2g">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT26" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_mbj7RPluEd-1httaBm5m2g|org.eventb.core.refinesEvent#_mbj7RfluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd4_1" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=TRUE" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMyigPeyEd-p8t79IbuE0Q|org.eventb.core.guard#_aGza0dq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd4_2" org.eventb.core.predicate="ctrlCableCommand=CABLE_WIND" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMyigPeyEd-p8t79IbuE0Q|org.eventb.core.guard#_aGza0tq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyElevatorBetweenTwoFloors ≔ FALSE" org.eventb.core.label="act4_1" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMyigPeyEd-p8t79IbuE0Q|org.eventb.core.action#_aGza09q-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="PhyElevatorFloor ≔ PhyElevatorFloor+1" org.eventb.core.label="act4_2" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMyigPeyEd-p8t79IbuE0Q|org.eventb.core.action#_aGza1Nq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="PhyCableEngine ≔ CABLE_WIND" org.eventb.core.label="act4_3" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMyigPeyEd-p8t79IbuE0Q|org.eventb.core.action#_aGza1dq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="snsrElevatorFloor ≔ PhyElevatorFloor+1" org.eventb.core.label="act4_4" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMyigPeyEd-p8t79IbuE0Q|org.eventb.core.action#_aG0B4Nq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT4" org.eventb.core.assignment="snsrCableEngine ≔ CABLE_WIND" org.eventb.core.label="act4_5" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMyigPeyEd-p8t79IbuE0Q|org.eventb.core.action#_aG0B4dq-Ed-L_e8_V4iXIg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT27" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_DOWN" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_mbkiUPluEd-1httaBm5m2g">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT27" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_mbkiUPluEd-1httaBm5m2g|org.eventb.core.refinesEvent#_mbkiUfluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd4_1" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=FALSE" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMzJkPeyEd-p8t79IbuE0Q|org.eventb.core.guard#_aG0B49q-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd4_2" org.eventb.core.predicate="PhyElevatorFloor≠0" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMzJkPeyEd-p8t79IbuE0Q|org.eventb.core.guard#_aG0B5Nq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd4_3" org.eventb.core.predicate="ctrlCableCommand=CABLE_UNWIND" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMzJkPeyEd-p8t79IbuE0Q|org.eventb.core.guard#_aG0B5dq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyElevatorBetweenTwoFloors ≔ TRUE" org.eventb.core.label="act4_1" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMzJkPeyEd-p8t79IbuE0Q|org.eventb.core.action#_aG0o8Nq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="PhyElevatorFloor ≔ PhyElevatorFloor − 1" org.eventb.core.label="act4_2" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMzJkPeyEd-p8t79IbuE0Q|org.eventb.core.action#_aG0o8dq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="PhyCableEngine ≔ CABLE_UNWIND" org.eventb.core.label="act4_3" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMzJkPeyEd-p8t79IbuE0Q|org.eventb.core.action#_aG0o8tq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="snsrElevatorFloor ≔ −1" org.eventb.core.label="act4_4" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMzJkPeyEd-p8t79IbuE0Q|org.eventb.core.action#_aG0o89q-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT4" org.eventb.core.assignment="snsrCableEngine ≔ CABLE_UNWIND" org.eventb.core.label="act4_5" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMzJkPeyEd-p8t79IbuE0Q|org.eventb.core.action#_aG0o9Nq-Ed-L_e8_V4iXIg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT28" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_DOWN" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_mbkiUvluEd-1httaBm5m2g">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT28" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_mbkiUvluEd-1httaBm5m2g|org.eventb.core.refinesEvent#_mbkiU_luEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd4_1" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=TRUE" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMzwoPeyEd-p8t79IbuE0Q|org.eventb.core.guard#_aG1QANq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd4_2" org.eventb.core.predicate="ctrlCableCommand=CABLE_UNWIND" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMzwoPeyEd-p8t79IbuE0Q|org.eventb.core.guard#_aG1QAdq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyElevatorBetweenTwoFloors ≔ FALSE" org.eventb.core.label="act4_1" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMzwoPeyEd-p8t79IbuE0Q|org.eventb.core.action#_aG1QAtq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="PhyCableEngine ≔ CABLE_UNWIND" org.eventb.core.label="act4_2" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMzwoPeyEd-p8t79IbuE0Q|org.eventb.core.action#_BGnXAdrCEd-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="snsrElevatorFloor ≔ PhyElevatorFloor" org.eventb.core.label="act4_3" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMzwoPeyEd-p8t79IbuE0Q|org.eventb.core.action#_aG1QBNq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="snsrCableEngine ≔ CABLE_UNWIND" org.eventb.core.label="act4_4" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_wMzwoPeyEd-p8t79IbuE0Q|org.eventb.core.action#_aG1QBdq-Ed-L_e8_V4iXIg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT29" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="STOP_CABLE_ENGINE" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_aG13ENq-Ed-L_e8_V4iXIg">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT29" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_aG13ENq-Ed-L_e8_V4iXIg|org.eventb.core.refinesEvent#_mbkiVPluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd4_1" org.eventb.core.predicate="PhyCableEngine≠CABLE_STOP" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_aG13ENq-Ed-L_e8_V4iXIg|org.eventb.core.guard#_aG13Edq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd4_2" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_aG13ENq-Ed-L_e8_V4iXIg|org.eventb.core.guard#_aG13Etq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyCableEngine ≔ CABLE_STOP" org.eventb.core.label="act4_1" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_aG13ENq-Ed-L_e8_V4iXIg|org.eventb.core.action#_aG13E9q-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="snsrCableEngine ≔ CABLE_STOP" org.eventb.core.label="act4_2" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_aG13ENq-Ed-L_e8_V4iXIg|org.eventb.core.action#_aG13FNq-Ed-L_e8_V4iXIg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT30" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="open_door" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_HKimItqzEd-7IuFxCL4SWw">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT30" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_HKimItqzEd-7IuFxCL4SWw|org.eventb.core.refinesEvent#_mblJYPluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd3_1" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_HKimItqzEd-7IuFxCL4SWw|org.eventb.core.guard#_HKjNMNqzEd-7IuFxCL4SWw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd3_2" org.eventb.core.predicate="ctrlDoorCommand≠DOOR_OPEN" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_HKimItqzEd-7IuFxCL4SWw|org.eventb.core.guard#_pVt4EPS0Ed-43_jmKUh78g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd4_1" org.eventb.core.predicate="snsrCableEngine=CABLE_STOP" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_HKimItqzEd-7IuFxCL4SWw|org.eventb.core.guard#_-PriIdrtEd-yLuKmXl8XEA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd5_1" org.eventb.core.predicate="snsrDoorPosition=DOOR_CLOSED" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_HKimItqzEd-7IuFxCL4SWw|org.eventb.core.guard#_qrELU_S9Ed-43_jmKUh78g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD4" org.eventb.core.label="grd8_1" org.eventb.core.predicate="snsrElevatorFloor∈ctrlFloorButtonLightsSet∪ctrlUpButtonLightsSet∪ctrlDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift08_down_buttons.bum|org.eventb.core.machineFile#lift08_down_buttons|org.eventb.core.event#_HKimItqzEd-7IuFxCL4SWw|org.eventb.core.guard#_4s15IfYfEd-UnYOzyke7oQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="ctrlDoorCommand ≔ DOOR_OPEN" org.eventb.core.label="act3_1" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_HKimItqzEd-7IuFxCL4SWw|org.eventb.core.action#_HKjNMdqzEd-7IuFxCL4SWw"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT31" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="stop_door" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_SjmMQNq3Ed-AAt710HomgA">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT31" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_SjmMQNq3Ed-AAt710HomgA|org.eventb.core.refinesEvent#_mblJYfluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd3_1" org.eventb.core.predicate="ctrlDoorCommand=DOOR_OPEN" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_SjmMQNq3Ed-AAt710HomgA|org.eventb.core.guard#_SjmzUNq3Ed-AAt710HomgA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd5_1" org.eventb.core.predicate="snsrDoorPosition=DOOR_OPENED" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_SjmMQNq3Ed-AAt710HomgA|org.eventb.core.guard#_F6clEuA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="ctrlDoorCommand ≔ DOOR_STOP" org.eventb.core.label="act3_1" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_SjmMQNq3Ed-AAt710HomgA|org.eventb.core.action#_SjmzUdq3Ed-AAt710HomgA"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT32" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="close_door" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_HKjNMtqzEd-7IuFxCL4SWw">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT32" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_HKjNMtqzEd-7IuFxCL4SWw|org.eventb.core.refinesEvent#_mblJYvluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd3_1" org.eventb.core.predicate="ctrlDoorCommand=DOOR_STOP" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_HKjNMtqzEd-7IuFxCL4SWw|org.eventb.core.guard#_HKj0QNqzEd-7IuFxCL4SWw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd5_1" org.eventb.core.predicate="snsrDoorEngine=DOOR_STOP" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_HKjNMtqzEd-7IuFxCL4SWw|org.eventb.core.guard#_F6dMIeA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd9_1" org.eventb.core.predicate="schedule≠SCHEDULER_WAIT" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_HKjNMtqzEd-7IuFxCL4SWw|org.eventb.core.guard#_5Er_I_YkEd-UnYOzyke7oQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd9_2" org.eventb.core.predicate="snsrElevatorFloor∉ctrlFloorButtonLightsSet" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_HKjNMtqzEd-7IuFxCL4SWw|org.eventb.core.guard#_UtpDUe5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD4" org.eventb.core.label="grd9_4" org.eventb.core.predicate="schedule=SCHEDULER_DOWN⇒snsrElevatorFloor∉ctrlDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_HKjNMtqzEd-7IuFxCL4SWw|org.eventb.core.guard#_UtocQu5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD5" org.eventb.core.label="grd9_3" org.eventb.core.predicate="schedule=SCHEDULER_UP⇒snsrElevatorFloor∉ctrlUpButtonLightsSet" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_HKjNMtqzEd-7IuFxCL4SWw|org.eventb.core.guard#_UtocQ-5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="ctrlDoorCommand ≔ DOOR_CLOSE" org.eventb.core.label="act3_1" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_HKjNMtqzEd-7IuFxCL4SWw|org.eventb.core.action#_HKj0QdqzEd-7IuFxCL4SWw"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT33" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="start_move_up" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT33" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.refinesEvent#_mblwcPluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd2_1" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.guard#_hokz8_S5Ed-43_jmKUh78g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd3_1" org.eventb.core.predicate="ctrlDoorCommand=DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.guard#_hokz9PS5Ed-43_jmKUh78g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd4_1" org.eventb.core.predicate="snsrCableEngine=CABLE_STOP" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.guard#_yrcXo90WEd-DHKwvWNa8WQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd4_2" org.eventb.core.predicate="snsrElevatorFloor<LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.guard#_holbAPS5Ed-43_jmKUh78g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD4" org.eventb.core.label="grd5_1" org.eventb.core.predicate="snsrDoorPosition=DOOR_CLOSED" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.guard#_F6dMI-A2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD5" org.eventb.core.label="grd5_2" org.eventb.core.predicate="snsrDoorEngine=DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.guard#_F6dMJOA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD6" org.eventb.core.label="grd9_1" org.eventb.core.predicate="schedule=SCHEDULER_UP" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.guard#_UtpDU-5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD7" org.eventb.core.label="grd9_2" org.eventb.core.predicate="snsrElevatorFloor∉ctrlFloorButtonLightsSet∪ctrlUpButtonLightsSet" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.guard#_5EsmMfYkEd-UnYOzyke7oQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="ctrlCableCommand ≔ CABLE_WIND" org.eventb.core.label="act2_1" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.action#_holbAfS5Ed-43_jmKUh78g"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="last_stop ≔ snsrElevatorFloor" org.eventb.core.label="act2_2" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.action#_holbAvS5Ed-43_jmKUh78g"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT34" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="start_move_down" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT34" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.refinesEvent#_mblwcfluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd2_1" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.guard#_holbBPS5Ed-43_jmKUh78g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd3_1" org.eventb.core.predicate="ctrlDoorCommand=DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.guard#_holbBfS5Ed-43_jmKUh78g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd4_1" org.eventb.core.predicate="snsrCableEngine=CABLE_STOP" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.guard#_yrc-st0WEd-DHKwvWNa8WQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd4_2" org.eventb.core.predicate="snsrElevatorFloor>0" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.guard#_holbBvS5Ed-43_jmKUh78g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD4" org.eventb.core.label="grd5_1" org.eventb.core.predicate="snsrDoorPosition=DOOR_CLOSED" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.guard#_F6dzMuA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD5" org.eventb.core.label="grd5_2" org.eventb.core.predicate="snsrDoorEngine=DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift05_phys_door.bum|org.eventb.core.machineFile#lift05_phys_door|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.guard#_F6dzM-A2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD6" org.eventb.core.label="grd9_1" org.eventb.core.predicate="schedule=SCHEDULER_DOWN" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.guard#_UtpqYu5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD7" org.eventb.core.label="grd9_2" org.eventb.core.predicate="snsrElevatorFloor∉ctrlFloorButtonLightsSet∪ctrlDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.guard#_5EtNQfYkEd-UnYOzyke7oQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="ctrlCableCommand ≔ CABLE_UNWIND" org.eventb.core.label="act2_1" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.action#_homCEPS5Ed-43_jmKUh78g"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="last_stop ≔ snsrElevatorFloor" org.eventb.core.label="act2_2" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.action#_homCEfS5Ed-43_jmKUh78g"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT35" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="stop" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT35" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw|org.eventb.core.refinesEvent#_mblwcvluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd2_1" org.eventb.core.predicate="ctrlCableCommand≠CABLE_STOP" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw|org.eventb.core.guard#_yC5I4tqwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2_2" org.eventb.core.predicate="last_stop≠PhyElevatorFloor" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw|org.eventb.core.guard#_yC5I49qwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd4_1" org.eventb.core.predicate="snsrElevatorFloor≠−1" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_homCEvS5Ed-43_jmKUh78g|org.eventb.core.guard#_homCFPS5Ed-43_jmKUh78g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd9_1" org.eventb.core.predicate="snsrElevatorFloor∈ctrlFloorButtonLightsSet∨(snsrElevatorFloor∈ctrlUpButtonLightsSet∧schedule=SCHEDULER_UP)∨(snsrElevatorFloor∈ctrlDownButtonLightsSet∧schedule=SCHEDULER_DOWN)∨(snsrElevatorFloor∈ctrlUpButtonLightsSet∧schedule=SCHEDULER_DOWN∧0 ‥ (snsrElevatorFloor − 1)∩requests=(∅ ⦂ ℙ(ℤ)))∨(snsrElevatorFloor∈ctrlDownButtonLightsSet∧schedule=SCHEDULER_UP∧snsrElevatorFloor+1 ‥ LAST_FLOOR∩requests=(∅ ⦂ ℙ(ℤ)))" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw|org.eventb.core.guard#_UtqRcu5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="ctrlCableCommand ≔ CABLE_STOP" org.eventb.core.label="act2_1" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw|org.eventb.core.action#_yC5v8NqwEd-O4vbSPlarTw"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="schedule ≔ SCHEDULER_WAIT" org.eventb.core.label="act9_2" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw|org.eventb.core.action#_UtqRc-5-Ed-dEtybZVK09Q"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT36" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="switch_schedule_to_up" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_Utq4gO5-Ed-dEtybZVK09Q">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT36" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_Utq4gO5-Ed-dEtybZVK09Q|org.eventb.core.refinesEvent#_mbmXgPluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd9_1" org.eventb.core.predicate="schedule=SCHEDULER_WAIT" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utq4gO5-Ed-dEtybZVK09Q|org.eventb.core.guard#_Utq4hO5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd9_2" org.eventb.core.predicate="snsrElevatorFloor+1 ‥ LAST_FLOOR∩requests≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utq4gO5-Ed-dEtybZVK09Q|org.eventb.core.guard#_Utq4he5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd9_3" org.eventb.core.predicate="snsrElevatorFloor∉ctrlFloorButtonLightsSet∪ctrlUpButtonLightsSet" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utq4gO5-Ed-dEtybZVK09Q|org.eventb.core.guard#_0iuhwPiTEd-5bJQIzgxuHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd9_4" org.eventb.core.predicate="0 ‥ (snsrElevatorFloor − 1)∩requests=(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utq4gO5-Ed-dEtybZVK09Q|org.eventb.core.guard#_Utrfke5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD4" org.eventb.core.label="grd9_5" org.eventb.core.predicate="last_schedule=SCHEDULER_DOWN" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utq4gO5-Ed-dEtybZVK09Q|org.eventb.core.guard#_Utrfk-5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD5" org.eventb.core.label="grd9_6" org.eventb.core.predicate="request_served=TRUE" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utq4gO5-Ed-dEtybZVK09Q|org.eventb.core.guard#_q3mBsPluEd-1httaBm5m2g" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="schedule ≔ SCHEDULER_UP" org.eventb.core.label="act9_1" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utq4gO5-Ed-dEtybZVK09Q|org.eventb.core.action#_UtrflO5-Ed-dEtybZVK09Q"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="last_schedule ≔ SCHEDULER_UP" org.eventb.core.label="act9_2" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utq4gO5-Ed-dEtybZVK09Q|org.eventb.core.action#_6IA_8Pk7Ed-WtNZH8d5nSA"/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="request_served ≔ FALSE" org.eventb.core.label="act9_3" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utq4gO5-Ed-dEtybZVK09Q|org.eventb.core.action#_q3mowPluEd-1httaBm5m2g"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT37" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="resume_schedule_up" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_Utrfle5-Ed-dEtybZVK09Q">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT37" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_Utrfle5-Ed-dEtybZVK09Q|org.eventb.core.refinesEvent#_mbmXgfluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd9_1" org.eventb.core.predicate="schedule=SCHEDULER_WAIT" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utrfle5-Ed-dEtybZVK09Q|org.eventb.core.guard#_UtsGou5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd9_2" org.eventb.core.predicate="snsrElevatorFloor+1 ‥ LAST_FLOOR∩requests≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utrfle5-Ed-dEtybZVK09Q|org.eventb.core.guard#_UtsGo-5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd9_3" org.eventb.core.predicate="snsrElevatorFloor∉ctrlFloorButtonLightsSet∪ctrlUpButtonLightsSet" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utrfle5-Ed-dEtybZVK09Q|org.eventb.core.guard#_0ivI0PiTEd-5bJQIzgxuHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd9_4" org.eventb.core.predicate="last_schedule=SCHEDULER_UP" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utrfle5-Ed-dEtybZVK09Q|org.eventb.core.guard#_UtstsO5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD4" org.eventb.core.label="grd9_5" org.eventb.core.predicate="request_served=TRUE" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utrfle5-Ed-dEtybZVK09Q|org.eventb.core.guard#_q3mowfluEd-1httaBm5m2g" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="schedule ≔ SCHEDULER_UP" org.eventb.core.label="act9_1" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utrfle5-Ed-dEtybZVK09Q|org.eventb.core.action#_Utstse5-Ed-dEtybZVK09Q"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="request_served ≔ FALSE" org.eventb.core.label="act9_2" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utrfle5-Ed-dEtybZVK09Q|org.eventb.core.action#_q3nP0PluEd-1httaBm5m2g"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT38" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="switch_schedule_to_down" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_Utstsu5-Ed-dEtybZVK09Q">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT38" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_Utstsu5-Ed-dEtybZVK09Q|org.eventb.core.refinesEvent#_mbmXgvluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd9_1" org.eventb.core.predicate="schedule=SCHEDULER_WAIT" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utstsu5-Ed-dEtybZVK09Q|org.eventb.core.guard#_UttUwO5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd9_2" org.eventb.core.predicate="0 ‥ (snsrElevatorFloor − 1)∩requests≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utstsu5-Ed-dEtybZVK09Q|org.eventb.core.guard#_UttUwe5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd9_3" org.eventb.core.predicate="snsrElevatorFloor∉ctrlFloorButtonLightsSet∪ctrlDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utstsu5-Ed-dEtybZVK09Q|org.eventb.core.guard#_0ivv4PiTEd-5bJQIzgxuHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd9_4" org.eventb.core.predicate="snsrElevatorFloor+1 ‥ LAST_FLOOR∩requests=(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utstsu5-Ed-dEtybZVK09Q|org.eventb.core.guard#_UttUw-5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD4" org.eventb.core.label="grd9_5" org.eventb.core.predicate="last_schedule=SCHEDULER_UP" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utstsu5-Ed-dEtybZVK09Q|org.eventb.core.guard#_q3n24PluEd-1httaBm5m2g" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD5" org.eventb.core.label="grd9_6" org.eventb.core.predicate="request_served=TRUE" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utstsu5-Ed-dEtybZVK09Q|org.eventb.core.guard#_UttUxe5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="schedule ≔ SCHEDULER_DOWN" org.eventb.core.label="act9_1" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utstsu5-Ed-dEtybZVK09Q|org.eventb.core.action#_Utt70O5-Ed-dEtybZVK09Q"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="last_schedule ≔ SCHEDULER_DOWN" org.eventb.core.label="act9_2" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utstsu5-Ed-dEtybZVK09Q|org.eventb.core.action#_6ICOEPk7Ed-WtNZH8d5nSA"/>
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="request_served ≔ FALSE" org.eventb.core.label="act9_3" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utstsu5-Ed-dEtybZVK09Q|org.eventb.core.action#_q3n24fluEd-1httaBm5m2g"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT39" org.eventb.core.accurate="true" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="resume_schedule_down" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_Utt70e5-Ed-dEtybZVK09Q">
<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift10_conv_lights.bcm|org.eventb.core.scMachineFile#lift10_conv_lights|org.eventb.core.scEvent#EVT39" org.eventb.core.source="/ProvenLift/lift11_conv_lights.bum|org.eventb.core.machineFile#lift11_conv_lights|org.eventb.core.event#_Utt70e5-Ed-dEtybZVK09Q|org.eventb.core.refinesEvent#_mbm-kPluEd-1httaBm5m2g"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd9_1" org.eventb.core.predicate="schedule=SCHEDULER_WAIT" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utt70e5-Ed-dEtybZVK09Q|org.eventb.core.guard#_Utt71O5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd9_2" org.eventb.core.predicate="0 ‥ (snsrElevatorFloor − 1)∩requests≠(∅ ⦂ ℙ(ℤ))" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utt70e5-Ed-dEtybZVK09Q|org.eventb.core.guard#_Utt71e5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd9_3" org.eventb.core.predicate="snsrElevatorFloor∉ctrlFloorButtonLightsSet∪ctrlDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utt70e5-Ed-dEtybZVK09Q|org.eventb.core.guard#_0iwW8PiTEd-5bJQIzgxuHg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd9_4" org.eventb.core.predicate="last_schedule=SCHEDULER_DOWN" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utt70e5-Ed-dEtybZVK09Q|org.eventb.core.guard#_Utui4e5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD4" org.eventb.core.label="grd9_5" org.eventb.core.predicate="request_served=TRUE" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utt70e5-Ed-dEtybZVK09Q|org.eventb.core.guard#_q3od8PluEd-1httaBm5m2g" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="schedule ≔ SCHEDULER_DOWN" org.eventb.core.label="act9_1" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utt70e5-Ed-dEtybZVK09Q|org.eventb.core.action#_Utui4u5-Ed-dEtybZVK09Q"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="request_served ≔ FALSE" org.eventb.core.label="act9_2" org.eventb.core.source="/ProvenLift/lift09_scheduler.bum|org.eventb.core.machineFile#lift09_scheduler|org.eventb.core.event#_Utt70e5-Ed-dEtybZVK09Q|org.eventb.core.action#_q3od8fluEd-1httaBm5m2g"/>
</org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>