/
lift03_door_engine.bum
43 lines (43 loc) · 5.89 KB
/
lift03_door_engine.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
<?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="1290097252658" org.eventb.texttools.text_representation="machine lift03_door_engine refines lift02_main_engine sees ctx3_door_engine variables floor ctrlCableCommand moved ctrlDoorCommand invariants @inv3_1 ctrlDoorCommand ∈ DOOR_COMMAND @inv3_3 ctrlCableCommand ≠ CABLE_STOP ⇒ ctrlDoorCommand = DOOR_CLOSE events event INITIALISATION extends INITIALISATION then @act3_1 ctrlDoorCommand ≔ DOOR_STOP end anticipated event open_door where @grd3_1 ctrlCableCommand = CABLE_STOP then @act3_1 ctrlDoorCommand ≔ DOOR_OPEN end anticipated event stop_door where @grd3_1 ctrlDoorCommand = DOOR_OPEN then @act3_1 ctrlDoorCommand ≔ DOOR_STOP end anticipated event close_door where @grd3_1 ctrlDoorCommand = DOOR_STOP then @act3_1 ctrlDoorCommand ≔ DOOR_CLOSE end anticipated event start_move_up extends start_move_up where @grd3_1 ctrlDoorCommand = DOOR_CLOSE end anticipated event move_up extends move_up end anticipated event start_move_down extends start_move_down where @grd3_1 ctrlDoorCommand = DOOR_CLOSE end anticipated event move_down extends move_down end anticipated event stop extends stop end end " version="5">
<org.eventb.core.refinesMachine name="_0F-1cPMvEd-IqfVXadHBVg" org.eventb.core.target="lift02_main_engine"/>
<org.eventb.core.seesContext name="_0F-1cfMvEd-IqfVXadHBVg" org.eventb.core.target="ctx3_door_engine"/>
<org.eventb.core.variable name="_9uEEsNd9Ed-Dle0at0Xgqg" org.eventb.core.identifier="floor"/>
<org.eventb.core.variable name="_1cMDMtd_Ed-Dle0at0Xgqg" org.eventb.core.identifier="ctrlCableCommand"/>
<org.eventb.core.variable name="_yC03ctqwEd-O4vbSPlarTw" org.eventb.core.identifier="moved"/>
<org.eventb.core.variable name="_HKh_EtqzEd-7IuFxCL4SWw" org.eventb.core.identifier="ctrlDoorCommand"/>
<org.eventb.core.invariant name="_HKimINqzEd-7IuFxCL4SWw" org.eventb.core.label="inv3_1" org.eventb.core.predicate="ctrlDoorCommand ∈ DOOR_COMMAND"/>
<org.eventb.core.invariant name="_Sjk-INq3Ed-AAt710HomgA" org.eventb.core.label="inv3_3" org.eventb.core.predicate="ctrlCableCommand ≠ CABLE_STOP ⇒ 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.action name="_HKimIdqzEd-7IuFxCL4SWw" org.eventb.core.assignment="ctrlDoorCommand ≔ DOOR_STOP" org.eventb.core.label="act3_1"/>
</org.eventb.core.event>
<org.eventb.core.event name="_HKimItqzEd-7IuFxCL4SWw" org.eventb.core.convergence="2" org.eventb.core.extended="false" org.eventb.core.label="open_door">
<org.eventb.core.guard name="_HKjNMNqzEd-7IuFxCL4SWw" org.eventb.core.label="grd3_1" org.eventb.core.predicate="ctrlCableCommand = CABLE_STOP"/>
<org.eventb.core.action name="_HKjNMdqzEd-7IuFxCL4SWw" org.eventb.core.assignment="ctrlDoorCommand ≔ DOOR_OPEN" org.eventb.core.label="act3_1"/>
</org.eventb.core.event>
<org.eventb.core.event name="_SjmMQNq3Ed-AAt710HomgA" org.eventb.core.convergence="2" org.eventb.core.extended="false" org.eventb.core.label="stop_door">
<org.eventb.core.guard name="_SjmzUNq3Ed-AAt710HomgA" org.eventb.core.label="grd3_1" org.eventb.core.predicate="ctrlDoorCommand = DOOR_OPEN"/>
<org.eventb.core.action name="_SjmzUdq3Ed-AAt710HomgA" org.eventb.core.assignment="ctrlDoorCommand ≔ DOOR_STOP" org.eventb.core.label="act3_1"/>
</org.eventb.core.event>
<org.eventb.core.event name="_HKjNMtqzEd-7IuFxCL4SWw" org.eventb.core.convergence="2" org.eventb.core.extended="false" org.eventb.core.label="close_door">
<org.eventb.core.guard name="_HKj0QNqzEd-7IuFxCL4SWw" org.eventb.core.label="grd3_1" org.eventb.core.predicate="ctrlDoorCommand = DOOR_STOP"/>
<org.eventb.core.action name="_HKj0QdqzEd-7IuFxCL4SWw" org.eventb.core.assignment="ctrlDoorCommand ≔ DOOR_CLOSE" org.eventb.core.label="act3_1"/>
</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="_0GAqoPMvEd-IqfVXadHBVg" org.eventb.core.target="start_move_up"/>
<org.eventb.core.guard name="_SjnaYdq3Ed-AAt710HomgA" org.eventb.core.label="grd3_1" org.eventb.core.predicate="ctrlDoorCommand = DOOR_CLOSE"/>
</org.eventb.core.event>
<org.eventb.core.event name="_9uFS0Nd9Ed-Dle0at0Xgqg" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="move_up">
<org.eventb.core.refinesEvent name="_0GBRsPMvEd-IqfVXadHBVg" org.eventb.core.target="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="_0GBRsfMvEd-IqfVXadHBVg" org.eventb.core.target="start_move_down"/>
<org.eventb.core.guard name="_SjoBcdq3Ed-AAt710HomgA" org.eventb.core.label="grd3_1" org.eventb.core.predicate="ctrlDoorCommand = DOOR_CLOSE"/>
</org.eventb.core.event>
<org.eventb.core.event name="_9uF54dd9Ed-Dle0at0Xgqg" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="move_down">
<org.eventb.core.refinesEvent name="_0GB4wPMvEd-IqfVXadHBVg" org.eventb.core.target="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="_0GB4wfMvEd-IqfVXadHBVg" org.eventb.core.target="stop"/>
</org.eventb.core.event>
</org.eventb.core.machineFile>