Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

deleted unused files

  • Loading branch information...
commit f6759a3151933992d3acef1be110d548f9d50220 1 parent 7b746f2
Adrian Friedli authored
View
523 rodin/lift10_conv_lights.bcm
0 additions, 523 deletions not shown
View
786 rodin/lift10_conv_lights.bpo
0 additions, 786 deletions not shown
View
9,013 rodin/lift10_conv_lights.bpr
0 additions, 9,013 deletions not shown
View
37 rodin/lift10_conv_lights.bps
@@ -1,37 +0,0 @@
-<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.psFile>
-<org.eventb.core.psStatus name="FIN" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="TURNS_ON_DOWN_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="TURNS_OFF_DOWN_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="turn_down_button_light_on/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="turn_down_button_light_off/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="TURNS_ON_UP_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="TURNS_OFF_UP_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="turn_up_button_light_on/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="turn_up_button_light_off/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="TURNS_ON_FLOOR_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="TURNS_OFF_FLOOR_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="turn_floor_button_light_on/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="turn_floor_button_light_off/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_OPENS_WHEN_CLOSED/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_OPENS_WHEN_HALF/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_CLOSES_WHEN_OPENED/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_CLOSES_WHEN_HALF/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_CLOSES_WHEN_CLOSED/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="STOP_DOOR_ENGINE/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_LEAVES_FLOOR_UP/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_REACHES_FLOOR_UP/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_LEAVES_FLOOR_DOWN/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_REACHES_FLOOR_DOWN/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="STOP_CABLE_ENGINE/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="open_door/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="stop_door/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="close_door/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="start_move_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="start_move_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="stop/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="switch_schedule_to_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="resume_schedule_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="switch_schedule_to_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="resume_schedule_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-</org.eventb.core.psFile>
View
152 rodin/lift10_conv_lights.bum
@@ -1,152 +0,0 @@
-<?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="1290783933679" org.eventb.texttools.text_representation="machine lift10_conv refines lift09_scheduler sees ctx5_scheduler&#10;&#10;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&#10;&#10;variant snsrFloorButtonsSet∖ ctrlFloorButtonLightsSet&#10;&#10;events&#10; event INITIALISATION extends INITIALISATION&#10; end&#10;&#10; event USER_PRESSES_DOWN_BUTTON extends USER_PRESSES_DOWN_BUTTON&#10; end&#10;&#10; event USER_RELEASES_DOWN_BUTTON extends USER_RELEASES_DOWN_BUTTON&#10; end&#10;&#10; anticipated event TURNS_ON_DOWN_BUTTON_LIGHT extends TURNS_ON_DOWN_BUTTON_LIGHT&#10; end&#10;&#10; anticipated event TURNS_OFF_DOWN_BUTTON_LIGHT extends TURNS_OFF_DOWN_BUTTON_LIGHT&#10; end&#10;&#10; anticipated event turn_down_button_light_on extends turn_down_button_light_on&#10; end&#10;&#10; anticipated event turn_down_button_light_off extends turn_down_button_light_off&#10; end&#10;&#10; event USER_PRESSES_UP_BUTTON extends USER_PRESSES_UP_BUTTON&#10; end&#10;&#10; event USER_RELEASES_UP_BUTTON extends USER_RELEASES_UP_BUTTON&#10; end&#10;&#10; anticipated event TURNS_ON_UP_BUTTON_LIGHT extends TURNS_ON_UP_BUTTON_LIGHT&#10; end&#10;&#10; anticipated event TURNS_OFF_UP_BUTTON_LIGHT extends TURNS_OFF_UP_BUTTON_LIGHT&#10; end&#10;&#10; anticipated event turn_up_button_light_on extends turn_up_button_light_on&#10; end&#10;&#10; anticipated event turn_up_button_light_off extends turn_up_button_light_off&#10; end&#10;&#10; event USER_PRESSES_FLOOR_BUTTON extends USER_PRESSES_FLOOR_BUTTON&#10; end&#10;&#10; event USER_RELEASES_FLOOR_BUTTON extends USER_RELEASES_FLOOR_BUTTON&#10; end&#10;&#10; anticipated event TURNS_ON_FLOOR_BUTTON_LIGHT extends TURNS_ON_FLOOR_BUTTON_LIGHT&#10; end&#10;&#10; anticipated event TURNS_OFF_FLOOR_BUTTON_LIGHT extends TURNS_OFF_FLOOR_BUTTON_LIGHT&#10; end&#10;&#10; convergent event turn_floor_button_light_on extends turn_floor_button_light_on&#10; end&#10;&#10; anticipated event turn_floor_button_light_off extends turn_floor_button_light_off&#10; end&#10;&#10; anticipated event DOOR_OPENS_WHEN_CLOSED extends DOOR_OPENS_WHEN_CLOSED&#10; end&#10;&#10; anticipated event DOOR_OPENS_WHEN_HALF extends DOOR_OPENS_WHEN_HALF&#10; end&#10;&#10; anticipated event DOOR_CLOSES_WHEN_OPENED extends DOOR_CLOSES_WHEN_OPENED&#10; end&#10;&#10; anticipated event DOOR_CLOSES_WHEN_HALF extends DOOR_CLOSES_WHEN_HALF&#10; end&#10;&#10; anticipated event DOOR_CLOSES_WHEN_CLOSED extends DOOR_CLOSES_WHEN_CLOSED&#10; end&#10;&#10; anticipated event STOP_DOOR_ENGINE extends STOP_DOOR_ENGINE&#10; end&#10;&#10; anticipated event ELEVATOR_LEAVES_FLOOR_UP extends ELEVATOR_LEAVES_FLOOR_UP&#10; end&#10;&#10; anticipated event ELEVATOR_REACHES_FLOOR_UP extends ELEVATOR_REACHES_FLOOR_UP&#10; end&#10;&#10; anticipated event ELEVATOR_LEAVES_FLOOR_DOWN extends ELEVATOR_LEAVES_FLOOR_DOWN&#10; end&#10;&#10; anticipated event ELEVATOR_REACHES_FLOOR_DOWN extends ELEVATOR_REACHES_FLOOR_DOWN&#10; end&#10;&#10; anticipated event STOP_CABLE_ENGINE extends STOP_CABLE_ENGINE&#10; end&#10;&#10; anticipated event open_door extends open_door&#10; end&#10;&#10; anticipated event stop_door extends stop_door&#10; end&#10;&#10; anticipated event close_door extends close_door&#10; end&#10;&#10; anticipated event start_move_up extends start_move_up&#10; end&#10;&#10; anticipated event start_move_down extends start_move_down&#10; end&#10;&#10; anticipated event stop extends stop&#10; end&#10;&#10; anticipated event switch_schedule_to_up extends switch_schedule_to_up&#10; end&#10;&#10; anticipated event resume_schedule_up extends resume_schedule_up&#10; end&#10;&#10; anticipated event switch_schedule_to_down extends switch_schedule_to_down&#10; end&#10;&#10; anticipated event resume_schedule_down extends resume_schedule_down&#10; end&#10;end&#10;" version="5">
-<org.eventb.core.refinesMachine name="_njudMPluEd-1httaBm5m2g" org.eventb.core.target="lift09_scheduler"/>
-<org.eventb.core.seesContext name="_njudMfluEd-1httaBm5m2g" 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="_8ov3UPk7Ed-WtNZH8d5nSA" org.eventb.core.identifier="requests"/>
-<org.eventb.core.variable name="_njwSYPluEd-1httaBm5m2g" org.eventb.core.identifier="request_served"/>
-<org.eventb.core.variant name="_us4UgPfqEd-vgams47i3xA" org.eventb.core.expression="snsrFloorButtonsSet∖ ctrlFloorButtonLightsSet"/>
-<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="_njwSYfluEd-1httaBm5m2g" org.eventb.core.target="USER_PRESSES_DOWN_BUTTON"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_njw5cPluEd-1httaBm5m2g" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_DOWN_BUTTON">
-<org.eventb.core.refinesEvent name="_njw5cfluEd-1httaBm5m2g" 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="_njw5cvluEd-1httaBm5m2g" 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="_njw5c_luEd-1httaBm5m2g" 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="_njxggPluEd-1httaBm5m2g" 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="_njxggfluEd-1httaBm5m2g" 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="_njxggvluEd-1httaBm5m2g" org.eventb.core.target="USER_PRESSES_UP_BUTTON"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_3Io6M-WyEd-64JNDK1TKiQ" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_UP_BUTTON">
-<org.eventb.core.refinesEvent name="_njyHkPluEd-1httaBm5m2g" 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="_njyHkfluEd-1httaBm5m2g" 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="_njyHkvluEd-1httaBm5m2g" 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="_njyuoPluEd-1httaBm5m2g" 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="_njyuofluEd-1httaBm5m2g" 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="_njyuovluEd-1httaBm5m2g" org.eventb.core.target="USER_PRESSES_FLOOR_BUTTON"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_njyuo_luEd-1httaBm5m2g" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_FLOOR_BUTTON">
-<org.eventb.core.refinesEvent name="_njzVsPluEd-1httaBm5m2g" 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="_njzVsfluEd-1httaBm5m2g" 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="_njzVsvluEd-1httaBm5m2g" 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="_njz8wPluEd-1httaBm5m2g" 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="_njz8wfluEd-1httaBm5m2g" 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="_njz8wvluEd-1httaBm5m2g" 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="_nj0j0PluEd-1httaBm5m2g" 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="_nj0j0fluEd-1httaBm5m2g" 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="_nj0j0vluEd-1httaBm5m2g" 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="_nj1K4PluEd-1httaBm5m2g" 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="_nj1K4fluEd-1httaBm5m2g" org.eventb.core.target="STOP_DOOR_ENGINE"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_nj1K4vluEd-1httaBm5m2g" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_UP">
-<org.eventb.core.refinesEvent name="_nj1K4_luEd-1httaBm5m2g" org.eventb.core.target="ELEVATOR_LEAVES_FLOOR_UP"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_nj1K5PluEd-1httaBm5m2g" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_UP">
-<org.eventb.core.refinesEvent name="_nj1x8PluEd-1httaBm5m2g" org.eventb.core.target="ELEVATOR_REACHES_FLOOR_UP"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_nj1x8fluEd-1httaBm5m2g" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_DOWN">
-<org.eventb.core.refinesEvent name="_nj1x8vluEd-1httaBm5m2g" org.eventb.core.target="ELEVATOR_LEAVES_FLOOR_DOWN"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_nj1x8_luEd-1httaBm5m2g" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_DOWN">
-<org.eventb.core.refinesEvent name="_nj1x9PluEd-1httaBm5m2g" 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="_nj2ZAPluEd-1httaBm5m2g" 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="_nj2ZAfluEd-1httaBm5m2g" 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="_nj2ZAvluEd-1httaBm5m2g" 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="_nj3AEPluEd-1httaBm5m2g" 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="_nj3AEfluEd-1httaBm5m2g" 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="_nj3AEvluEd-1httaBm5m2g" 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="_nj3nIPluEd-1httaBm5m2g" 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="_nj3nIfluEd-1httaBm5m2g" 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="_nj3nIvluEd-1httaBm5m2g" 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="_nj4OMPluEd-1httaBm5m2g" 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="_nj4OMfluEd-1httaBm5m2g" org.eventb.core.target="resume_schedule_down"/>
-</org.eventb.core.event>
-</org.eventb.core.machineFile>
View
523 rodin/lift11_conv_lights.bcm
0 additions, 523 deletions not shown
View
779 rodin/lift11_conv_lights.bpo
0 additions, 779 deletions not shown
View
658 rodin/lift11_conv_lights.bpr
@@ -1,658 +0,0 @@
-<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.prFile version="1">
-<org.eventb.core.prProof name="FIN" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10,p11,p12,p13,p14,p15,p16,p17,p18,p19,p20,p21,p22,p23,p24,p25,p26,p27,p28,p29,p30,p31,p32,p33,p34,p35,p36,p37,p38,p39,p40,p41,p42,p43,p44,p45,p46,p47,p48,p49,p50,p51,p52,p53,p54,p55,p56,p57,p58,p59,p60,p61" org.eventb.core.prSets="CABLE_COMMAND,DOOR_COMMAND,DOOR_POSITION,SCHEDULER_STRATEGY">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0">
-<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p10" org.eventb.core.prInfHyps="p62"/>
-<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p10"/>
-<org.eventb.core.prHypAction name="FORWARD_INF2" org.eventb.core.prHyps="p8" org.eventb.core.prInfHyps="p63"/>
-<org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p8"/>
-<org.eventb.core.prHypAction name="FORWARD_INF4" org.eventb.core.prHyps="p50" org.eventb.core.prInfHyps="p64"/>
-<org.eventb.core.prHypAction name="HIDE5" org.eventb.core.prHyps="p50"/>
-<org.eventb.core.prHypAction name="FORWARD_INF6" org.eventb.core.prHyps="p55" org.eventb.core.prInfHyps="p65"/>
-<org.eventb.core.prHypAction name="HIDE7" org.eventb.core.prHyps="p55"/>
-<org.eventb.core.prHypAction name="FORWARD_INF8" org.eventb.core.prHyps="p15" org.eventb.core.prInfHyps="p66"/>
-<org.eventb.core.prHypAction name="HIDE9" org.eventb.core.prHyps="p15"/>
-<org.eventb.core.prHypAction name="FORWARD_INF10" org.eventb.core.prHyps="p24" org.eventb.core.prInfHyps="p67"/>
-<org.eventb.core.prHypAction name="HIDE11" org.eventb.core.prHyps="p24"/>
-<org.eventb.core.prHypAction name="FORWARD_INF12" org.eventb.core.prHyps="p2" org.eventb.core.prInfHyps="p68"/>
-<org.eventb.core.prHypAction name="HIDE13" org.eventb.core.prHyps="p2"/>
-<org.eventb.core.prHypAction name="FORWARD_INF14" org.eventb.core.prHyps="p20" org.eventb.core.prInfHyps="p69"/>
-<org.eventb.core.prHypAction name="HIDE15" org.eventb.core.prHyps="p20"/>
-<org.eventb.core.prHypAction name="FORWARD_INF16" org.eventb.core.prHyps="p18" org.eventb.core.prInfHyps="p70"/>
-<org.eventb.core.prHypAction name="HIDE17" org.eventb.core.prHyps="p18"/>
-<org.eventb.core.prHypAction name="FORWARD_INF18" org.eventb.core.prHyps="p33" org.eventb.core.prInfHyps="p71"/>
-<org.eventb.core.prHypAction name="HIDE19" org.eventb.core.prHyps="p33"/>
-<org.eventb.core.prHypAction name="FORWARD_INF20" org.eventb.core.prHyps="p60" org.eventb.core.prInfHyps="p72"/>
-<org.eventb.core.prHypAction name="HIDE21" org.eventb.core.prHyps="p60"/>
-<org.eventb.core.prHypAction name="FORWARD_INF22" org.eventb.core.prHyps="p22" org.eventb.core.prInfHyps="p73"/>
-<org.eventb.core.prHypAction name="HIDE23" org.eventb.core.prHyps="p22"/>
-<org.eventb.core.prHypAction name="FORWARD_INF24" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p74"/>
-<org.eventb.core.prHypAction name="HIDE25" org.eventb.core.prHyps="p1"/>
-<org.eventb.core.prHypAction name="FORWARD_INF26" org.eventb.core.prHyps="p39" org.eventb.core.prInfHyps="p75"/>
-<org.eventb.core.prHypAction name="HIDE27" org.eventb.core.prHyps="p39"/>
-<org.eventb.core.prHypAction name="FORWARD_INF28" org.eventb.core.prHyps="p53" org.eventb.core.prInfHyps="p76"/>
-<org.eventb.core.prHypAction name="HIDE29" org.eventb.core.prHyps="p53"/>
-<org.eventb.core.prRule name="org.eventb.core.seqprover.typeRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0">
-<org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p77"/>
-<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p78"/>
-<org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p79"/>
-<org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p80"/>
-<org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p81"/>
-<org.eventb.core.prHypAction name="HIDE5" org.eventb.core.prHyps="p82"/>
-<org.eventb.core.prHypAction name="HIDE6" org.eventb.core.prHyps="p83"/>
-<org.eventb.core.prHypAction name="HIDE7" org.eventb.core.prHyps="p84"/>
-<org.eventb.core.prHypAction name="HIDE8" org.eventb.core.prHyps="p85"/>
-<org.eventb.core.prHypAction name="HIDE9" org.eventb.core.prHyps="p86"/>
-<org.eventb.core.prRule name="com.clearsy.atelierb.provers.core.externalML" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p26,p3,p44,p34,p40,p48,p29,p43,p12,p49,p9,p7,p14,p16,p56,p36,p38,p57,p28,p31,p42,p52,p61,p51,p4,p59,p46,p35,p23,p47,p37,p17,p6,p32,p5,p13,p41,p11,p25,p45,p27,p54,p30,p19,p58,p21,p62,p63,p64,p65,p66,p67,p68,p69,p70,p71,p72,p73,p74,p75,p76">
-<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
-</org.eventb.core.prRule>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="CABLE_STOP" org.eventb.core.type="CABLE_COMMAND"/>
-<org.eventb.core.prIdent name="CABLE_UNWIND" org.eventb.core.type="CABLE_COMMAND"/>
-<org.eventb.core.prIdent name="CABLE_WIND" org.eventb.core.type="CABLE_COMMAND"/>
-<org.eventb.core.prIdent name="DOOR_CLOSE" org.eventb.core.type="DOOR_COMMAND"/>
-<org.eventb.core.prIdent name="DOOR_CLOSED" org.eventb.core.type="DOOR_POSITION"/>
-<org.eventb.core.prIdent name="DOOR_HALF" org.eventb.core.type="DOOR_POSITION"/>
-<org.eventb.core.prIdent name="DOOR_OPEN" org.eventb.core.type="DOOR_COMMAND"/>
-<org.eventb.core.prIdent name="DOOR_OPENED" org.eventb.core.type="DOOR_POSITION"/>
-<org.eventb.core.prIdent name="DOOR_STOP" org.eventb.core.type="DOOR_COMMAND"/>
-<org.eventb.core.prIdent name="LAST_FLOOR" org.eventb.core.type="ℤ"/>
-<org.eventb.core.prIdent name="PhyCableEngine" org.eventb.core.type="CABLE_COMMAND"/>
-<org.eventb.core.prIdent name="PhyDoorEngine" org.eventb.core.type="DOOR_COMMAND"/>
-<org.eventb.core.prIdent name="PhyDoorPosition" org.eventb.core.type="DOOR_POSITION"/>
-<org.eventb.core.prIdent name="PhyDownButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="PhyDownButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="PhyElevatorBetweenTwoFloors" org.eventb.core.type="BOOL"/>
-<org.eventb.core.prIdent name="PhyElevatorFloor" org.eventb.core.type="ℤ"/>
-<org.eventb.core.prIdent name="PhyFloorButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="PhyFloorButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="PhyUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="PhyUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="SCHEDULER_DOWN" org.eventb.core.type="SCHEDULER_STRATEGY"/>
-<org.eventb.core.prIdent name="SCHEDULER_UP" org.eventb.core.type="SCHEDULER_STRATEGY"/>
-<org.eventb.core.prIdent name="SCHEDULER_WAIT" org.eventb.core.type="SCHEDULER_STRATEGY"/>
-<org.eventb.core.prIdent name="b2n" org.eventb.core.type="ℙ(BOOL×ℤ)"/>
-<org.eventb.core.prIdent name="ctrlCableCommand" org.eventb.core.type="CABLE_COMMAND"/>
-<org.eventb.core.prIdent name="ctrlDoorCommand" org.eventb.core.type="DOOR_COMMAND"/>
-<org.eventb.core.prIdent name="ctrlDownButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="ctrlFloorButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="last_schedule" org.eventb.core.type="SCHEDULER_STRATEGY"/>
-<org.eventb.core.prIdent name="last_stop" org.eventb.core.type="ℤ"/>
-<org.eventb.core.prIdent name="requests" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="schedule" org.eventb.core.type="SCHEDULER_STRATEGY"/>
-<org.eventb.core.prIdent name="snsrCableEngine" org.eventb.core.type="CABLE_COMMAND"/>
-<org.eventb.core.prIdent name="snsrDoorEngine" org.eventb.core.type="DOOR_COMMAND"/>
-<org.eventb.core.prIdent name="snsrDoorPosition" org.eventb.core.type="DOOR_POSITION"/>
-<org.eventb.core.prIdent name="snsrDownButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrElevatorFloor" org.eventb.core.type="ℤ"/>
-<org.eventb.core.prIdent name="snsrFloorButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP∧PhyCableEngine≠CABLE_STOP⇒snsrElevatorFloor∈requests"/>
-<org.eventb.core.prPred name="p2" org.eventb.core.predicate="ctrlCableCommand≠CABLE_STOP⇒snsrDoorPosition=DOOR_CLOSED"/>
-<org.eventb.core.prPred name="p70" org.eventb.core.predicate="¬PhyCableEngine=CABLE_STOP⇒PhyDoorPosition=DOOR_CLOSED"/>
-<org.eventb.core.prPred name="p3" org.eventb.core.predicate="b2n∈BOOL ⤖ {0,1}"/>
-<org.eventb.core.prPred name="p4" org.eventb.core.predicate="snsrFloorButtonsSet⊆0 ‥ LAST_FLOOR"/>
-<org.eventb.core.prPred name="p5" org.eventb.core.predicate="snsrDownButtonsSet⊆1 ‥ LAST_FLOOR"/>
-<org.eventb.core.prPred name="p6" org.eventb.core.predicate="ctrlUpButtonLightsSet⊆0 ‥ (LAST_FLOOR − 1)"/>
-<org.eventb.core.prPred name="p7" org.eventb.core.predicate="PhyElevatorFloor∈ℕ"/>
-<org.eventb.core.prPred name="p82" org.eventb.core.predicate="PhyDoorEngine∈DOOR_COMMAND"/>
-<org.eventb.core.prPred name="p8" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=TRUE⇒PhyElevatorFloor≠LAST_FLOOR"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="finite(snsrUpButtonsSet ∖ ctrlUpButtonLightsSet)"/>
-<org.eventb.core.prPred name="p67" org.eventb.core.predicate="¬ctrlCableCommand=CABLE_STOP⇒snsrDoorEngine=DOOR_CLOSE"/>
-<org.eventb.core.prPred name="p9" org.eventb.core.predicate="partition(SCHEDULER_STRATEGY,{SCHEDULER_UP},{SCHEDULER_DOWN},{SCHEDULER_WAIT})"/>
-<org.eventb.core.prPred name="p78" org.eventb.core.predicate="ctrlDoorCommand∈DOOR_COMMAND"/>
-<org.eventb.core.prPred name="p66" org.eventb.core.predicate="¬snsrCableEngine=CABLE_STOP⇒ctrlDoorCommand=DOOR_CLOSE"/>
-<org.eventb.core.prPred name="p10" org.eventb.core.predicate="ctrlCableCommand≠CABLE_STOP⇒ctrlDoorCommand=DOOR_CLOSE"/>
-<org.eventb.core.prPred name="p11" org.eventb.core.predicate="ctrlDownButtonLightsSet⊆1 ‥ LAST_FLOOR"/>
-<org.eventb.core.prPred name="p12" org.eventb.core.predicate="partition(DOOR_COMMAND,{DOOR_STOP},{DOOR_OPEN},{DOOR_CLOSE})"/>
-<org.eventb.core.prPred name="p15" org.eventb.core.predicate="snsrCableEngine≠CABLE_STOP⇒ctrlDoorCommand=DOOR_CLOSE"/>
-<org.eventb.core.prPred name="p14" org.eventb.core.predicate="PhyElevatorFloor≤LAST_FLOOR"/>
-<org.eventb.core.prPred name="p13" org.eventb.core.predicate="snsrDownButtonsSet=PhyDownButtonsSet"/>
-<org.eventb.core.prPred name="p83" org.eventb.core.predicate="PhyDoorPosition∈DOOR_POSITION"/>
-<org.eventb.core.prPred name="p16" org.eventb.core.predicate="PhyElevatorFloor&lt;LAST_FLOOR∨0&lt;PhyElevatorFloor"/>
-<org.eventb.core.prPred name="p69" org.eventb.core.predicate="¬PhyCableEngine=CABLE_STOP⇒PhyDoorEngine=DOOR_CLOSE"/>
-<org.eventb.core.prPred name="p80" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors∈BOOL"/>
-<org.eventb.core.prPred name="p71" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP∧PhyElevatorFloor=LAST_FLOOR⇒¬schedule=SCHEDULER_UP"/>
-<org.eventb.core.prPred name="p85" org.eventb.core.predicate="snsrDoorPosition∈DOOR_POSITION"/>
-<org.eventb.core.prPred name="p68" org.eventb.core.predicate="¬ctrlCableCommand=CABLE_STOP⇒snsrDoorPosition=DOOR_CLOSED"/>
-<org.eventb.core.prPred name="p18" org.eventb.core.predicate="PhyCableEngine≠CABLE_STOP⇒PhyDoorPosition=DOOR_CLOSED"/>
-<org.eventb.core.prPred name="p17" org.eventb.core.predicate="PhyUpButtonLightsSet⊆0 ‥ (LAST_FLOOR − 1)"/>
-<org.eventb.core.prPred name="p19" org.eventb.core.predicate="requests=(∅ ⦂ ℙ(ℤ))⇒PhyCableEngine=CABLE_STOP"/>
-<org.eventb.core.prPred name="p20" org.eventb.core.predicate="PhyCableEngine≠CABLE_STOP⇒PhyDoorEngine=DOOR_CLOSE"/>
-<org.eventb.core.prPred name="p21" org.eventb.core.predicate="ctrlCableCommand=CABLE_UNWIND⇒schedule=SCHEDULER_DOWN"/>
-<org.eventb.core.prPred name="p22" org.eventb.core.predicate="schedule≠SCHEDULER_WAIT∧ctrlCableCommand=CABLE_STOP⇒requests ∖ {snsrElevatorFloor}≠(∅ ⦂ ℙ(ℤ))"/>
-<org.eventb.core.prPred name="p23" org.eventb.core.predicate="PhyUpButtonsSet⊆0 ‥ (LAST_FLOOR − 1)"/>
-<org.eventb.core.prPred name="p24" org.eventb.core.predicate="ctrlCableCommand≠CABLE_STOP⇒snsrDoorEngine=DOOR_CLOSE"/>
-<org.eventb.core.prPred name="p25" org.eventb.core.predicate="requests⊆0 ‥ LAST_FLOOR"/>
-<org.eventb.core.prPred name="p26" org.eventb.core.predicate="LAST_FLOOR∈ℕ1"/>
-<org.eventb.core.prPred name="p74" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP∧¬PhyCableEngine=CABLE_STOP⇒snsrElevatorFloor∈requests"/>
-<org.eventb.core.prPred name="p27" org.eventb.core.predicate="last_schedule∈{SCHEDULER_UP,SCHEDULER_DOWN}"/>
-<org.eventb.core.prPred name="p28" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=FALSE⇒snsrElevatorFloor=PhyElevatorFloor"/>
-<org.eventb.core.prPred name="p29" org.eventb.core.predicate="FALSE∈dom(b2n)"/>
-<org.eventb.core.prPred name="p30" org.eventb.core.predicate="requests=(∅ ⦂ ℙ(ℤ))⇒schedule=SCHEDULER_WAIT"/>
-<org.eventb.core.prPred name="p31" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP⇒PhyElevatorFloor=snsrElevatorFloor"/>
-<org.eventb.core.prPred name="p75" org.eventb.core.predicate="¬schedule=SCHEDULER_WAIT⇒schedule=last_schedule"/>
-<org.eventb.core.prPred name="p32" org.eventb.core.predicate="PhyDownButtonsSet⊆1 ‥ LAST_FLOOR"/>
-<org.eventb.core.prPred name="p33" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP∧PhyElevatorFloor=LAST_FLOOR⇒schedule≠SCHEDULER_UP"/>
-<org.eventb.core.prPred name="p34" org.eventb.core.predicate="TRUE∈dom(b2n)"/>
-<org.eventb.core.prPred name="p35" org.eventb.core.predicate="ctrlFloorButtonLightsSet⊆0 ‥ LAST_FLOOR"/>
-<org.eventb.core.prPred name="p36" org.eventb.core.predicate="snsrCableEngine=PhyCableEngine"/>
-<org.eventb.core.prPred name="p37" org.eventb.core.predicate="snsrUpButtonsSet=PhyUpButtonsSet"/>
-<org.eventb.core.prPred name="p38" org.eventb.core.predicate="snsrElevatorFloor∈−1 ‥ LAST_FLOOR"/>
-<org.eventb.core.prPred name="p63" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=TRUE⇒¬PhyElevatorFloor=LAST_FLOOR"/>
-<org.eventb.core.prPred name="p39" org.eventb.core.predicate="schedule≠SCHEDULER_WAIT⇒schedule=last_schedule"/>
-<org.eventb.core.prPred name="p40" org.eventb.core.predicate="b2n∈BOOL ⇸ ℤ"/>
-<org.eventb.core.prPred name="p86" org.eventb.core.predicate="schedule∈SCHEDULER_STRATEGY"/>
-<org.eventb.core.prPred name="p65" org.eventb.core.predicate="snsrElevatorFloor=−1⇒¬PhyCableEngine=CABLE_STOP"/>
-<org.eventb.core.prPred name="p41" org.eventb.core.predicate="PhyDownButtonLightsSet⊆1 ‥ LAST_FLOOR"/>
-<org.eventb.core.prPred name="p42" org.eventb.core.predicate="snsrCableEngine=CABLE_STOP⇒PhyElevatorFloor=snsrElevatorFloor"/>
-<org.eventb.core.prPred name="p62" org.eventb.core.predicate="¬ctrlCableCommand=CABLE_STOP⇒ctrlDoorCommand=DOOR_CLOSE"/>
-<org.eventb.core.prPred name="p43" org.eventb.core.predicate="partition(CABLE_COMMAND,{CABLE_STOP},{CABLE_WIND},{CABLE_UNWIND})"/>
-<org.eventb.core.prPred name="p73" org.eventb.core.predicate="¬schedule=SCHEDULER_WAIT∧ctrlCableCommand=CABLE_STOP⇒¬requests ∖ {snsrElevatorFloor}=(∅ ⦂ ℙ(ℤ))"/>
-<org.eventb.core.prPred name="p44" org.eventb.core.predicate="b2n(TRUE)=1"/>
-<org.eventb.core.prPred name="p45" org.eventb.core.predicate="requests=ctrlFloorButtonLightsSet∪ctrlUpButtonLightsSet∪ctrlDownButtonLightsSet"/>
-<org.eventb.core.prPred name="p46" org.eventb.core.predicate="PhyFloorButtonLightsSet⊆0 ‥ LAST_FLOOR"/>
-<org.eventb.core.prPred name="p76" org.eventb.core.predicate="¬ctrlCableCommand=CABLE_STOP⇒schedule=last_schedule"/>
-<org.eventb.core.prPred name="p47" org.eventb.core.predicate="snsrUpButtonsSet⊆0 ‥ (LAST_FLOOR − 1)"/>
-<org.eventb.core.prPred name="p48" org.eventb.core.predicate="b2n(FALSE)=0"/>
-<org.eventb.core.prPred name="p50" org.eventb.core.predicate="snsrElevatorFloor=−1⇒ctrlCableCommand≠CABLE_STOP"/>
-<org.eventb.core.prPred name="p49" org.eventb.core.predicate="partition(DOOR_POSITION,{DOOR_OPENED},{DOOR_HALF},{DOOR_CLOSED})"/>
-<org.eventb.core.prPred name="p51" org.eventb.core.predicate="PhyFloorButtonsSet⊆0 ‥ LAST_FLOOR"/>
-<org.eventb.core.prPred name="p52" org.eventb.core.predicate="snsrDoorEngine=PhyDoorEngine"/>
-<org.eventb.core.prPred name="p64" org.eventb.core.predicate="snsrElevatorFloor=−1⇒¬ctrlCableCommand=CABLE_STOP"/>
-<org.eventb.core.prPred name="p53" org.eventb.core.predicate="ctrlCableCommand≠CABLE_STOP⇒schedule=last_schedule"/>
-<org.eventb.core.prPred name="p54" org.eventb.core.predicate="schedule=SCHEDULER_WAIT⇒ctrlCableCommand=CABLE_STOP"/>
-<org.eventb.core.prPred name="p79" org.eventb.core.predicate="PhyCableEngine∈CABLE_COMMAND"/>
-<org.eventb.core.prPred name="p55" org.eventb.core.predicate="snsrElevatorFloor=−1⇒PhyCableEngine≠CABLE_STOP"/>
-<org.eventb.core.prPred name="p72" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP∧PhyElevatorFloor=0⇒¬schedule=SCHEDULER_DOWN"/>
-<org.eventb.core.prPred name="p56" org.eventb.core.predicate="last_stop∈0 ‥ LAST_FLOOR"/>
-<org.eventb.core.prPred name="p77" org.eventb.core.predicate="ctrlCableCommand∈CABLE_COMMAND"/>
-<org.eventb.core.prPred name="p57" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=TRUE⇒snsrElevatorFloor=−1"/>
-<org.eventb.core.prPred name="p58" org.eventb.core.predicate="ctrlCableCommand=CABLE_WIND⇒schedule=SCHEDULER_UP"/>
-<org.eventb.core.prPred name="p84" org.eventb.core.predicate="snsrDoorEngine∈DOOR_COMMAND"/>
-<org.eventb.core.prPred name="p81" org.eventb.core.predicate="snsrCableEngine∈CABLE_COMMAND"/>
-<org.eventb.core.prPred name="p60" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP∧PhyElevatorFloor=0⇒schedule≠SCHEDULER_DOWN"/>
-<org.eventb.core.prPred name="p59" org.eventb.core.predicate="snsrFloorButtonsSet=PhyFloorButtonsSet"/>
-<org.eventb.core.prPred name="p61" org.eventb.core.predicate="snsrDoorPosition=PhyDoorPosition"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="TURNS_ON_DOWN_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="TURNS_OFF_DOWN_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="turn_down_button_light_on/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="turn_down_button_light_off/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="TURNS_ON_UP_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="TURNS_OFF_UP_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="turn_up_button_light_on/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0">
-<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p3"/>
-<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
-<org.eventb.core.prRule name="org.eventb.core.seqprover.typeRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0">
-<org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p4"/>
-<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p5"/>
-<org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p6"/>
-<org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p7"/>
-<org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p8"/>
-<org.eventb.core.prHypAction name="HIDE5" org.eventb.core.prHyps="p9"/>
-<org.eventb.core.prHypAction name="HIDE6" org.eventb.core.prHyps="p10"/>
-<org.eventb.core.prHypAction name="HIDE7" org.eventb.core.prHyps="p11"/>
-<org.eventb.core.prHypAction name="HIDE8" org.eventb.core.prHyps="p12"/>
-<org.eventb.core.prHypAction name="HIDE9" org.eventb.core.prHyps="p13"/>
-<org.eventb.core.prRule name="org.eventb.pp.pp" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="NewPP" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p3,p2">
-<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="R500"/>
-<org.eventb.core.prString name=".maxSteps" org.eventb.core.prSValue="2000"/>
-</org.eventb.core.prRule>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="x" org.eventb.core.type="ℤ"/>
-<org.eventb.core.prPred name="p9" org.eventb.core.predicate="PhyDoorEngine∈DOOR_COMMAND">
-<org.eventb.core.prIdent name="DOOR_COMMAND" org.eventb.core.type="ℙ(DOOR_COMMAND)"/>
-<org.eventb.core.prIdent name="PhyDoorEngine" org.eventb.core.type="DOOR_COMMAND"/>
-</org.eventb.core.prPred>
-<org.eventb.core.prPred name="p6" org.eventb.core.predicate="PhyCableEngine∈CABLE_COMMAND">
-<org.eventb.core.prIdent name="CABLE_COMMAND" org.eventb.core.type="ℙ(CABLE_COMMAND)"/>
-<org.eventb.core.prIdent name="PhyCableEngine" org.eventb.core.type="CABLE_COMMAND"/>
-</org.eventb.core.prPred>
-<org.eventb.core.prPred name="p13" org.eventb.core.predicate="schedule∈SCHEDULER_STRATEGY">
-<org.eventb.core.prIdent name="SCHEDULER_STRATEGY" org.eventb.core.type="ℙ(SCHEDULER_STRATEGY)"/>
-<org.eventb.core.prIdent name="schedule" org.eventb.core.type="SCHEDULER_STRATEGY"/>
-</org.eventb.core.prPred>
-<org.eventb.core.prPred name="p5" org.eventb.core.predicate="ctrlDoorCommand∈DOOR_COMMAND">
-<org.eventb.core.prIdent name="DOOR_COMMAND" org.eventb.core.type="ℙ(DOOR_COMMAND)"/>
-<org.eventb.core.prIdent name="ctrlDoorCommand" org.eventb.core.type="DOOR_COMMAND"/>
-</org.eventb.core.prPred>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="x∉ctrlUpButtonLightsSet"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ (ctrlUpButtonLightsSet∪{x})⊂snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-<org.eventb.core.prPred name="p4" org.eventb.core.predicate="ctrlCableCommand∈CABLE_COMMAND">
-<org.eventb.core.prIdent name="CABLE_COMMAND" org.eventb.core.type="ℙ(CABLE_COMMAND)"/>
-<org.eventb.core.prIdent name="ctrlCableCommand" org.eventb.core.type="CABLE_COMMAND"/>
-</org.eventb.core.prPred>
-<org.eventb.core.prPred name="p10" org.eventb.core.predicate="PhyDoorPosition∈DOOR_POSITION">
-<org.eventb.core.prIdent name="DOOR_POSITION" org.eventb.core.type="ℙ(DOOR_POSITION)"/>
-<org.eventb.core.prIdent name="PhyDoorPosition" org.eventb.core.type="DOOR_POSITION"/>
-</org.eventb.core.prPred>
-<org.eventb.core.prPred name="p11" org.eventb.core.predicate="snsrDoorEngine∈DOOR_COMMAND">
-<org.eventb.core.prIdent name="DOOR_COMMAND" org.eventb.core.type="ℙ(DOOR_COMMAND)"/>
-<org.eventb.core.prIdent name="snsrDoorEngine" org.eventb.core.type="DOOR_COMMAND"/>
-</org.eventb.core.prPred>
-<org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬x∈ctrlUpButtonLightsSet"/>
-<org.eventb.core.prPred name="p8" org.eventb.core.predicate="snsrCableEngine∈CABLE_COMMAND">
-<org.eventb.core.prIdent name="CABLE_COMMAND" org.eventb.core.type="ℙ(CABLE_COMMAND)"/>
-<org.eventb.core.prIdent name="snsrCableEngine" org.eventb.core.type="CABLE_COMMAND"/>
-</org.eventb.core.prPred>
-<org.eventb.core.prPred name="p7" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors∈BOOL">
-<org.eventb.core.prIdent name="PhyElevatorBetweenTwoFloors" org.eventb.core.type="BOOL"/>
-</org.eventb.core.prPred>
-<org.eventb.core.prPred name="p2" org.eventb.core.predicate="x∈snsrUpButtonsSet"/>
-<org.eventb.core.prPred name="p12" org.eventb.core.predicate="snsrDoorPosition∈DOOR_POSITION">
-<org.eventb.core.prIdent name="DOOR_POSITION" org.eventb.core.type="ℙ(DOOR_POSITION)"/>
-<org.eventb.core.prIdent name="snsrDoorPosition" org.eventb.core.type="DOOR_POSITION"/>
-</org.eventb.core.prPred>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="turn_up_button_light_off/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p3">
-<org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p1" org.eventb.core.prInfHyps="p2"/>
-<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
-<org.eventb.core.prRule name="org.eventb.core.seqprover.typeRewrites:0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0">
-<org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p4"/>
-<org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p5"/>
-<org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p6"/>
-<org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p7"/>
-<org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p8"/>
-<org.eventb.core.prHypAction name="HIDE5" org.eventb.core.prHyps="p9"/>
-<org.eventb.core.prHypAction name="HIDE6" org.eventb.core.prHyps="p10"/>
-<org.eventb.core.prHypAction name="HIDE7" org.eventb.core.prHyps="p11"/>
-<org.eventb.core.prHypAction name="HIDE8" org.eventb.core.prHyps="p12"/>
-<org.eventb.core.prHypAction name="HIDE9" org.eventb.core.prHyps="p13"/>
-<org.eventb.core.prRule name="org.eventb.pp.pp" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="NewPP" org.eventb.core.prGoal="p3" org.eventb.core.prHyps="p2">
-<org.eventb.core.prString name=".arg" org.eventb.core.prSValue="R500"/>
-<org.eventb.core.prString name=".maxSteps" org.eventb.core.prSValue="2000"/>
-</org.eventb.core.prRule>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrElevatorFloor" org.eventb.core.type="ℤ"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ (ctrlUpButtonLightsSet ∖ {snsrElevatorFloor})⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-<org.eventb.core.prPred name="p3" org.eventb.core.predicate="snsrUpButtonsSet⊆(snsrUpButtonsSet ∖ ctrlUpButtonLightsSet)∪(ctrlUpButtonLightsSet ∖ {snsrElevatorFloor})"/>
-<org.eventb.core.prPred name="p9" org.eventb.core.predicate="PhyDoorEngine∈DOOR_COMMAND">
-<org.eventb.core.prIdent name="DOOR_COMMAND" org.eventb.core.type="ℙ(DOOR_COMMAND)"/>
-<org.eventb.core.prIdent name="PhyDoorEngine" org.eventb.core.type="DOOR_COMMAND"/>
-</org.eventb.core.prPred>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="snsrElevatorFloor∉snsrUpButtonsSet"/>
-<org.eventb.core.prPred name="p6" org.eventb.core.predicate="PhyCableEngine∈CABLE_COMMAND">
-<org.eventb.core.prIdent name="CABLE_COMMAND" org.eventb.core.type="ℙ(CABLE_COMMAND)"/>
-<org.eventb.core.prIdent name="PhyCableEngine" org.eventb.core.type="CABLE_COMMAND"/>
-</org.eventb.core.prPred>
-<org.eventb.core.prPred name="p13" org.eventb.core.predicate="schedule∈SCHEDULER_STRATEGY">
-<org.eventb.core.prIdent name="SCHEDULER_STRATEGY" org.eventb.core.type="ℙ(SCHEDULER_STRATEGY)"/>
-<org.eventb.core.prIdent name="schedule" org.eventb.core.type="SCHEDULER_STRATEGY"/>
-</org.eventb.core.prPred>
-<org.eventb.core.prPred name="p5" org.eventb.core.predicate="ctrlDoorCommand∈DOOR_COMMAND">
-<org.eventb.core.prIdent name="DOOR_COMMAND" org.eventb.core.type="ℙ(DOOR_COMMAND)"/>
-<org.eventb.core.prIdent name="ctrlDoorCommand" org.eventb.core.type="DOOR_COMMAND"/>
-</org.eventb.core.prPred>
-<org.eventb.core.prPred name="p4" org.eventb.core.predicate="ctrlCableCommand∈CABLE_COMMAND">
-<org.eventb.core.prIdent name="CABLE_COMMAND" org.eventb.core.type="ℙ(CABLE_COMMAND)"/>
-<org.eventb.core.prIdent name="ctrlCableCommand" org.eventb.core.type="CABLE_COMMAND"/>
-</org.eventb.core.prPred>
-<org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬snsrElevatorFloor∈snsrUpButtonsSet"/>
-<org.eventb.core.prPred name="p10" org.eventb.core.predicate="PhyDoorPosition∈DOOR_POSITION">
-<org.eventb.core.prIdent name="DOOR_POSITION" org.eventb.core.type="ℙ(DOOR_POSITION)"/>
-<org.eventb.core.prIdent name="PhyDoorPosition" org.eventb.core.type="DOOR_POSITION"/>
-</org.eventb.core.prPred>
-<org.eventb.core.prPred name="p11" org.eventb.core.predicate="snsrDoorEngine∈DOOR_COMMAND">
-<org.eventb.core.prIdent name="DOOR_COMMAND" org.eventb.core.type="ℙ(DOOR_COMMAND)"/>
-<org.eventb.core.prIdent name="snsrDoorEngine" org.eventb.core.type="DOOR_COMMAND"/>
-</org.eventb.core.prPred>
-<org.eventb.core.prPred name="p8" org.eventb.core.predicate="snsrCableEngine∈CABLE_COMMAND">
-<org.eventb.core.prIdent name="CABLE_COMMAND" org.eventb.core.type="ℙ(CABLE_COMMAND)"/>
-<org.eventb.core.prIdent name="snsrCableEngine" org.eventb.core.type="CABLE_COMMAND"/>
-</org.eventb.core.prPred>
-<org.eventb.core.prPred name="p7" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors∈BOOL">
-<org.eventb.core.prIdent name="PhyElevatorBetweenTwoFloors" org.eventb.core.type="BOOL"/>
-</org.eventb.core.prPred>
-<org.eventb.core.prPred name="p12" org.eventb.core.predicate="snsrDoorPosition∈DOOR_POSITION">
-<org.eventb.core.prIdent name="DOOR_POSITION" org.eventb.core.type="ℙ(DOOR_POSITION)"/>
-<org.eventb.core.prIdent name="snsrDoorPosition" org.eventb.core.type="DOOR_POSITION"/>
-</org.eventb.core.prPred>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="TURNS_ON_FLOOR_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="TURNS_OFF_FLOOR_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="turn_floor_button_light_off/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="DOOR_OPENS_WHEN_CLOSED/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="DOOR_OPENS_WHEN_HALF/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="DOOR_CLOSES_WHEN_OPENED/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="DOOR_CLOSES_WHEN_HALF/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="DOOR_CLOSES_WHEN_CLOSED/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="STOP_DOOR_ENGINE/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="ELEVATOR_LEAVES_FLOOR_UP/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="ELEVATOR_REACHES_FLOOR_UP/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="ELEVATOR_LEAVES_FLOOR_DOWN/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="ELEVATOR_REACHES_FLOOR_DOWN/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="STOP_CABLE_ENGINE/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="open_door/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="stop_door/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="close_door/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="start_move_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="start_move_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="stop/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="switch_schedule_to_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="resume_schedule_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="switch_schedule_to_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-<org.eventb.core.prProof name="resume_schedule_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.autoRewrites:1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
-<org.eventb.core.prAnte name="0" org.eventb.core.prGoal="p1">
-<org.eventb.core.prRule name="org.eventb.core.seqprover.trueGoal" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
-</org.eventb.core.prAnte>
-</org.eventb.core.prRule>
-<org.eventb.core.prIdent name="ctrlUpButtonLightsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prIdent name="snsrUpButtonsSet" org.eventb.core.type="ℙ(ℤ)"/>
-<org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
-<org.eventb.core.prPred name="p0" org.eventb.core.predicate="snsrUpButtonsSet ∖ ctrlUpButtonLightsSet⊆snsrUpButtonsSet ∖ ctrlUpButtonLightsSet"/>
-</org.eventb.core.prProof>
-</org.eventb.core.prFile>
View
36 rodin/lift11_conv_lights.bps
@@ -1,36 +0,0 @@
-<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.psFile>
-<org.eventb.core.psStatus name="FIN" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="TURNS_ON_DOWN_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="TURNS_OFF_DOWN_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="turn_down_button_light_on/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="turn_down_button_light_off/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="TURNS_ON_UP_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="TURNS_OFF_UP_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="turn_up_button_light_on/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="turn_up_button_light_off/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="TURNS_ON_FLOOR_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="TURNS_OFF_FLOOR_BUTTON_LIGHT/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="turn_floor_button_light_off/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_OPENS_WHEN_CLOSED/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_OPENS_WHEN_HALF/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_CLOSES_WHEN_OPENED/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_CLOSES_WHEN_HALF/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_CLOSES_WHEN_CLOSED/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="STOP_DOOR_ENGINE/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_LEAVES_FLOOR_UP/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_REACHES_FLOOR_UP/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_LEAVES_FLOOR_DOWN/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_REACHES_FLOOR_DOWN/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="STOP_CABLE_ENGINE/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="open_door/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="stop_door/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="close_door/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="start_move_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="start_move_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="stop/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="switch_schedule_to_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="resume_schedule_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="switch_schedule_to_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="resume_schedule_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-</org.eventb.core.psFile>
View
152 rodin/lift11_conv_lights.bum
@@ -1,152 +0,0 @@
-<?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="1290783926097" org.eventb.texttools.text_representation="machine lift11_conv_light refines lift10_conv_lights sees ctx5_scheduler&#10;&#10;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&#10;&#10;variant snsrUpButtonsSet∖ ctrlUpButtonLightsSet&#10;&#10;events&#10; event INITIALISATION extends INITIALISATION&#10; end&#10;&#10; event USER_PRESSES_DOWN_BUTTON extends USER_PRESSES_DOWN_BUTTON&#10; end&#10;&#10; event USER_RELEASES_DOWN_BUTTON extends USER_RELEASES_DOWN_BUTTON&#10; end&#10;&#10; anticipated event TURNS_ON_DOWN_BUTTON_LIGHT extends TURNS_ON_DOWN_BUTTON_LIGHT&#10; end&#10;&#10; anticipated event TURNS_OFF_DOWN_BUTTON_LIGHT extends TURNS_OFF_DOWN_BUTTON_LIGHT&#10; end&#10;&#10; anticipated event turn_down_button_light_on extends turn_down_button_light_on&#10; end&#10;&#10; anticipated event turn_down_button_light_off extends turn_down_button_light_off&#10; end&#10;&#10; event USER_PRESSES_UP_BUTTON extends USER_PRESSES_UP_BUTTON&#10; end&#10;&#10; event USER_RELEASES_UP_BUTTON extends USER_RELEASES_UP_BUTTON&#10; end&#10;&#10; anticipated event TURNS_ON_UP_BUTTON_LIGHT extends TURNS_ON_UP_BUTTON_LIGHT&#10; end&#10;&#10; anticipated event TURNS_OFF_UP_BUTTON_LIGHT extends TURNS_OFF_UP_BUTTON_LIGHT&#10; end&#10;&#10; convergent event turn_up_button_light_on extends turn_up_button_light_on&#10; end&#10;&#10; anticipated event turn_up_button_light_off extends turn_up_button_light_off&#10; end&#10;&#10; event USER_PRESSES_FLOOR_BUTTON extends USER_PRESSES_FLOOR_BUTTON&#10; end&#10;&#10; event USER_RELEASES_FLOOR_BUTTON extends USER_RELEASES_FLOOR_BUTTON&#10; end&#10;&#10; anticipated event TURNS_ON_FLOOR_BUTTON_LIGHT extends TURNS_ON_FLOOR_BUTTON_LIGHT&#10; end&#10;&#10; anticipated event TURNS_OFF_FLOOR_BUTTON_LIGHT extends TURNS_OFF_FLOOR_BUTTON_LIGHT&#10; end&#10;&#10; convergent event turn_floor_button_light_on extends turn_floor_button_light_on&#10; end&#10;&#10; anticipated event turn_floor_button_light_off extends turn_floor_button_light_off&#10; end&#10;&#10; anticipated event DOOR_OPENS_WHEN_CLOSED extends DOOR_OPENS_WHEN_CLOSED&#10; end&#10;&#10; anticipated event DOOR_OPENS_WHEN_HALF extends DOOR_OPENS_WHEN_HALF&#10; end&#10;&#10; anticipated event DOOR_CLOSES_WHEN_OPENED extends DOOR_CLOSES_WHEN_OPENED&#10; end&#10;&#10; anticipated event DOOR_CLOSES_WHEN_HALF extends DOOR_CLOSES_WHEN_HALF&#10; end&#10;&#10; anticipated event DOOR_CLOSES_WHEN_CLOSED extends DOOR_CLOSES_WHEN_CLOSED&#10; end&#10;&#10; anticipated event STOP_DOOR_ENGINE extends STOP_DOOR_ENGINE&#10; end&#10;&#10; anticipated event ELEVATOR_LEAVES_FLOOR_UP extends ELEVATOR_LEAVES_FLOOR_UP&#10; end&#10;&#10; anticipated event ELEVATOR_REACHES_FLOOR_UP extends ELEVATOR_REACHES_FLOOR_UP&#10; end&#10;&#10; anticipated event ELEVATOR_LEAVES_FLOOR_DOWN extends ELEVATOR_LEAVES_FLOOR_DOWN&#10; end&#10;&#10; anticipated event ELEVATOR_REACHES_FLOOR_DOWN extends ELEVATOR_REACHES_FLOOR_DOWN&#10; end&#10;&#10; anticipated event STOP_CABLE_ENGINE extends STOP_CABLE_ENGINE&#10; end&#10;&#10; anticipated event open_door extends open_door&#10; end&#10;&#10; anticipated event stop_door extends stop_door&#10; end&#10;&#10; anticipated event close_door extends close_door&#10; end&#10;&#10; anticipated event start_move_up extends start_move_up&#10; end&#10;&#10; anticipated event start_move_down extends start_move_down&#10; end&#10;&#10; anticipated event stop extends stop&#10; end&#10;&#10; anticipated event switch_schedule_to_up extends switch_schedule_to_up&#10; end&#10;&#10; anticipated event resume_schedule_up extends resume_schedule_up&#10; end&#10;&#10; anticipated event switch_schedule_to_down extends switch_schedule_to_down&#10; end&#10;&#10; anticipated event resume_schedule_down extends resume_schedule_down&#10; end&#10;end&#10;" version="5">
-<org.eventb.core.refinesMachine name="_mbd0oPluEd-1httaBm5m2g" org.eventb.core.target="lift10_conv_lights"/>
-<org.eventb.core.seesContext name="_mbd0ofluEd-1httaBm5m2g" 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="_8ov3UPk7Ed-WtNZH8d5nSA" org.eventb.core.identifier="requests"/>
-<org.eventb.core.variable name="_mbfp0PluEd-1httaBm5m2g" org.eventb.core.identifier="request_served"/>
-<org.eventb.core.variant name="_028ScPk8Ed-hoNTGCqdYog" org.eventb.core.expression="snsrUpButtonsSet∖ ctrlUpButtonLightsSet"/>
-<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="_mbfp0fluEd-1httaBm5m2g" org.eventb.core.target="USER_PRESSES_DOWN_BUTTON"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_mbgQ4PluEd-1httaBm5m2g" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_DOWN_BUTTON">
-<org.eventb.core.refinesEvent name="_mbgQ4fluEd-1httaBm5m2g" 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="_mbgQ4vluEd-1httaBm5m2g" 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="_mbgQ4_luEd-1httaBm5m2g" 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="_mbgQ5PluEd-1httaBm5m2g" 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="_mbg38PluEd-1httaBm5m2g" 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="_mbg38fluEd-1httaBm5m2g" org.eventb.core.target="USER_PRESSES_UP_BUTTON"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_3Io6M-WyEd-64JNDK1TKiQ" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_UP_BUTTON">
-<org.eventb.core.refinesEvent name="_mbg38vluEd-1httaBm5m2g" 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="_mbhfAPluEd-1httaBm5m2g" 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="_mbhfAfluEd-1httaBm5m2g" 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="_mbhfAvluEd-1httaBm5m2g" 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="_mbhfA_luEd-1httaBm5m2g" 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="_mbiGEPluEd-1httaBm5m2g" org.eventb.core.target="USER_PRESSES_FLOOR_BUTTON"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_mbiGEfluEd-1httaBm5m2g" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_FLOOR_BUTTON">
-<org.eventb.core.refinesEvent name="_mbiGEvluEd-1httaBm5m2g" 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="_mbiGE_luEd-1httaBm5m2g" 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="_mbiGFPluEd-1httaBm5m2g" 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="_mbitIPluEd-1httaBm5m2g" 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="_mbitIfluEd-1httaBm5m2g" 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="_mbitIvluEd-1httaBm5m2g" 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="_mbjUMPluEd-1httaBm5m2g" 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="_mbjUMfluEd-1httaBm5m2g" 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="_mbjUMvluEd-1httaBm5m2g" 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="_mbj7QPluEd-1httaBm5m2g" 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="_mbj7QfluEd-1httaBm5m2g" org.eventb.core.target="STOP_DOOR_ENGINE"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_mbj7QvluEd-1httaBm5m2g" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_UP">
-<org.eventb.core.refinesEvent name="_mbj7Q_luEd-1httaBm5m2g" org.eventb.core.target="ELEVATOR_LEAVES_FLOOR_UP"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_mbj7RPluEd-1httaBm5m2g" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_UP">
-<org.eventb.core.refinesEvent name="_mbj7RfluEd-1httaBm5m2g" org.eventb.core.target="ELEVATOR_REACHES_FLOOR_UP"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_mbkiUPluEd-1httaBm5m2g" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_DOWN">
-<org.eventb.core.refinesEvent name="_mbkiUfluEd-1httaBm5m2g" org.eventb.core.target="ELEVATOR_LEAVES_FLOOR_DOWN"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_mbkiUvluEd-1httaBm5m2g" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_DOWN">
-<org.eventb.core.refinesEvent name="_mbkiU_luEd-1httaBm5m2g" 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="_mbkiVPluEd-1httaBm5m2g" 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="_mblJYPluEd-1httaBm5m2g" 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="_mblJYfluEd-1httaBm5m2g" 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="_mblJYvluEd-1httaBm5m2g" 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="_mblwcPluEd-1httaBm5m2g" 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="_mblwcfluEd-1httaBm5m2g" 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="_mblwcvluEd-1httaBm5m2g" 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="_mbmXgPluEd-1httaBm5m2g" 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="_mbmXgfluEd-1httaBm5m2g" 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="_mbmXgvluEd-1httaBm5m2g" 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="_mbm-kPluEd-1httaBm5m2g" org.eventb.core.target="resume_schedule_down"/>
-</org.eventb.core.event>
-</org.eventb.core.machineFile>
View
531 rodin/lift18_conv_schedule.bcm
0 additions, 531 deletions not shown
View
854 rodin/lift18_conv_schedule.bpo
0 additions, 854 deletions not shown
View
2  rodin/lift18_conv_schedule.bpo_tmp
@@ -1,2 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<org.eventb.core.poFile/>
View
7,419 rodin/lift18_conv_schedule.bpr
0 additions, 7,419 deletions not shown
View
46 rodin/lift18_conv_schedule.bps
@@ -1,46 +0,0 @@
-<?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.psFile>
-<org.eventb.core.psStatus name="VWD" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_OPENS_WHEN_CLOSED/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_OPENS_WHEN_CLOSED/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_OPENS_WHEN_HALF/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_OPENS_WHEN_HALF/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_CLOSES_WHEN_OPENED/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_CLOSES_WHEN_OPENED/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_CLOSES_WHEN_HALF/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_CLOSES_WHEN_HALF/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_CLOSES_WHEN_CLOSED/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="DOOR_CLOSES_WHEN_CLOSED/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="STOP_DOOR_ENGINE/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="STOP_DOOR_ENGINE/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_LEAVES_FLOOR_UP/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_LEAVES_FLOOR_UP/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_REACHES_FLOOR_UP/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_REACHES_FLOOR_UP/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_LEAVES_FLOOR_DOWN/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_LEAVES_FLOOR_DOWN/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_REACHES_FLOOR_DOWN/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="ELEVATOR_REACHES_FLOOR_DOWN/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="STOP_CABLE_ENGINE/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="STOP_CABLE_ENGINE/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="open_door/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="open_door/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="stop_door/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="stop_door/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="close_door/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="close_door/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="start_move_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="start_move_up/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="start_move_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="start_move_down/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="stop/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="stop/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="switch_schedule_to_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="switch_schedule_to_up/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="resume_schedule_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="resume_schedule_up/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="switch_schedule_to_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="switch_schedule_to_down/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="resume_schedule_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="resume_schedule_down/NAT" org.eventb.core.confidence="1000" org.eventb.core.poStamp="30" org.eventb.core.psManual="false"/>
-</org.eventb.core.psFile>
View
152 rodin/lift18_conv_schedule.bum
@@ -1,152 +0,0 @@
-<?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="1290784346594" org.eventb.texttools.text_representation="machine lift18_conv_door refines lift17_conv_lights sees ctx6_conv_utils&#10;&#10;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&#10;&#10;variant b2n(request_served)&#10;&#10;events&#10; event INITIALISATION extends INITIALISATION&#10; end&#10;&#10; event USER_PRESSES_DOWN_BUTTON extends USER_PRESSES_DOWN_BUTTON&#10; end&#10;&#10; event USER_RELEASES_DOWN_BUTTON extends USER_RELEASES_DOWN_BUTTON&#10; end&#10;&#10; convergent event TURNS_ON_DOWN_BUTTON_LIGHT extends TURNS_ON_DOWN_BUTTON_LIGHT&#10; end&#10;&#10; convergent event TURNS_OFF_DOWN_BUTTON_LIGHT extends TURNS_OFF_DOWN_BUTTON_LIGHT&#10; end&#10;&#10; convergent event turn_down_button_light_on extends turn_down_button_light_on&#10; end&#10;&#10; convergent event turn_down_button_light_off extends turn_down_button_light_off&#10; end&#10;&#10; event USER_PRESSES_UP_BUTTON extends USER_PRESSES_UP_BUTTON&#10; end&#10;&#10; event USER_RELEASES_UP_BUTTON extends USER_RELEASES_UP_BUTTON&#10; end&#10;&#10; convergent event TURNS_ON_UP_BUTTON_LIGHT extends TURNS_ON_UP_BUTTON_LIGHT&#10; end&#10;&#10; convergent event TURNS_OFF_UP_BUTTON_LIGHT extends TURNS_OFF_UP_BUTTON_LIGHT&#10; end&#10;&#10; convergent event turn_up_button_light_on extends turn_up_button_light_on&#10; end&#10;&#10; convergent event turn_up_button_light_off extends turn_up_button_light_off&#10; end&#10;&#10; event USER_PRESSES_FLOOR_BUTTON extends USER_PRESSES_FLOOR_BUTTON&#10; end&#10;&#10; event USER_RELEASES_FLOOR_BUTTON extends USER_RELEASES_FLOOR_BUTTON&#10; end&#10;&#10; convergent event TURNS_ON_FLOOR_BUTTON_LIGHT extends TURNS_ON_FLOOR_BUTTON_LIGHT&#10; end&#10;&#10; convergent event TURNS_OFF_FLOOR_BUTTON_LIGHT extends TURNS_OFF_FLOOR_BUTTON_LIGHT&#10; end&#10;&#10; convergent event turn_floor_button_light_on extends turn_floor_button_light_on&#10; end&#10;&#10; convergent event turn_floor_button_light_off extends turn_floor_button_light_off&#10; end&#10;&#10; anticipated event DOOR_OPENS_WHEN_CLOSED extends DOOR_OPENS_WHEN_CLOSED&#10; end&#10;&#10; anticipated event DOOR_OPENS_WHEN_HALF extends DOOR_OPENS_WHEN_HALF&#10; end&#10;&#10; anticipated event DOOR_CLOSES_WHEN_OPENED extends DOOR_CLOSES_WHEN_OPENED&#10; end&#10;&#10; anticipated event DOOR_CLOSES_WHEN_HALF extends DOOR_CLOSES_WHEN_HALF&#10; end&#10;&#10; anticipated event DOOR_CLOSES_WHEN_CLOSED extends DOOR_CLOSES_WHEN_CLOSED&#10; end&#10;&#10; anticipated event STOP_DOOR_ENGINE extends STOP_DOOR_ENGINE&#10; end&#10;&#10; anticipated event ELEVATOR_LEAVES_FLOOR_UP extends ELEVATOR_LEAVES_FLOOR_UP&#10; end&#10;&#10; anticipated event ELEVATOR_REACHES_FLOOR_UP extends ELEVATOR_REACHES_FLOOR_UP&#10; end&#10;&#10; anticipated event ELEVATOR_LEAVES_FLOOR_DOWN extends ELEVATOR_LEAVES_FLOOR_DOWN&#10; end&#10;&#10; anticipated event ELEVATOR_REACHES_FLOOR_DOWN extends ELEVATOR_REACHES_FLOOR_DOWN&#10; end&#10;&#10; anticipated event STOP_CABLE_ENGINE extends STOP_CABLE_ENGINE&#10; end&#10;&#10; anticipated event open_door extends open_door&#10; end&#10;&#10; anticipated event stop_door extends stop_door&#10; end&#10;&#10; anticipated event close_door extends close_door&#10; end&#10;&#10; anticipated event start_move_up extends start_move_up&#10; end&#10;&#10; anticipated event start_move_down extends start_move_down&#10; end&#10;&#10; anticipated event stop extends stop&#10; end&#10;&#10; convergent event switch_schedule_to_up extends switch_schedule_to_up&#10; end&#10;&#10; convergent event resume_schedule_up extends resume_schedule_up&#10; end&#10;&#10; convergent event switch_schedule_to_down extends switch_schedule_to_down&#10; end&#10;&#10; convergent event resume_schedule_down extends resume_schedule_down&#10; end&#10;end&#10;" version="5">
-<org.eventb.core.refinesMachine name="_lGKZIPlvEd-F0OvBKAXwJQ" org.eventb.core.target="lift17_conv_lights"/>
-<org.eventb.core.seesContext name="_lGKZIflvEd-F0OvBKAXwJQ" 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.variant name="_lGMOUPlvEd-F0OvBKAXwJQ" org.eventb.core.expression="b2n(request_served)"/>
-<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="_lGM1YPlvEd-F0OvBKAXwJQ" org.eventb.core.target="USER_PRESSES_DOWN_BUTTON"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_lGM1YflvEd-F0OvBKAXwJQ" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_DOWN_BUTTON">
-<org.eventb.core.refinesEvent name="_lGM1YvlvEd-F0OvBKAXwJQ" 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="_lGNccPlvEd-F0OvBKAXwJQ" 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="_lGNccflvEd-F0OvBKAXwJQ" 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="_lGNccvlvEd-F0OvBKAXwJQ" 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="_lGODgPlvEd-F0OvBKAXwJQ" 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="_lGODgflvEd-F0OvBKAXwJQ" org.eventb.core.target="USER_PRESSES_UP_BUTTON"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_3Io6M-WyEd-64JNDK1TKiQ" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_UP_BUTTON">
-<org.eventb.core.refinesEvent name="_lGODgvlvEd-F0OvBKAXwJQ" 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="_lGOqkPlvEd-F0OvBKAXwJQ" 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="_lGOqkflvEd-F0OvBKAXwJQ" 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="_lGOqkvlvEd-F0OvBKAXwJQ" 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="_lGPRoPlvEd-F0OvBKAXwJQ" 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="_lGPRoflvEd-F0OvBKAXwJQ" org.eventb.core.target="USER_PRESSES_FLOOR_BUTTON"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_lGPRovlvEd-F0OvBKAXwJQ" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_FLOOR_BUTTON">
-<org.eventb.core.refinesEvent name="_lGPRo_lvEd-F0OvBKAXwJQ" 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="_lGPRpPlvEd-F0OvBKAXwJQ" 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="_lGP4sPlvEd-F0OvBKAXwJQ" 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="_lGP4sflvEd-F0OvBKAXwJQ" 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="_lGP4svlvEd-F0OvBKAXwJQ" 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="_lGQfwPlvEd-F0OvBKAXwJQ" 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="_lGQfwflvEd-F0OvBKAXwJQ" 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="_lGQfwvlvEd-F0OvBKAXwJQ" 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="_lGRG0PlvEd-F0OvBKAXwJQ" 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="_lGRG0flvEd-F0OvBKAXwJQ" 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="_lGRt4PlvEd-F0OvBKAXwJQ" org.eventb.core.target="STOP_DOOR_ENGINE"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_lGRt4flvEd-F0OvBKAXwJQ" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_UP">
-<org.eventb.core.refinesEvent name="_lGRt4vlvEd-F0OvBKAXwJQ" org.eventb.core.target="ELEVATOR_LEAVES_FLOOR_UP"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_lGRt4_lvEd-F0OvBKAXwJQ" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_UP">
-<org.eventb.core.refinesEvent name="_lGRt5PlvEd-F0OvBKAXwJQ" org.eventb.core.target="ELEVATOR_REACHES_FLOOR_UP"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_lGRt5flvEd-F0OvBKAXwJQ" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_DOWN">
-<org.eventb.core.refinesEvent name="_lGSU8PlvEd-F0OvBKAXwJQ" org.eventb.core.target="ELEVATOR_LEAVES_FLOOR_DOWN"/>
-</org.eventb.core.event>
-<org.eventb.core.event name="_lGSU8flvEd-F0OvBKAXwJQ" org.eventb.core.convergence="2" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_DOWN">
-<org.eventb.core.refinesEvent name="_lGSU8vlvEd-F0OvBKAXwJQ" 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="_lGSU8_lvEd-F0OvBKAXwJQ" 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="_lGS8APlvEd-F0OvBKAXwJQ" 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="_lGS8AflvEd-F0OvBKAXwJQ" 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="_lGS8AvlvEd-F0OvBKAXwJQ" 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="_lGTjEPlvEd-F0OvBKAXwJQ" 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="_lGTjEflvEd-F0OvBKAXwJQ" 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="_lGUKIPlvEd-F0OvBKAXwJQ" 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="_lGUKIflvEd-F0OvBKAXwJQ" 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="_lGUKIvlvEd-F0OvBKAXwJQ" 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="_lGUxMPlvEd-F0OvBKAXwJQ" 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="_lGUxMflvEd-F0OvBKAXwJQ" org.eventb.core.target="resume_schedule_down"/>
-</org.eventb.core.event>
-</org.eventb.core.machineFile>
Please sign in to comment.
Something went wrong with that request. Please try again.