/
lift27_conv_door.bum
153 lines (153 loc) · 20 KB
/
lift27_conv_door.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
<?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="1290846898993" org.eventb.texttools.text_representation="machine lift27_conv_door refines lift26_conv_move sees ctx6_conv_utils 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 theorem @thm1 finite(DOOR_COMMAND) variant card({x∣x∈DOOR_COMMAND ∧ schedule ≠ SCHEDULER_WAIT ∧ (schedule = SCHEDULER_DOWN ⇒ snsrElevatorFloor ∉ (ctrlFloorButtonLightsSet ∪ ctrlDownButtonLightsSet)) ∧ (schedule = SCHEDULER_UP ⇒ snsrElevatorFloor ∉ (ctrlFloorButtonLightsSet ∪ ctrlUpButtonLightsSet))} ∩ {ctrlDoorCommand, DOOR_CLOSE}) 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 convergent event TURNS_ON_DOWN_BUTTON_LIGHT extends TURNS_ON_DOWN_BUTTON_LIGHT end convergent event TURNS_OFF_DOWN_BUTTON_LIGHT extends TURNS_OFF_DOWN_BUTTON_LIGHT end convergent event turn_down_button_light_on extends turn_down_button_light_on end convergent 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 convergent event TURNS_ON_UP_BUTTON_LIGHT extends TURNS_ON_UP_BUTTON_LIGHT end convergent event TURNS_OFF_UP_BUTTON_LIGHT extends TURNS_OFF_UP_BUTTON_LIGHT end convergent event turn_up_button_light_on extends turn_up_button_light_on end convergent 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 convergent event TURNS_ON_FLOOR_BUTTON_LIGHT extends TURNS_ON_FLOOR_BUTTON_LIGHT end convergent event TURNS_OFF_FLOOR_BUTTON_LIGHT extends TURNS_OFF_FLOOR_BUTTON_LIGHT end convergent event turn_floor_button_light_on extends turn_floor_button_light_on end convergent 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 convergent event ELEVATOR_LEAVES_FLOOR_UP extends ELEVATOR_LEAVES_FLOOR_UP end convergent event ELEVATOR_REACHES_FLOOR_UP extends ELEVATOR_REACHES_FLOOR_UP end convergent event ELEVATOR_LEAVES_FLOOR_DOWN extends ELEVATOR_LEAVES_FLOOR_DOWN end convergent event ELEVATOR_REACHES_FLOOR_DOWN extends ELEVATOR_REACHES_FLOOR_DOWN end convergent 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 convergent event close_door extends close_door end convergent event start_move_up extends start_move_up end convergent event start_move_down extends start_move_down end convergent event stop extends stop end convergent event switch_schedule_to_up extends switch_schedule_to_up end convergent event resume_schedule_up extends resume_schedule_up end convergent event switch_schedule_to_down extends switch_schedule_to_down end convergent event resume_schedule_down extends resume_schedule_down end end " version="5">
<org.eventb.core.refinesMachine name="_OH9qsPoBEd-Ch-yEUQ-68g" org.eventb.core.target="lift26_conv_move"/>
<org.eventb.core.seesContext name="_OH9qsfoBEd-Ch-yEUQ-68g" org.eventb.core.target="ctx6_conv_utils"/>
<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="_Q8sKQPk_Ed-hoNTGCqdYog" org.eventb.core.identifier="requests"/>
<org.eventb.core.variable name="_bLy3MPluEd-1httaBm5m2g" org.eventb.core.identifier="request_served"/>
<org.eventb.core.invariant name="_5TZ5QPmVEd-4S-prP9DsJw" org.eventb.core.label="thm1" org.eventb.core.predicate="finite(DOOR_COMMAND)" org.eventb.core.theorem="true"/>
<org.eventb.core.variant name="_5TZ5QfmVEd-4S-prP9DsJw" org.eventb.core.expression="card({x∣x∈DOOR_COMMAND ∧ schedule ≠ SCHEDULER_WAIT ∧ (schedule = SCHEDULER_DOWN ⇒ snsrElevatorFloor ∉ (ctrlFloorButtonLightsSet ∪ ctrlDownButtonLightsSet)) ∧ (schedule = SCHEDULER_UP ⇒ snsrElevatorFloor ∉ (ctrlFloorButtonLightsSet ∪ ctrlUpButtonLightsSet))} ∩ {ctrlDoorCommand, DOOR_CLOSE})"/>
<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="_OIAG8PoBEd-Ch-yEUQ-68g" org.eventb.core.target="USER_PRESSES_DOWN_BUTTON"/>
</org.eventb.core.event>
<org.eventb.core.event name="_OIAG8foBEd-Ch-yEUQ-68g" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_DOWN_BUTTON">
<org.eventb.core.refinesEvent name="_OIAG8voBEd-Ch-yEUQ-68g" org.eventb.core.target="USER_RELEASES_DOWN_BUTTON"/>
</org.eventb.core.event>
<org.eventb.core.event name="_3Il25eWyEd-64JNDK1TKiQ" org.eventb.core.convergence="1" org.eventb.core.extended="true" org.eventb.core.label="TURNS_ON_DOWN_BUTTON_LIGHT">
<org.eventb.core.refinesEvent name="_OIAG8_oBEd-Ch-yEUQ-68g" org.eventb.core.target="TURNS_ON_DOWN_BUTTON_LIGHT"/>
</org.eventb.core.event>
<org.eventb.core.event name="_3Imd9eWyEd-64JNDK1TKiQ" org.eventb.core.convergence="1" org.eventb.core.extended="true" org.eventb.core.label="TURNS_OFF_DOWN_BUTTON_LIGHT">
<org.eventb.core.refinesEvent name="_OIAG9PoBEd-Ch-yEUQ-68g" org.eventb.core.target="TURNS_OFF_DOWN_BUTTON_LIGHT"/>
</org.eventb.core.event>
<org.eventb.core.event name="_3InsEuWyEd-64JNDK1TKiQ" org.eventb.core.convergence="1" org.eventb.core.extended="true" org.eventb.core.label="turn_down_button_light_on">
<org.eventb.core.refinesEvent name="_OIAuAPoBEd-Ch-yEUQ-68g" 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="1" org.eventb.core.extended="true" org.eventb.core.label="turn_down_button_light_off">
<org.eventb.core.refinesEvent name="_OIAuAfoBEd-Ch-yEUQ-68g" 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="_OIAuAvoBEd-Ch-yEUQ-68g" 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="_OIAuA_oBEd-Ch-yEUQ-68g" org.eventb.core.target="USER_RELEASES_UP_BUTTON"/>
</org.eventb.core.event>
<org.eventb.core.event name="_pvV5BuEsEd-bh-7nDQnLgQ" org.eventb.core.convergence="1" org.eventb.core.extended="true" org.eventb.core.label="TURNS_ON_UP_BUTTON_LIGHT">
<org.eventb.core.refinesEvent name="_OIBVEPoBEd-Ch-yEUQ-68g" 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="1" org.eventb.core.extended="true" org.eventb.core.label="TURNS_OFF_UP_BUTTON_LIGHT">
<org.eventb.core.refinesEvent name="_OIBVEfoBEd-Ch-yEUQ-68g" 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="1" org.eventb.core.extended="true" org.eventb.core.label="turn_up_button_light_on">
<org.eventb.core.refinesEvent name="_OIBVEvoBEd-Ch-yEUQ-68g" 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="1" org.eventb.core.extended="true" org.eventb.core.label="turn_up_button_light_off">
<org.eventb.core.refinesEvent name="_OIB8IPoBEd-Ch-yEUQ-68g" 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="_OIB8IfoBEd-Ch-yEUQ-68g" org.eventb.core.target="USER_PRESSES_FLOOR_BUTTON"/>
</org.eventb.core.event>
<org.eventb.core.event name="_OIB8IvoBEd-Ch-yEUQ-68g" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_FLOOR_BUTTON">
<org.eventb.core.refinesEvent name="_OIB8I_oBEd-Ch-yEUQ-68g" 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="1" org.eventb.core.extended="true" org.eventb.core.label="TURNS_ON_FLOOR_BUTTON_LIGHT">
<org.eventb.core.refinesEvent name="_OIB8JPoBEd-Ch-yEUQ-68g" 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="1" org.eventb.core.extended="true" org.eventb.core.label="TURNS_OFF_FLOOR_BUTTON_LIGHT">
<org.eventb.core.refinesEvent name="_OICjMPoBEd-Ch-yEUQ-68g" 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="1" org.eventb.core.extended="true" org.eventb.core.label="turn_floor_button_light_on">
<org.eventb.core.refinesEvent name="_OICjMfoBEd-Ch-yEUQ-68g" 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="1" org.eventb.core.extended="true" org.eventb.core.label="turn_floor_button_light_off">
<org.eventb.core.refinesEvent name="_OICjMvoBEd-Ch-yEUQ-68g" 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="_OIDKQPoBEd-Ch-yEUQ-68g" 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="_OIDKQfoBEd-Ch-yEUQ-68g" 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="_OIDKQvoBEd-Ch-yEUQ-68g" 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="_OIDKQ_oBEd-Ch-yEUQ-68g" 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="_OIDxUPoBEd-Ch-yEUQ-68g" 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="_OIDxUfoBEd-Ch-yEUQ-68g" org.eventb.core.target="STOP_DOOR_ENGINE"/>
</org.eventb.core.event>
<org.eventb.core.event name="_OIDxUvoBEd-Ch-yEUQ-68g" org.eventb.core.convergence="1" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_UP">
<org.eventb.core.refinesEvent name="_OIDxU_oBEd-Ch-yEUQ-68g" org.eventb.core.target="ELEVATOR_LEAVES_FLOOR_UP"/>
</org.eventb.core.event>
<org.eventb.core.event name="_OIDxVPoBEd-Ch-yEUQ-68g" org.eventb.core.convergence="1" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_UP">
<org.eventb.core.refinesEvent name="_OIEYYPoBEd-Ch-yEUQ-68g" org.eventb.core.target="ELEVATOR_REACHES_FLOOR_UP"/>
</org.eventb.core.event>
<org.eventb.core.event name="_OIEYYfoBEd-Ch-yEUQ-68g" org.eventb.core.convergence="1" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_DOWN">
<org.eventb.core.refinesEvent name="_OIEYYvoBEd-Ch-yEUQ-68g" org.eventb.core.target="ELEVATOR_LEAVES_FLOOR_DOWN"/>
</org.eventb.core.event>
<org.eventb.core.event name="_OIEYY_oBEd-Ch-yEUQ-68g" org.eventb.core.convergence="1" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_DOWN">
<org.eventb.core.refinesEvent name="_OIEYZPoBEd-Ch-yEUQ-68g" 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="1" org.eventb.core.extended="true" org.eventb.core.label="STOP_CABLE_ENGINE">
<org.eventb.core.refinesEvent name="_OIE_cPoBEd-Ch-yEUQ-68g" 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="_OIE_cfoBEd-Ch-yEUQ-68g" 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="_OIE_cvoBEd-Ch-yEUQ-68g" org.eventb.core.target="stop_door"/>
</org.eventb.core.event>
<org.eventb.core.event name="_HKjNMtqzEd-7IuFxCL4SWw" org.eventb.core.convergence="1" org.eventb.core.extended="true" org.eventb.core.label="close_door">
<org.eventb.core.refinesEvent name="_OIFmgPoBEd-Ch-yEUQ-68g" org.eventb.core.target="close_door"/>
</org.eventb.core.event>
<org.eventb.core.event name="_yC2soNqwEd-O4vbSPlarTw" org.eventb.core.convergence="1" org.eventb.core.extended="true" org.eventb.core.label="start_move_up">
<org.eventb.core.refinesEvent name="_OIFmgfoBEd-Ch-yEUQ-68g" org.eventb.core.target="start_move_up"/>
</org.eventb.core.event>
<org.eventb.core.event name="_yC36wNqwEd-O4vbSPlarTw" org.eventb.core.convergence="1" org.eventb.core.extended="true" org.eventb.core.label="start_move_down">
<org.eventb.core.refinesEvent name="_OIFmgvoBEd-Ch-yEUQ-68g" org.eventb.core.target="start_move_down"/>
</org.eventb.core.event>
<org.eventb.core.event name="_yC5I4dqwEd-O4vbSPlarTw" org.eventb.core.convergence="1" org.eventb.core.extended="true" org.eventb.core.label="stop">
<org.eventb.core.refinesEvent name="_OIFmg_oBEd-Ch-yEUQ-68g" org.eventb.core.target="stop"/>
</org.eventb.core.event>
<org.eventb.core.event name="_Utq4gO5-Ed-dEtybZVK09Q" org.eventb.core.convergence="1" org.eventb.core.extended="true" org.eventb.core.label="switch_schedule_to_up">
<org.eventb.core.refinesEvent name="_OIGNkPoBEd-Ch-yEUQ-68g" org.eventb.core.target="switch_schedule_to_up"/>
</org.eventb.core.event>
<org.eventb.core.event name="_Utrfle5-Ed-dEtybZVK09Q" org.eventb.core.convergence="1" org.eventb.core.extended="true" org.eventb.core.label="resume_schedule_up">
<org.eventb.core.refinesEvent name="_OIGNkfoBEd-Ch-yEUQ-68g" org.eventb.core.target="resume_schedule_up"/>
</org.eventb.core.event>
<org.eventb.core.event name="_Utstsu5-Ed-dEtybZVK09Q" org.eventb.core.convergence="1" org.eventb.core.extended="true" org.eventb.core.label="switch_schedule_to_down">
<org.eventb.core.refinesEvent name="_OIGNkvoBEd-Ch-yEUQ-68g" org.eventb.core.target="switch_schedule_to_down"/>
</org.eventb.core.event>
<org.eventb.core.event name="_Utt70e5-Ed-dEtybZVK09Q" org.eventb.core.convergence="1" org.eventb.core.extended="true" org.eventb.core.label="resume_schedule_down">
<org.eventb.core.refinesEvent name="_OIG0oPoBEd-Ch-yEUQ-68g" org.eventb.core.target="resume_schedule_down"/>
</org.eventb.core.event>
</org.eventb.core.machineFile>