-
Notifications
You must be signed in to change notification settings - Fork 0
/
lift11_conv_add_req.bum
154 lines (154 loc) · 20.6 KB
/
lift11_conv_add_req.bum
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
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.texttools.text_lastmodified="1291328143647" org.eventb.texttools.text_representation="machine lift11_conv_add_req refines lift09_scheduler sees ctx5_scheduler variables PhyElevatorFloor PhyCableEngine PhyElevatorBetweenTwoFloors ctrlCableCommand snsrCableEngine snsrElevatorFloor PhyDoorEngine PhyDoorPosition ctrlDoorCommand snsrDoorEngine snsrDoorPosition PhyFloorButtonsSet snsrFloorButtonsSet PhyFloorButtonLightsSet ctrlFloorButtonLightsSet PhyUpButtonsSet snsrUpButtonsSet PhyUpButtonLightsSet ctrlUpButtonLightsSet PhyDownButtonsSet snsrDownButtonsSet PhyDownButtonLightsSet ctrlDownButtonLightsSet last_schedule schedule last_stop requests request_served invariants @inv11_1 schedule = SCHEDULER_WAIT ∧ snsrElevatorFloor∉requests ⇒ request_served = TRUE events event INITIALISATION extends INITIALISATION end event USER_PRESSES_DOWN_BUTTON extends USER_PRESSES_DOWN_BUTTON end anticipated event USER_RELEASES_DOWN_BUTTON extends USER_RELEASES_DOWN_BUTTON end anticipated event TURNS_ON_DOWN_BUTTON_LIGHT extends TURNS_ON_DOWN_BUTTON_LIGHT end anticipated event TURNS_OFF_DOWN_BUTTON_LIGHT extends TURNS_OFF_DOWN_BUTTON_LIGHT end anticipated event turn_down_button_light_on extends turn_down_button_light_on end anticipated event turn_down_button_light_off extends turn_down_button_light_off end event USER_PRESSES_UP_BUTTON extends USER_PRESSES_UP_BUTTON end anticipated event USER_RELEASES_UP_BUTTON extends USER_RELEASES_UP_BUTTON end anticipated event TURNS_ON_UP_BUTTON_LIGHT extends TURNS_ON_UP_BUTTON_LIGHT end anticipated event TURNS_OFF_UP_BUTTON_LIGHT extends TURNS_OFF_UP_BUTTON_LIGHT end anticipated event turn_up_button_light_on extends turn_up_button_light_on end anticipated event turn_up_button_light_off extends turn_up_button_light_off end event USER_PRESSES_FLOOR_BUTTON extends USER_PRESSES_FLOOR_BUTTON end anticipated event USER_RELEASES_FLOOR_BUTTON extends USER_RELEASES_FLOOR_BUTTON end anticipated event TURNS_ON_FLOOR_BUTTON_LIGHT extends TURNS_ON_FLOOR_BUTTON_LIGHT end anticipated event TURNS_OFF_FLOOR_BUTTON_LIGHT extends TURNS_OFF_FLOOR_BUTTON_LIGHT end anticipated event turn_floor_button_light_on extends turn_floor_button_light_on end anticipated event turn_floor_button_light_off extends turn_floor_button_light_off end anticipated event DOOR_OPENS_WHEN_CLOSED extends DOOR_OPENS_WHEN_CLOSED end anticipated event DOOR_OPENS_WHEN_HALF extends DOOR_OPENS_WHEN_HALF end anticipated event DOOR_CLOSES_WHEN_OPENED extends DOOR_CLOSES_WHEN_OPENED end anticipated event DOOR_CLOSES_WHEN_HALF extends DOOR_CLOSES_WHEN_HALF end anticipated event DOOR_CLOSES_WHEN_CLOSED extends DOOR_CLOSES_WHEN_CLOSED end anticipated event STOP_DOOR_ENGINE extends STOP_DOOR_ENGINE end anticipated event ELEVATOR_LEAVES_FLOOR_UP extends ELEVATOR_LEAVES_FLOOR_UP where @grd11_1 snsrElevatorFloor = last_stop ∨ (snsrElevatorFloor ∉ (ctrlFloorButtonLightsSet ∪ ctrlUpButtonLightsSet) ∧ (snsrElevatorFloor ∉ ctrlDownButtonLightsSet ∨ snsrElevatorFloor+1‥LAST_FLOOR ∩ requests ≠ ∅)) end anticipated event ELEVATOR_REACHES_FLOOR_UP extends ELEVATOR_REACHES_FLOOR_UP end anticipated event ELEVATOR_LEAVES_FLOOR_DOWN extends ELEVATOR_LEAVES_FLOOR_DOWN where @grd11_1 snsrElevatorFloor = last_stop ∨ (snsrElevatorFloor ∉ (ctrlFloorButtonLightsSet ∪ ctrlDownButtonLightsSet) ∧ (snsrElevatorFloor ∉ ctrlUpButtonLightsSet ∨ 0‥snsrElevatorFloor−1 ∩ requests ≠ ∅)) end anticipated event ELEVATOR_REACHES_FLOOR_DOWN extends ELEVATOR_REACHES_FLOOR_DOWN end anticipated event STOP_CABLE_ENGINE extends STOP_CABLE_ENGINE end anticipated event open_door extends open_door end anticipated event stop_door extends stop_door end anticipated event close_door extends close_door end anticipated event start_move_up extends start_move_up end anticipated event start_move_down extends start_move_down end anticipated event stop extends stop end anticipated event switch_schedule_to_up extends switch_schedule_to_up end anticipated event resume_schedule_up extends resume_schedule_up end anticipated event switch_schedule_to_down extends switch_schedule_to_down end anticipated event resume_schedule_down extends resume_schedule_down end end " version="5">
<org.eventb.core.refinesMachine name="_tKoyoP5hEd-RbO_JCG3Adw" org.eventb.core.target="lift09_scheduler"/>
<org.eventb.core.seesContext name="_tKoyof5hEd-RbO_JCG3Adw" org.eventb.core.target="ctx5_scheduler"/>
<org.eventb.core.variable name="_9uEEsNd9Ed-Dle0at0Xgqg" org.eventb.core.identifier="PhyElevatorFloor"/>
<org.eventb.core.variable name="_aGvwctq-Ed-L_e8_V4iXIg" org.eventb.core.identifier="PhyCableEngine"/>
<org.eventb.core.variable name="_aGwXgNq-Ed-L_e8_V4iXIg" org.eventb.core.identifier="PhyElevatorBetweenTwoFloors"/>
<org.eventb.core.variable name="_1cMDMtd_Ed-Dle0at0Xgqg" org.eventb.core.identifier="ctrlCableCommand"/>
<org.eventb.core.variable name="_aGwXgtq-Ed-L_e8_V4iXIg" org.eventb.core.identifier="snsrCableEngine"/>
<org.eventb.core.variable name="_aGwXg9q-Ed-L_e8_V4iXIg" org.eventb.core.identifier="snsrElevatorFloor"/>
<org.eventb.core.variable name="_KgYVwOAzEd-73py7lbE8bg" org.eventb.core.identifier="PhyDoorEngine"/>
<org.eventb.core.variable name="_KgYVweAzEd-73py7lbE8bg" org.eventb.core.identifier="PhyDoorPosition"/>
<org.eventb.core.variable name="_HKh_EtqzEd-7IuFxCL4SWw" org.eventb.core.identifier="ctrlDoorCommand"/>
<org.eventb.core.variable name="_KgY80OAzEd-73py7lbE8bg" org.eventb.core.identifier="snsrDoorEngine"/>
<org.eventb.core.variable name="_KgY80eAzEd-73py7lbE8bg" org.eventb.core.identifier="snsrDoorPosition"/>
<org.eventb.core.variable name="_tIzE0OA_Ed-78bCl9yYd-Q" org.eventb.core.identifier="PhyFloorButtonsSet"/>
<org.eventb.core.variable name="_tIzr4OA_Ed-78bCl9yYd-Q" org.eventb.core.identifier="snsrFloorButtonsSet"/>
<org.eventb.core.variable name="_tIzr4eA_Ed-78bCl9yYd-Q" org.eventb.core.identifier="PhyFloorButtonLightsSet"/>
<org.eventb.core.variable name="_tIzr4uA_Ed-78bCl9yYd-Q" org.eventb.core.identifier="ctrlFloorButtonLightsSet"/>
<org.eventb.core.variable name="_pvTcwOEsEd-bh-7nDQnLgQ" org.eventb.core.identifier="PhyUpButtonsSet"/>
<org.eventb.core.variable name="_pvTcweEsEd-bh-7nDQnLgQ" org.eventb.core.identifier="snsrUpButtonsSet"/>
<org.eventb.core.variable name="_pvTcwuEsEd-bh-7nDQnLgQ" org.eventb.core.identifier="PhyUpButtonLightsSet"/>
<org.eventb.core.variable name="_pvUD0OEsEd-bh-7nDQnLgQ" org.eventb.core.identifier="ctrlUpButtonLightsSet"/>
<org.eventb.core.variable name="_3IjaoOWyEd-64JNDK1TKiQ" org.eventb.core.identifier="PhyDownButtonsSet"/>
<org.eventb.core.variable name="_3IjaoeWyEd-64JNDK1TKiQ" org.eventb.core.identifier="snsrDownButtonsSet"/>
<org.eventb.core.variable name="_3IjaouWyEd-64JNDK1TKiQ" org.eventb.core.identifier="PhyDownButtonLightsSet"/>
<org.eventb.core.variable name="_3Ijao-WyEd-64JNDK1TKiQ" org.eventb.core.identifier="ctrlDownButtonLightsSet"/>
<org.eventb.core.variable name="_UtggcO5-Ed-dEtybZVK09Q" org.eventb.core.identifier="last_schedule"/>
<org.eventb.core.variable name="_Utggce5-Ed-dEtybZVK09Q" org.eventb.core.identifier="schedule"/>
<org.eventb.core.variable name="_-7fiIPS-Ed-43_jmKUh78g" org.eventb.core.identifier="last_stop"/>
<org.eventb.core.variable name="_6H3O8Pk7Ed-WtNZH8d5nSA" org.eventb.core.identifier="requests"/>
<org.eventb.core.variable name="_6yDrMP4MEd-Vo467mFpzFA" org.eventb.core.identifier="request_served"/>
<org.eventb.core.invariant name="_EdQF4PlyEd-F0OvBKAXwJQ" org.eventb.core.label="inv11_1" org.eventb.core.predicate="schedule = SCHEDULER_WAIT ∧ snsrElevatorFloor∉requests ⇒ request_served = TRUE"/>
<org.eventb.core.event name="'" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION"/>
<org.eventb.core.event name="_3IkoxOWyEd-64JNDK1TKiQ" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_PRESSES_DOWN_BUTTON">
<org.eventb.core.refinesEvent name="_tKqn0P5hEd-RbO_JCG3Adw" org.eventb.core.target="USER_PRESSES_DOWN_BUTTON"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tKqn0f5hEd-RbO_JCG3Adw" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_DOWN_BUTTON">
<org.eventb.core.refinesEvent name="_tKrO4P5hEd-RbO_JCG3Adw" org.eventb.core.target="USER_RELEASES_DOWN_BUTTON"/>
</org.eventb.core.event>
<org.eventb.core.event name="_3Il25eWyEd-64JNDK1TKiQ" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="TURNS_ON_DOWN_BUTTON_LIGHT">
<org.eventb.core.refinesEvent name="_tKrO4f5hEd-RbO_JCG3Adw" org.eventb.core.target="TURNS_ON_DOWN_BUTTON_LIGHT"/>
</org.eventb.core.event>
<org.eventb.core.event name="_3Imd9eWyEd-64JNDK1TKiQ" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="TURNS_OFF_DOWN_BUTTON_LIGHT">
<org.eventb.core.refinesEvent name="_tKrO4v5hEd-RbO_JCG3Adw" org.eventb.core.target="TURNS_OFF_DOWN_BUTTON_LIGHT"/>
</org.eventb.core.event>
<org.eventb.core.event name="_3InsEuWyEd-64JNDK1TKiQ" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="turn_down_button_light_on">
<org.eventb.core.refinesEvent name="_tKrO4_5hEd-RbO_JCG3Adw" org.eventb.core.target="turn_down_button_light_on"/>
</org.eventb.core.event>
<org.eventb.core.event name="_3IoTI-WyEd-64JNDK1TKiQ" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="turn_down_button_light_off">
<org.eventb.core.refinesEvent name="_tKr18P5hEd-RbO_JCG3Adw" org.eventb.core.target="turn_down_button_light_off"/>
</org.eventb.core.event>
<org.eventb.core.event name="_pvVR8eEsEd-bh-7nDQnLgQ" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_PRESSES_UP_BUTTON">
<org.eventb.core.refinesEvent name="_tKr18f5hEd-RbO_JCG3Adw" org.eventb.core.target="USER_PRESSES_UP_BUTTON"/>
</org.eventb.core.event>
<org.eventb.core.event name="_3Io6M-WyEd-64JNDK1TKiQ" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_UP_BUTTON">
<org.eventb.core.refinesEvent name="_tKr18v5hEd-RbO_JCG3Adw" org.eventb.core.target="USER_RELEASES_UP_BUTTON"/>
</org.eventb.core.event>
<org.eventb.core.event name="_pvV5BuEsEd-bh-7nDQnLgQ" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="TURNS_ON_UP_BUTTON_LIGHT">
<org.eventb.core.refinesEvent name="_tKr18_5hEd-RbO_JCG3Adw" org.eventb.core.target="TURNS_ON_UP_BUTTON_LIGHT"/>
</org.eventb.core.event>
<org.eventb.core.event name="_pvWgFeEsEd-bh-7nDQnLgQ" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="TURNS_OFF_UP_BUTTON_LIGHT">
<org.eventb.core.refinesEvent name="_tKsdAP5hEd-RbO_JCG3Adw" org.eventb.core.target="TURNS_OFF_UP_BUTTON_LIGHT"/>
</org.eventb.core.event>
<org.eventb.core.event name="_pvXHJeEsEd-bh-7nDQnLgQ" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="turn_up_button_light_on">
<org.eventb.core.refinesEvent name="_tKsdAf5hEd-RbO_JCG3Adw" org.eventb.core.target="turn_up_button_light_on"/>
</org.eventb.core.event>
<org.eventb.core.event name="_pvXuNeEsEd-bh-7nDQnLgQ" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="turn_up_button_light_off">
<org.eventb.core.refinesEvent name="_tKsdAv5hEd-RbO_JCG3Adw" org.eventb.core.target="turn_up_button_light_off"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tI1hE-A_Ed-78bCl9yYd-Q" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_PRESSES_FLOOR_BUTTON">
<org.eventb.core.refinesEvent name="_tKtEEP5hEd-RbO_JCG3Adw" org.eventb.core.target="USER_PRESSES_FLOOR_BUTTON"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tKtEEf5hEd-RbO_JCG3Adw" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_FLOOR_BUTTON">
<org.eventb.core.refinesEvent name="_tKtEEv5hEd-RbO_JCG3Adw" org.eventb.core.target="USER_RELEASES_FLOOR_BUTTON"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tI2vNeA_Ed-78bCl9yYd-Q" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="TURNS_ON_FLOOR_BUTTON_LIGHT">
<org.eventb.core.refinesEvent name="_tKtEE_5hEd-RbO_JCG3Adw" org.eventb.core.target="TURNS_ON_FLOOR_BUTTON_LIGHT"/>
</org.eventb.core.event>
<org.eventb.core.event name="_pvY8UuEsEd-bh-7nDQnLgQ" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="TURNS_OFF_FLOOR_BUTTON_LIGHT">
<org.eventb.core.refinesEvent name="_tKtEFP5hEd-RbO_JCG3Adw" org.eventb.core.target="TURNS_OFF_FLOOR_BUTTON_LIGHT"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tI4kYuA_Ed-78bCl9yYd-Q" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="turn_floor_button_light_on">
<org.eventb.core.refinesEvent name="_tKtrIP5hEd-RbO_JCG3Adw" org.eventb.core.target="turn_floor_button_light_on"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tI5ygOA_Ed-78bCl9yYd-Q" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="turn_floor_button_light_off">
<org.eventb.core.refinesEvent name="_tKtrIf5hEd-RbO_JCG3Adw" org.eventb.core.target="turn_floor_button_light_off"/>
</org.eventb.core.event>
<org.eventb.core.event name="_KgayBOAzEd-73py7lbE8bg" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="DOOR_OPENS_WHEN_CLOSED">
<org.eventb.core.refinesEvent name="_tKtrIv5hEd-RbO_JCG3Adw" org.eventb.core.target="DOOR_OPENS_WHEN_CLOSED"/>
</org.eventb.core.event>
<org.eventb.core.event name="_KgcAIOAzEd-73py7lbE8bg" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="DOOR_OPENS_WHEN_HALF">
<org.eventb.core.refinesEvent name="_tKuSMP5hEd-RbO_JCG3Adw" org.eventb.core.target="DOOR_OPENS_WHEN_HALF"/>
</org.eventb.core.event>
<org.eventb.core.event name="_KgcnM-AzEd-73py7lbE8bg" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="DOOR_CLOSES_WHEN_OPENED">
<org.eventb.core.refinesEvent name="_tKuSMf5hEd-RbO_JCG3Adw" org.eventb.core.target="DOOR_CLOSES_WHEN_OPENED"/>
</org.eventb.core.event>
<org.eventb.core.event name="_KgdOReAzEd-73py7lbE8bg" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="DOOR_CLOSES_WHEN_HALF">
<org.eventb.core.refinesEvent name="_tKuSMv5hEd-RbO_JCG3Adw" org.eventb.core.target="DOOR_CLOSES_WHEN_HALF"/>
</org.eventb.core.event>
<org.eventb.core.event name="_KgecYeAzEd-73py7lbE8bg" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="DOOR_CLOSES_WHEN_CLOSED">
<org.eventb.core.refinesEvent name="_tKuSM_5hEd-RbO_JCG3Adw" org.eventb.core.target="DOOR_CLOSES_WHEN_CLOSED"/>
</org.eventb.core.event>
<org.eventb.core.event name="_KgfDcuAzEd-73py7lbE8bg" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="STOP_DOOR_ENGINE">
<org.eventb.core.refinesEvent name="_tKu5QP5hEd-RbO_JCG3Adw" org.eventb.core.target="STOP_DOOR_ENGINE"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tKu5Qf5hEd-RbO_JCG3Adw" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_UP">
<org.eventb.core.refinesEvent name="_tKu5Qv5hEd-RbO_JCG3Adw" org.eventb.core.target="ELEVATOR_LEAVES_FLOOR_UP"/>
<org.eventb.core.guard name="_EdU-YflyEd-F0OvBKAXwJQ" org.eventb.core.label="grd11_1" org.eventb.core.predicate="snsrElevatorFloor = last_stop ∨ (snsrElevatorFloor ∉ (ctrlFloorButtonLightsSet ∪ ctrlUpButtonLightsSet) ∧ (snsrElevatorFloor ∉ ctrlDownButtonLightsSet ∨ snsrElevatorFloor+1‥LAST_FLOOR ∩ requests ≠ ∅))"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tKu5Q_5hEd-RbO_JCG3Adw" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_UP">
<org.eventb.core.refinesEvent name="_tKu5RP5hEd-RbO_JCG3Adw" org.eventb.core.target="ELEVATOR_REACHES_FLOOR_UP"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tKvgUP5hEd-RbO_JCG3Adw" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_DOWN">
<org.eventb.core.refinesEvent name="_tKvgUf5hEd-RbO_JCG3Adw" org.eventb.core.target="ELEVATOR_LEAVES_FLOOR_DOWN"/>
<org.eventb.core.guard name="_EdU-ZvlyEd-F0OvBKAXwJQ" org.eventb.core.label="grd11_1" org.eventb.core.predicate="snsrElevatorFloor = last_stop ∨ (snsrElevatorFloor ∉ (ctrlFloorButtonLightsSet ∪ ctrlDownButtonLightsSet) ∧ (snsrElevatorFloor ∉ ctrlUpButtonLightsSet ∨ 0‥snsrElevatorFloor−1 ∩ requests ≠ ∅))"/>
</org.eventb.core.event>
<org.eventb.core.event name="_tKvgUv5hEd-RbO_JCG3Adw" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_DOWN">
<org.eventb.core.refinesEvent name="_tKvgU_5hEd-RbO_JCG3Adw" org.eventb.core.target="ELEVATOR_REACHES_FLOOR_DOWN"/>
</org.eventb.core.event>
<org.eventb.core.event name="_aG13ENq-Ed-L_e8_V4iXIg" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="STOP_CABLE_ENGINE">
<org.eventb.core.refinesEvent name="_tKwHYP5hEd-RbO_JCG3Adw" org.eventb.core.target="STOP_CABLE_ENGINE"/>
</org.eventb.core.event>
<org.eventb.core.event name="_HKimItqzEd-7IuFxCL4SWw" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="open_door">
<org.eventb.core.refinesEvent name="_tKwHYf5hEd-RbO_JCG3Adw" org.eventb.core.target="open_door"/>
</org.eventb.core.event>
<org.eventb.core.event name="_SjmMQNq3Ed-AAt710HomgA" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="stop_door">
<org.eventb.core.refinesEvent name="_tKwHYv5hEd-RbO_JCG3Adw" org.eventb.core.target="stop_door"/>
</org.eventb.core.event>
<org.eventb.core.event name="_HKjNMtqzEd-7IuFxCL4SWw" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="close_door">
<org.eventb.core.refinesEvent name="_tKwHY_5hEd-RbO_JCG3Adw" org.eventb.core.target="close_door"/>
</org.eventb.core.event>
<org.eventb.core.event name="_yC2soNqwEd-O4vbSPlarTw" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="start_move_up">
<org.eventb.core.refinesEvent name="_tKwucP5hEd-RbO_JCG3Adw" org.eventb.core.target="start_move_up"/>
</org.eventb.core.event>
<org.eventb.core.event name="_yC36wNqwEd-O4vbSPlarTw" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="start_move_down">
<org.eventb.core.refinesEvent name="_tKwucf5hEd-RbO_JCG3Adw" org.eventb.core.target="start_move_down"/>
</org.eventb.core.event>
<org.eventb.core.event name="_yC5I4dqwEd-O4vbSPlarTw" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="stop">
<org.eventb.core.refinesEvent name="_tKwucv5hEd-RbO_JCG3Adw" org.eventb.core.target="stop"/>
</org.eventb.core.event>
<org.eventb.core.event name="_Utq4gO5-Ed-dEtybZVK09Q" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="switch_schedule_to_up">
<org.eventb.core.refinesEvent name="_tKxVgP5hEd-RbO_JCG3Adw" org.eventb.core.target="switch_schedule_to_up"/>
</org.eventb.core.event>
<org.eventb.core.event name="_Utrfle5-Ed-dEtybZVK09Q" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="resume_schedule_up">
<org.eventb.core.refinesEvent name="_tKxVgf5hEd-RbO_JCG3Adw" org.eventb.core.target="resume_schedule_up"/>
</org.eventb.core.event>
<org.eventb.core.event name="_Utstsu5-Ed-dEtybZVK09Q" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="switch_schedule_to_down">
<org.eventb.core.refinesEvent name="_tKxVgv5hEd-RbO_JCG3Adw" org.eventb.core.target="switch_schedule_to_down"/>
</org.eventb.core.event>
<org.eventb.core.event name="_Utt70e5-Ed-dEtybZVK09Q" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="resume_schedule_down">
<org.eventb.core.refinesEvent name="_tKx8kP5hEd-RbO_JCG3Adw" org.eventb.core.target="resume_schedule_down"/>
</org.eventb.core.event>
</org.eventb.core.machineFile>