Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

clean project

  • Loading branch information...
commit 34279161a477c4d3206c7e750074cac97cd7a437 1 parent c4962ad
Adrian Friedli authored
View
90 rodin/lift23_scheduler.bcm
@@ -1,7 +1,7 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scMachineFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd">
-<org.eventb.core.scRefinesMachine name="REF" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.refinesMachine#_0m8XMO5-Ed-dEtybZVK09Q"/>
-<org.eventb.core.scSeesContext name="SEES0" org.eventb.core.scTarget="/ProvenLift/ctx5_scheduler.bcc" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.seesContext#_0m8-QO5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesMachine name="REF" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.refinesMachine#_fbh80O6TEd-y3JdGki7orA"/>
+<org.eventb.core.scSeesContext name="SEES0" org.eventb.core.scTarget="/ProvenLift/ctx5_scheduler.bcc" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.seesContext#_fbh80e6TEd-y3JdGki7orA"/>
<org.eventb.core.scInternalContext name="ctx1_floors">
<org.eventb.core.scAxiom name="AXM0" org.eventb.core.label="axm1_1" org.eventb.core.predicate="LAST_FLOOR∈ℕ1" org.eventb.core.source="/ProvenLift/ctx1_floors.buc|org.eventb.core.contextFile#ctx1_floors|org.eventb.core.axiom#_lTa6wdd9Ed-Dle0at0Xgqg" org.eventb.core.theorem="false"/>
<org.eventb.core.scConstant name="LAST_FLOOR" org.eventb.core.source="/ProvenLift/ctx1_floors.buc|org.eventb.core.contextFile#ctx1_floors|org.eventb.core.constant#_lTa6wNd9Ed-Dle0at0Xgqg" org.eventb.core.type="ℤ"/>
@@ -164,15 +164,15 @@
<org.eventb.core.scAction name="ACT27" org.eventb.core.assignment="schedule ≔ SCHEDULER_WAIT" org.eventb.core.label="act23_1" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#'|org.eventb.core.action#_Uthuku5-Ed-dEtybZVK09Q"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT1" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_PRESSES_DOWN_BUTTON" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_3IkoxOWyEd-64JNDK1TKiQ">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT1" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_3IkoxOWyEd-64JNDK1TKiQ|org.eventb.core.refinesEvent#_0nABkO5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT1" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_3IkoxOWyEd-64JNDK1TKiQ|org.eventb.core.refinesEvent#_fblAIO6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd19_1" org.eventb.core.predicate="x∈1 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3IkoxOWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3IlP0eWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd19_2" org.eventb.core.predicate="x∉PhyDownButtonsSet" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3IkoxOWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3IlP0uWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyDownButtonsSet ≔ PhyDownButtonsSet∪{x}" org.eventb.core.label="act19_1" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3IkoxOWyEd-64JNDK1TKiQ|org.eventb.core.action#_3IlP0-WyEd-64JNDK1TKiQ"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="snsrDownButtonsSet ≔ snsrDownButtonsSet∪{x}" org.eventb.core.label="act19_2" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3IkoxOWyEd-64JNDK1TKiQ|org.eventb.core.action#_3IlP1OWyEd-64JNDK1TKiQ"/>
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3IkoxOWyEd-64JNDK1TKiQ|org.eventb.core.parameter#_3IlP0OWyEd-64JNDK1TKiQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
-<org.eventb.core.scEvent name="EVT2" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_DOWN_BUTTON" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_0nABke5-Ed-dEtybZVK09Q">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT2" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_0nABke5-Ed-dEtybZVK09Q|org.eventb.core.refinesEvent#_0nABku5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scEvent name="EVT2" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_DOWN_BUTTON" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_fblAIe6TEd-y3JdGki7orA">
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT2" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_fblAIe6TEd-y3JdGki7orA|org.eventb.core.refinesEvent#_fblAIu6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd19_1" org.eventb.core.predicate="x∈1 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_NE2OUO5wEd-5fb9VYGAuGg|org.eventb.core.guard#_3Il24eWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd19_2" org.eventb.core.predicate="x∈PhyDownButtonsSet" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_NE2OUO5wEd-5fb9VYGAuGg|org.eventb.core.guard#_3Il24uWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyDownButtonsSet ≔ PhyDownButtonsSet ∖ {x}" org.eventb.core.label="act19_1" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_NE2OUO5wEd-5fb9VYGAuGg|org.eventb.core.action#_3Il24-WyEd-64JNDK1TKiQ"/>
@@ -180,7 +180,7 @@
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_NE2OUO5wEd-5fb9VYGAuGg|org.eventb.core.parameter#_3Il24OWyEd-64JNDK1TKiQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT3" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="TURNS_ON_DOWN_BUTTON_LIGHT" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_3Il25eWyEd-64JNDK1TKiQ">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT3" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_3Il25eWyEd-64JNDK1TKiQ|org.eventb.core.refinesEvent#_0nAooO5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT3" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_3Il25eWyEd-64JNDK1TKiQ|org.eventb.core.refinesEvent#_fblAI-6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd19_1" org.eventb.core.predicate="x∈1 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3Il25eWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3Imd8eWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd19_2" org.eventb.core.predicate="x∈ctrlDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3Il25eWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3Imd8uWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd19_3" org.eventb.core.predicate="x∉PhyDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3Il25eWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3Imd8-WyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
@@ -188,7 +188,7 @@
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3Il25eWyEd-64JNDK1TKiQ|org.eventb.core.parameter#_3Imd8OWyEd-64JNDK1TKiQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT4" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="TURNS_OFF_DOWN_BUTTON_LIGHT" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_3Imd9eWyEd-64JNDK1TKiQ">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT4" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_3Imd9eWyEd-64JNDK1TKiQ|org.eventb.core.refinesEvent#_0nAooe5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT4" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_3Imd9eWyEd-64JNDK1TKiQ|org.eventb.core.refinesEvent#_fblnMO6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd19_1" org.eventb.core.predicate="x∈1 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3Imd9eWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3InFAeWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd19_2" org.eventb.core.predicate="x∉ctrlDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3Imd9eWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3InFAuWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd19_3" org.eventb.core.predicate="x∈PhyDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3Imd9eWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3InsEOWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
@@ -196,7 +196,7 @@
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3Imd9eWyEd-64JNDK1TKiQ|org.eventb.core.parameter#_3InFAOWyEd-64JNDK1TKiQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT5" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="turn_down_button_light_on" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_3InsEuWyEd-64JNDK1TKiQ">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT5" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_3InsEuWyEd-64JNDK1TKiQ|org.eventb.core.refinesEvent#_0nAoou5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT5" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_3InsEuWyEd-64JNDK1TKiQ|org.eventb.core.refinesEvent#_fblnMe6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd19_1" org.eventb.core.predicate="x∈1 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3InsEuWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3InsFOWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd19_2" org.eventb.core.predicate="x∈snsrDownButtonsSet" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3InsEuWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3InsFeWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd19_3" org.eventb.core.predicate="x∉ctrlDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3InsEuWyEd-64JNDK1TKiQ|org.eventb.core.guard#_3IoTIOWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
@@ -205,7 +205,7 @@
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3InsEuWyEd-64JNDK1TKiQ|org.eventb.core.parameter#_3InsE-WyEd-64JNDK1TKiQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT6" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="turn_down_button_light_off" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_3IoTI-WyEd-64JNDK1TKiQ">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT6" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_3IoTI-WyEd-64JNDK1TKiQ|org.eventb.core.refinesEvent#_0nAoo-5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT6" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_3IoTI-WyEd-64JNDK1TKiQ|org.eventb.core.refinesEvent#_fblnMu6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd19_1" org.eventb.core.predicate="floor&gt;0" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3IoTI-WyEd-64JNDK1TKiQ|org.eventb.core.guard#_3IoTJOWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd19_2" org.eventb.core.predicate="snsrDoorPosition=DOOR_OPENED" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3IoTI-WyEd-64JNDK1TKiQ|org.eventb.core.guard#_3IoTJeWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd19_3" org.eventb.core.predicate="floor∈ctrlDownButtonLightsSet" org.eventb.core.source="/ProvenLift/lift19_down_buttons.bum|org.eventb.core.machineFile#lift19_down_buttons|org.eventb.core.event#_3IoTI-WyEd-64JNDK1TKiQ|org.eventb.core.guard#_3Io6MOWyEd-64JNDK1TKiQ" org.eventb.core.theorem="false"/>
@@ -213,7 +213,7 @@
<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd23_1" org.eventb.core.predicate="schedule=SCHEDULER_DOWN" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_3IoTI-WyEd-64JNDK1TKiQ|org.eventb.core.guard#_Uti8su5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT7" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_PRESSES_UP_BUTTON" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_pvVR8eEsEd-bh-7nDQnLgQ">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT7" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_pvVR8eEsEd-bh-7nDQnLgQ|org.eventb.core.refinesEvent#_0nBPsO5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT7" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_pvVR8eEsEd-bh-7nDQnLgQ|org.eventb.core.refinesEvent#_fbmOQO6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd11_1" org.eventb.core.predicate="x∈0 ‥ (LAST_FLOOR − 1)" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvVR8eEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvVR8-EsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd11_2" org.eventb.core.predicate="x∉PhyUpButtonsSet" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvVR8eEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvVR9OEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyUpButtonsSet ≔ PhyUpButtonsSet∪{x}" org.eventb.core.label="act11_1" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvVR8eEsEd-bh-7nDQnLgQ|org.eventb.core.action#_pvVR9eEsEd-bh-7nDQnLgQ"/>
@@ -221,7 +221,7 @@
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvVR8eEsEd-bh-7nDQnLgQ|org.eventb.core.parameter#_pvVR8uEsEd-bh-7nDQnLgQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT8" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_UP_BUTTON" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_3Io6M-WyEd-64JNDK1TKiQ">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT8" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_3Io6M-WyEd-64JNDK1TKiQ|org.eventb.core.refinesEvent#_0nBPse5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT8" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_3Io6M-WyEd-64JNDK1TKiQ|org.eventb.core.refinesEvent#_fbmOQe6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd11_1" org.eventb.core.predicate="x∈0 ‥ (LAST_FLOOR − 1)" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvV5AOEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvV5AuEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd11_2" org.eventb.core.predicate="x∈PhyUpButtonsSet" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvV5AOEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvV5A-EsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyUpButtonsSet ≔ PhyUpButtonsSet ∖ {x}" org.eventb.core.label="act11_1" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvV5AOEsEd-bh-7nDQnLgQ|org.eventb.core.action#_pvV5BOEsEd-bh-7nDQnLgQ"/>
@@ -229,7 +229,7 @@
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvV5AOEsEd-bh-7nDQnLgQ|org.eventb.core.parameter#_pvV5AeEsEd-bh-7nDQnLgQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT9" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="TURNS_ON_UP_BUTTON_LIGHT" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_pvV5BuEsEd-bh-7nDQnLgQ">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT9" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_pvV5BuEsEd-bh-7nDQnLgQ|org.eventb.core.refinesEvent#_0nB2wO5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT9" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_pvV5BuEsEd-bh-7nDQnLgQ|org.eventb.core.refinesEvent#_fbmOQu6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd11_1" org.eventb.core.predicate="x∈0 ‥ (LAST_FLOOR − 1)" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvV5BuEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvWgEeEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd11_2" org.eventb.core.predicate="x∈ctrlUpButtonLightsSet" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvV5BuEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvWgEuEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd11_3" org.eventb.core.predicate="x∉PhyUpButtonLightsSet" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvV5BuEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvWgE-EsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
@@ -237,7 +237,7 @@
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvV5BuEsEd-bh-7nDQnLgQ|org.eventb.core.parameter#_pvWgEOEsEd-bh-7nDQnLgQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT10" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="TURNS_OFF_UP_BUTTON_LIGHT" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_pvWgFeEsEd-bh-7nDQnLgQ">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT10" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_pvWgFeEsEd-bh-7nDQnLgQ|org.eventb.core.refinesEvent#_0nB2we5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT10" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_pvWgFeEsEd-bh-7nDQnLgQ|org.eventb.core.refinesEvent#_fbmOQ-6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd11_1" org.eventb.core.predicate="x∈0 ‥ (LAST_FLOOR − 1)" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvWgFeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvXHIeEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd11_2" org.eventb.core.predicate="x∉ctrlUpButtonLightsSet" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvWgFeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvXHIuEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd11_3" org.eventb.core.predicate="x∈PhyUpButtonLightsSet" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvWgFeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvXHI-EsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
@@ -245,7 +245,7 @@
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvWgFeEsEd-bh-7nDQnLgQ|org.eventb.core.parameter#_pvXHIOEsEd-bh-7nDQnLgQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT11" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="turn_up_button_light_on" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_pvXHJeEsEd-bh-7nDQnLgQ">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT11" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_pvXHJeEsEd-bh-7nDQnLgQ|org.eventb.core.refinesEvent#_0nB2wu5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT11" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_pvXHJeEsEd-bh-7nDQnLgQ|org.eventb.core.refinesEvent#_fbm1UO6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd11_1" org.eventb.core.predicate="x∈0 ‥ (LAST_FLOOR − 1)" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvXHJeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvXuMOEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd11_2" org.eventb.core.predicate="x∈snsrUpButtonsSet" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvXHJeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvXuMeEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd11_3" org.eventb.core.predicate="x∉ctrlUpButtonLightsSet" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvXHJeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvXuMuEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
@@ -254,7 +254,7 @@
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvXHJeEsEd-bh-7nDQnLgQ|org.eventb.core.parameter#_pvXHJuEsEd-bh-7nDQnLgQ" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT12" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="turn_up_button_light_off" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_pvXuNeEsEd-bh-7nDQnLgQ">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT12" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_pvXuNeEsEd-bh-7nDQnLgQ|org.eventb.core.refinesEvent#_0nCd0O5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT12" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_pvXuNeEsEd-bh-7nDQnLgQ|org.eventb.core.refinesEvent#_fbm1Ue6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd11_1" org.eventb.core.predicate="floor&lt;LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvXuNeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvXuNuEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd11_2" org.eventb.core.predicate="snsrDoorPosition=DOOR_OPENED" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvXuNeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvYVQOEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd11_3" org.eventb.core.predicate="floor∈ctrlUpButtonLightsSet" org.eventb.core.source="/ProvenLift/lift15_up_buttons.bum|org.eventb.core.machineFile#lift15_up_buttons|org.eventb.core.event#_pvXuNeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_pvYVQeEsEd-bh-7nDQnLgQ" org.eventb.core.theorem="false"/>
@@ -262,15 +262,15 @@
<org.eventb.core.scGuard name="GRD3" org.eventb.core.label="grd23_1" org.eventb.core.predicate="schedule=SCHEDULER_UP" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_pvXuNeEsEd-bh-7nDQnLgQ|org.eventb.core.guard#_UtkK0u5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT13" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_PRESSES_FLOOR_BUTTON" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_tI1hE-A_Ed-78bCl9yYd-Q">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT13" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_tI1hE-A_Ed-78bCl9yYd-Q|org.eventb.core.refinesEvent#_0nCd0e5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT13" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_tI1hE-A_Ed-78bCl9yYd-Q|org.eventb.core.refinesEvent#_fbm1Uu6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd11_1" org.eventb.core.predicate="x∈0 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI1hE-A_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI1hFeA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd11_2" org.eventb.core.predicate="x∉PhyFloorButtonsSet" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI1hE-A_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI2IIOA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyFloorButtonsSet ≔ PhyFloorButtonsSet∪{x}" org.eventb.core.label="act11_1" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI1hE-A_Ed-78bCl9yYd-Q|org.eventb.core.action#_tI2IIeA_Ed-78bCl9yYd-Q"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="snsrFloorButtonsSet ≔ snsrFloorButtonsSet∪{x}" org.eventb.core.label="act11_2" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI1hE-A_Ed-78bCl9yYd-Q|org.eventb.core.action#_tI2IIuA_Ed-78bCl9yYd-Q"/>
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI1hE-A_Ed-78bCl9yYd-Q|org.eventb.core.parameter#_tI1hFOA_Ed-78bCl9yYd-Q" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
-<org.eventb.core.scEvent name="EVT14" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_FLOOR_BUTTON" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_0nCd0u5-Ed-dEtybZVK09Q">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT14" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_0nCd0u5-Ed-dEtybZVK09Q|org.eventb.core.refinesEvent#_0nCd0-5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scEvent name="EVT14" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_FLOOR_BUTTON" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_fbm1U-6TEd-y3JdGki7orA">
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT14" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_fbm1U-6TEd-y3JdGki7orA|org.eventb.core.refinesEvent#_fbncYO6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd11_1" org.eventb.core.predicate="x∈0 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_Iyc28O5uEd-5fb9VYGAuGg|org.eventb.core.guard#_tI2vMeA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd11_2" org.eventb.core.predicate="x∈PhyFloorButtonsSet" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_Iyc28O5uEd-5fb9VYGAuGg|org.eventb.core.guard#_tI2vMuA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyFloorButtonsSet ≔ PhyFloorButtonsSet ∖ {x}" org.eventb.core.label="act11_1" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_Iyc28O5uEd-5fb9VYGAuGg|org.eventb.core.action#_tI2vM-A_Ed-78bCl9yYd-Q"/>
@@ -278,7 +278,7 @@
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_Iyc28O5uEd-5fb9VYGAuGg|org.eventb.core.parameter#_tI2vMOA_Ed-78bCl9yYd-Q" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT15" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="TURNS_ON_FLOOR_BUTTON_LIGHT" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_tI2vNeA_Ed-78bCl9yYd-Q">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT15" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_tI2vNeA_Ed-78bCl9yYd-Q|org.eventb.core.refinesEvent#_0nDE4O5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT15" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_tI2vNeA_Ed-78bCl9yYd-Q|org.eventb.core.refinesEvent#_fbncYe6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd11_1" org.eventb.core.predicate="x∈0 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI2vNeA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI3WQeA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd11_2" org.eventb.core.predicate="x∈ctrlFloorButtonLightsSet" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI2vNeA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI3WQuA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd11_3" org.eventb.core.predicate="x∉PhyFloorButtonLightsSet" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI2vNeA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI3WQ-A_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
@@ -286,7 +286,7 @@
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI2vNeA_Ed-78bCl9yYd-Q|org.eventb.core.parameter#_tI3WQOA_Ed-78bCl9yYd-Q" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT16" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="TURNS_OFF_FLOOR_BUTTON_LIGHT" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_pvY8UuEsEd-bh-7nDQnLgQ">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT16" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_pvY8UuEsEd-bh-7nDQnLgQ|org.eventb.core.refinesEvent#_0nDE4e5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT16" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_pvY8UuEsEd-bh-7nDQnLgQ|org.eventb.core.refinesEvent#_fbncYu6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd11_1" org.eventb.core.predicate="x∈0 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI39UeA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI39U-A_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd11_2" org.eventb.core.predicate="x∉ctrlFloorButtonLightsSet" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI39UeA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI39VOA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd11_3" org.eventb.core.predicate="x∈PhyFloorButtonLightsSet" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI39UeA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI4kYOA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
@@ -294,7 +294,7 @@
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI39UeA_Ed-78bCl9yYd-Q|org.eventb.core.parameter#_tI39UuA_Ed-78bCl9yYd-Q" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT17" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="turn_floor_button_light_on" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_tI4kYuA_Ed-78bCl9yYd-Q">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT17" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_tI4kYuA_Ed-78bCl9yYd-Q|org.eventb.core.refinesEvent#_0nDr8O5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT17" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_tI4kYuA_Ed-78bCl9yYd-Q|org.eventb.core.refinesEvent#_fboDcO6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd11_1" org.eventb.core.predicate="x∈0 ‥ LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI4kYuA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI4kZOA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd11_2" org.eventb.core.predicate="x∈snsrFloorButtonsSet" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI4kYuA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI5LcOA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd11_3" org.eventb.core.predicate="x∉ctrlFloorButtonLightsSet" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI4kYuA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI5LceA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
@@ -303,13 +303,13 @@
<org.eventb.core.scParameter name="x" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI4kYuA_Ed-78bCl9yYd-Q|org.eventb.core.parameter#_tI4kY-A_Ed-78bCl9yYd-Q" org.eventb.core.type="ℤ"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT18" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="turn_floor_button_light_off" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_tI5ygOA_Ed-78bCl9yYd-Q">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT18" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_tI5ygOA_Ed-78bCl9yYd-Q|org.eventb.core.refinesEvent#_0nDr8e5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT18" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_tI5ygOA_Ed-78bCl9yYd-Q|org.eventb.core.refinesEvent#_fboDce6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd11_1" org.eventb.core.predicate="snsrDoorPosition=DOOR_OPENED" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI5ygOA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI5ygeA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd11_2" org.eventb.core.predicate="floor∈ctrlFloorButtonLightsSet" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI5ygOA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_tI5yguA_Ed-78bCl9yYd-Q" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="act11_1" org.eventb.core.predicate="floor∉ctrlFloorButtonLightsSet" org.eventb.core.source="/ProvenLift/lift11_buttons.bum|org.eventb.core.machineFile#lift11_buttons|org.eventb.core.event#_tI5ygOA_Ed-78bCl9yYd-Q|org.eventb.core.guard#_MIVnwO45Ed-YEZpgk7369g" org.eventb.core.theorem="false"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT19" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="DOOR_OPENS_WHEN_CLOSED" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_KgayBOAzEd-73py7lbE8bg">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT19" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_KgayBOAzEd-73py7lbE8bg|org.eventb.core.refinesEvent#_0nDr8u5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT19" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_KgayBOAzEd-73py7lbE8bg|org.eventb.core.refinesEvent#_fboDcu6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="PhyDoorPosition=DOOR_CLOSED" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6WedOA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6XFgOA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="ctrlDoorCommand=DOOR_OPEN" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6WedOA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6XFgeA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyDoorPosition ≔ DOOR_HALF" org.eventb.core.label="act1" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6WedOA2Ed-73py7lbE8bg|org.eventb.core.action#_F6XFguA2Ed-73py7lbE8bg"/>
@@ -318,7 +318,7 @@
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="snsrDoorEngine ≔ DOOR_OPEN" org.eventb.core.label="act4" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6WedOA2Ed-73py7lbE8bg|org.eventb.core.action#_F6XFheA2Ed-73py7lbE8bg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT20" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="DOOR_OPENS_WHEN_HALF" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_KgcAIOAzEd-73py7lbE8bg">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT20" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_KgcAIOAzEd-73py7lbE8bg|org.eventb.core.refinesEvent#_0nETAO5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT20" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_KgcAIOAzEd-73py7lbE8bg|org.eventb.core.refinesEvent#_fboDc-6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="PhyDoorPosition=DOOR_HALF" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6XskOA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6XskeA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="ctrlDoorCommand=DOOR_OPEN" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6XskOA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6XskuA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyDoorPosition ≔ DOOR_OPENED" org.eventb.core.label="act1" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6XskOA2Ed-73py7lbE8bg|org.eventb.core.action#_F6Xsk-A2Ed-73py7lbE8bg"/>
@@ -327,7 +327,7 @@
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="snsrDoorEngine ≔ DOOR_OPEN" org.eventb.core.label="act4" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6XskOA2Ed-73py7lbE8bg|org.eventb.core.action#_F6YToeA2Ed-73py7lbE8bg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT21" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="DOOR_CLOSES_WHEN_OPENED" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_KgcnM-AzEd-73py7lbE8bg">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT21" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_KgcnM-AzEd-73py7lbE8bg|org.eventb.core.refinesEvent#_0nETAe5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT21" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_KgcnM-AzEd-73py7lbE8bg|org.eventb.core.refinesEvent#_fboqgO6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="PhyDoorPosition=DOOR_OPENED" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6YTouA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6YTo-A2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="ctrlDoorCommand=DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6YTouA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6YTpOA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyDoorPosition ≔ DOOR_HALF" org.eventb.core.label="act1" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6YTouA2Ed-73py7lbE8bg|org.eventb.core.action#_F6Y6sOA2Ed-73py7lbE8bg"/>
@@ -336,7 +336,7 @@
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="snsrDoorEngine ≔ DOOR_CLOSE" org.eventb.core.label="act4" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6YTouA2Ed-73py7lbE8bg|org.eventb.core.action#_F6Y6s-A2Ed-73py7lbE8bg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT22" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="DOOR_CLOSES_WHEN_HALF" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_KgdOReAzEd-73py7lbE8bg">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT22" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_KgdOReAzEd-73py7lbE8bg|org.eventb.core.refinesEvent#_0nETAu5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT22" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_KgdOReAzEd-73py7lbE8bg|org.eventb.core.refinesEvent#_fboqge6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="PhyDoorPosition=DOOR_HALF" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6Y6tOA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6Y6teA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="ctrlDoorCommand=DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6Y6tOA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6ZhwOA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyDoorPosition ≔ DOOR_CLOSED" org.eventb.core.label="act1" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6Y6tOA2Ed-73py7lbE8bg|org.eventb.core.action#_F6ZhweA2Ed-73py7lbE8bg"/>
@@ -345,7 +345,7 @@
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="snsrDoorEngine ≔ DOOR_CLOSE" org.eventb.core.label="act4" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6Y6tOA2Ed-73py7lbE8bg|org.eventb.core.action#_F6ZhxOA2Ed-73py7lbE8bg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT23" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="DOOR_CLOSES_WHEN_CLOSED" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_KgecYeAzEd-73py7lbE8bg">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT23" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_KgecYeAzEd-73py7lbE8bg|org.eventb.core.refinesEvent#_0nE6EO5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT23" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_KgecYeAzEd-73py7lbE8bg|org.eventb.core.refinesEvent#_fboqgu6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="PhyDoorPosition=DOOR_CLOSED" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6ZhxeA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6aI0OA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="ctrlDoorCommand=DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6ZhxeA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6aI0eA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd3" org.eventb.core.predicate="PhyDoorEngine≠DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6ZhxeA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6aI0uA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
@@ -353,14 +353,14 @@
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="snsrDoorEngine ≔ DOOR_CLOSE" org.eventb.core.label="act2" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6ZhxeA2Ed-73py7lbE8bg|org.eventb.core.action#_F6aI1OA2Ed-73py7lbE8bg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT24" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="STOP_DOOR_ENGINE" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_KgfDcuAzEd-73py7lbE8bg">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT24" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_KgfDcuAzEd-73py7lbE8bg|org.eventb.core.refinesEvent#_0nE6Ee5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT24" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_KgfDcuAzEd-73py7lbE8bg|org.eventb.core.refinesEvent#_fbpRkO6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1" org.eventb.core.predicate="PhyDoorEngine≠DOOR_STOP" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6aI1eA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6av4OA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2" org.eventb.core.predicate="ctrlDoorCommand=DOOR_STOP" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6aI1eA2Ed-73py7lbE8bg|org.eventb.core.guard#_F6av4eA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyDoorEngine ≔ DOOR_STOP" org.eventb.core.label="act1" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6aI1eA2Ed-73py7lbE8bg|org.eventb.core.action#_F6av4uA2Ed-73py7lbE8bg"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="snsrDoorEngine ≔ DOOR_STOP" org.eventb.core.label="act2" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_F6aI1eA2Ed-73py7lbE8bg|org.eventb.core.action#_F6av4-A2Ed-73py7lbE8bg"/>
</org.eventb.core.scEvent>
-<org.eventb.core.scEvent name="EVT25" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_UP" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_0nE6Eu5-Ed-dEtybZVK09Q">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT25" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_0nE6Eu5-Ed-dEtybZVK09Q|org.eventb.core.refinesEvent#_0nE6E-5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scEvent name="EVT25" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_UP" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_fbpRke6TEd-y3JdGki7orA">
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT25" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_fbpRke6TEd-y3JdGki7orA|org.eventb.core.refinesEvent#_fbpRku6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd4_1" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=FALSE" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_WIqngOAzEd-73py7lbE8bg|org.eventb.core.guard#_aGyMttq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd4_2" org.eventb.core.predicate="PhyElevatorFloor≠LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_WIqngOAzEd-73py7lbE8bg|org.eventb.core.guard#_aGyzwNq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd4_3" org.eventb.core.predicate="ctrlCableCommand=CABLE_WIND" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_WIqngOAzEd-73py7lbE8bg|org.eventb.core.guard#_aGyzwdq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
@@ -369,8 +369,8 @@
<org.eventb.core.scAction name="ACT2" org.eventb.core.assignment="snsrElevatorFloor ≔ −1" org.eventb.core.label="act4_3" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_WIqngOAzEd-73py7lbE8bg|org.eventb.core.action#_aGyzxNq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="snsrCableEngine ≔ CABLE_WIND" org.eventb.core.label="act4_4" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_WIqngOAzEd-73py7lbE8bg|org.eventb.core.action#_aGyzxdq-Ed-L_e8_V4iXIg"/>
</org.eventb.core.scEvent>
-<org.eventb.core.scEvent name="EVT26" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_UP" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_0nE6FO5-Ed-dEtybZVK09Q">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT26" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_0nE6FO5-Ed-dEtybZVK09Q|org.eventb.core.refinesEvent#_0nFhIO5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scEvent name="EVT26" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_UP" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_fbpRk-6TEd-y3JdGki7orA">
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT26" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_fbpRk-6TEd-y3JdGki7orA|org.eventb.core.refinesEvent#_fbpRlO6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd4_1" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=TRUE" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_WIrOkOAzEd-73py7lbE8bg|org.eventb.core.guard#_aGza0dq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd4_2" org.eventb.core.predicate="ctrlCableCommand=CABLE_WIND" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_WIrOkOAzEd-73py7lbE8bg|org.eventb.core.guard#_aGza0tq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyElevatorBetweenTwoFloors ≔ FALSE" org.eventb.core.label="act4_1" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_WIrOkOAzEd-73py7lbE8bg|org.eventb.core.action#_aGza09q-Ed-L_e8_V4iXIg"/>
@@ -379,8 +379,8 @@
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="snsrElevatorFloor ≔ PhyElevatorFloor+1" org.eventb.core.label="act4_4" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_WIrOkOAzEd-73py7lbE8bg|org.eventb.core.action#_aG0B4Nq-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT4" org.eventb.core.assignment="snsrCableEngine ≔ CABLE_WIND" org.eventb.core.label="act4_5" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_WIrOkOAzEd-73py7lbE8bg|org.eventb.core.action#_aG0B4dq-Ed-L_e8_V4iXIg"/>
</org.eventb.core.scEvent>
-<org.eventb.core.scEvent name="EVT27" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_DOWN" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_0nFhIe5-Ed-dEtybZVK09Q">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT27" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_0nFhIe5-Ed-dEtybZVK09Q|org.eventb.core.refinesEvent#_0nFhIu5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scEvent name="EVT27" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_DOWN" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_fbpRle6TEd-y3JdGki7orA">
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT27" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_fbpRle6TEd-y3JdGki7orA|org.eventb.core.refinesEvent#_fbp4oO6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd4_1" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=FALSE" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_WIscsOAzEd-73py7lbE8bg|org.eventb.core.guard#_aG0B49q-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd4_2" org.eventb.core.predicate="PhyElevatorFloor≠0" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_WIscsOAzEd-73py7lbE8bg|org.eventb.core.guard#_aG0B5Nq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd4_3" org.eventb.core.predicate="ctrlCableCommand=CABLE_UNWIND" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_WIscsOAzEd-73py7lbE8bg|org.eventb.core.guard#_aG0B5dq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
@@ -390,8 +390,8 @@
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="snsrElevatorFloor ≔ −1" org.eventb.core.label="act4_4" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_WIscsOAzEd-73py7lbE8bg|org.eventb.core.action#_aG0o89q-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT4" org.eventb.core.assignment="snsrCableEngine ≔ CABLE_UNWIND" org.eventb.core.label="act4_5" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_WIscsOAzEd-73py7lbE8bg|org.eventb.core.action#_aG0o9Nq-Ed-L_e8_V4iXIg"/>
</org.eventb.core.scEvent>
-<org.eventb.core.scEvent name="EVT28" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_DOWN" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_0nFhI-5-Ed-dEtybZVK09Q">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT28" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_0nFhI-5-Ed-dEtybZVK09Q|org.eventb.core.refinesEvent#_0nFhJO5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scEvent name="EVT28" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_DOWN" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_fbp4oe6TEd-y3JdGki7orA">
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT28" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_fbp4oe6TEd-y3JdGki7orA|org.eventb.core.refinesEvent#_fbp4ou6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd4_1" org.eventb.core.predicate="PhyElevatorBetweenTwoFloors=TRUE" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_WItq0OAzEd-73py7lbE8bg|org.eventb.core.guard#_aG1QANq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd4_2" org.eventb.core.predicate="ctrlCableCommand=CABLE_UNWIND" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_WItq0OAzEd-73py7lbE8bg|org.eventb.core.guard#_aG1QAdq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyElevatorBetweenTwoFloors ≔ FALSE" org.eventb.core.label="act4_1" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_WItq0OAzEd-73py7lbE8bg|org.eventb.core.action#_aG1QAtq-Ed-L_e8_V4iXIg"/>
@@ -400,14 +400,14 @@
<org.eventb.core.scAction name="ACT3" org.eventb.core.assignment="snsrCableEngine ≔ CABLE_UNWIND" org.eventb.core.label="act4_4" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_WItq0OAzEd-73py7lbE8bg|org.eventb.core.action#_aG1QBdq-Ed-L_e8_V4iXIg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT29" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="STOP_CABLE_ENGINE" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_aG13ENq-Ed-L_e8_V4iXIg">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT29" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_aG13ENq-Ed-L_e8_V4iXIg|org.eventb.core.refinesEvent#_0nGIMO5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT29" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_aG13ENq-Ed-L_e8_V4iXIg|org.eventb.core.refinesEvent#_fbp4o-6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd4_1" org.eventb.core.predicate="PhyCableEngine≠CABLE_STOP" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_aG13ENq-Ed-L_e8_V4iXIg|org.eventb.core.guard#_aG13Edq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd4_2" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_aG13ENq-Ed-L_e8_V4iXIg|org.eventb.core.guard#_aG13Etq-Ed-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="PhyCableEngine ≔ CABLE_STOP" org.eventb.core.label="act4_1" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_aG13ENq-Ed-L_e8_V4iXIg|org.eventb.core.action#_aG13E9q-Ed-L_e8_V4iXIg"/>
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="snsrCableEngine ≔ CABLE_STOP" org.eventb.core.label="act4_2" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_aG13ENq-Ed-L_e8_V4iXIg|org.eventb.core.action#_aG13FNq-Ed-L_e8_V4iXIg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT30" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="open_door" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_HKimItqzEd-7IuFxCL4SWw">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT30" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_HKimItqzEd-7IuFxCL4SWw|org.eventb.core.refinesEvent#_0nGIMe5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT30" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_HKimItqzEd-7IuFxCL4SWw|org.eventb.core.refinesEvent#_fbqfsO6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd3_1" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_HKimItqzEd-7IuFxCL4SWw|org.eventb.core.guard#_HKjNMNqzEd-7IuFxCL4SWw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd3_2" org.eventb.core.predicate="opened=FALSE" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_HKimItqzEd-7IuFxCL4SWw|org.eventb.core.guard#_85BdkNqzEd-IzpmRUY7GDg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd4_1" org.eventb.core.predicate="snsrCableEngine=CABLE_STOP" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_HKimItqzEd-7IuFxCL4SWw|org.eventb.core.guard#_-PriIdrtEd-yLuKmXl8XEA" org.eventb.core.theorem="false"/>
@@ -415,13 +415,13 @@
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="opened ≔ TRUE" org.eventb.core.label="act3_2" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_HKimItqzEd-7IuFxCL4SWw|org.eventb.core.action#_85CEoNqzEd-IzpmRUY7GDg"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT31" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="stop_door" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_SjmMQNq3Ed-AAt710HomgA">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT31" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_SjmMQNq3Ed-AAt710HomgA|org.eventb.core.refinesEvent#_0nGvQO5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT31" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_SjmMQNq3Ed-AAt710HomgA|org.eventb.core.refinesEvent#_fbqfse6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd3_1" org.eventb.core.predicate="ctrlDoorCommand=DOOR_OPEN" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_SjmMQNq3Ed-AAt710HomgA|org.eventb.core.guard#_SjmzUNq3Ed-AAt710HomgA" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd7_1" org.eventb.core.predicate="snsrDoorPosition=DOOR_OPENED" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_SjmMQNq3Ed-AAt710HomgA|org.eventb.core.guard#_F6clEuA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="ctrlDoorCommand ≔ DOOR_STOP" org.eventb.core.label="act3_1" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_SjmMQNq3Ed-AAt710HomgA|org.eventb.core.action#_SjmzUdq3Ed-AAt710HomgA"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT32" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="close_door" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_HKjNMtqzEd-7IuFxCL4SWw">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT32" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_HKjNMtqzEd-7IuFxCL4SWw|org.eventb.core.refinesEvent#_0nGvQe5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT32" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_HKjNMtqzEd-7IuFxCL4SWw|org.eventb.core.refinesEvent#_fbqfsu6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd3_1" org.eventb.core.predicate="ctrlDoorCommand=DOOR_STOP" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_HKjNMtqzEd-7IuFxCL4SWw|org.eventb.core.guard#_HKj0QNqzEd-7IuFxCL4SWw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd7_1" org.eventb.core.predicate="snsrDoorEngine=DOOR_STOP" org.eventb.core.source="/ProvenLift/lift07_phys_door.bum|org.eventb.core.machineFile#lift07_phys_door|org.eventb.core.event#_HKjNMtqzEd-7IuFxCL4SWw|org.eventb.core.guard#_F6dMIeA2Ed-73py7lbE8bg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="ACT0" org.eventb.core.assignment="ctrlDoorCommand ≔ DOOR_CLOSE" org.eventb.core.label="act3_1" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_HKjNMtqzEd-7IuFxCL4SWw|org.eventb.core.action#_HKj0QdqzEd-7IuFxCL4SWw"/>
@@ -431,7 +431,7 @@
<org.eventb.core.scGuard name="GRD5" org.eventb.core.label="grd23_2" org.eventb.core.predicate="floor∉ctrlFloorButtonLightsSet" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_HKjNMtqzEd-7IuFxCL4SWw|org.eventb.core.guard#_UtpDUe5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT33" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="start_move_up" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT33" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.refinesEvent#_0nHWUO5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT33" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.refinesEvent#_fbrGwO6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd2_1" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.guard#_yC2sodqwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2_2" org.eventb.core.predicate="floor&lt;LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.guard#_yC2sotqwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd3_1" org.eventb.core.predicate="ctrlDoorCommand=DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.guard#_SjnaYdq3Ed-AAt710HomgA" org.eventb.core.theorem="false"/>
@@ -442,7 +442,7 @@
<org.eventb.core.scGuard name="GRD6" org.eventb.core.label="grd23_1" org.eventb.core.predicate="schedule=SCHEDULER_UP" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_yC2soNqwEd-O4vbSPlarTw|org.eventb.core.guard#_UtpDU-5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT34" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="move_up" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_9uFS0Nd9Ed-Dle0at0Xgqg">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT34" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_9uFS0Nd9Ed-Dle0at0Xgqg|org.eventb.core.refinesEvent#_0nHWUe5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT34" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_9uFS0Nd9Ed-Dle0at0Xgqg|org.eventb.core.refinesEvent#_fbrGwe6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1_1" org.eventb.core.predicate="floor&lt;LAST_FLOOR" org.eventb.core.source="/ProvenLift/lift01_floors.bum|org.eventb.core.machineFile#lift01_floors|org.eventb.core.event#_9uFS0Nd9Ed-Dle0at0Xgqg|org.eventb.core.guard#_9uFS0dd9Ed-Dle0at0Xgqg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2_1" org.eventb.core.predicate="ctrlCableCommand=CABLE_WIND" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_9uFS0Nd9Ed-Dle0at0Xgqg|org.eventb.core.guard#_yC3TsdqwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd4_1" org.eventb.core.predicate="floor&lt;snsrElevatorFloor" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_9uFS0Nd9Ed-Dle0at0Xgqg|org.eventb.core.guard#_BGpMMdrCEd-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
@@ -450,7 +450,7 @@
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="moved ≔ TRUE" org.eventb.core.label="act2_1" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_9uFS0Nd9Ed-Dle0at0Xgqg|org.eventb.core.action#_yC3TstqwEd-O4vbSPlarTw"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT35" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="start_move_down" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT35" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.refinesEvent#_0nH9YO5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT35" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.refinesEvent#_fbrt0O6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd2_1" org.eventb.core.predicate="ctrlCableCommand=CABLE_STOP" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.guard#_yC36wdqwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2_2" org.eventb.core.predicate="floor&gt;0" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.guard#_yC36wtqwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd3_1" org.eventb.core.predicate="ctrlDoorCommand=DOOR_CLOSE" org.eventb.core.source="/ProvenLift/lift03_door_engine.bum|org.eventb.core.machineFile#lift03_door_engine|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.guard#_SjoBcdq3Ed-AAt710HomgA" org.eventb.core.theorem="false"/>
@@ -461,7 +461,7 @@
<org.eventb.core.scGuard name="GRD6" org.eventb.core.label="grd23_1" org.eventb.core.predicate="schedule=SCHEDULER_DOWN" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_yC36wNqwEd-O4vbSPlarTw|org.eventb.core.guard#_UtpqYu5-Ed-dEtybZVK09Q" org.eventb.core.theorem="false"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT36" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="move_down" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_9uF54dd9Ed-Dle0at0Xgqg">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT36" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_9uF54dd9Ed-Dle0at0Xgqg|org.eventb.core.refinesEvent#_0nH9Ye5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT36" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_9uF54dd9Ed-Dle0at0Xgqg|org.eventb.core.refinesEvent#_fbrt0e6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd1_1" org.eventb.core.predicate="0&lt;floor" org.eventb.core.source="/ProvenLift/lift01_floors.bum|org.eventb.core.machineFile#lift01_floors|org.eventb.core.event#_9uF54dd9Ed-Dle0at0Xgqg|org.eventb.core.guard#_9uGg8Nd9Ed-Dle0at0Xgqg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2_1" org.eventb.core.predicate="ctrlCableCommand=CABLE_UNWIND" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_9uF54dd9Ed-Dle0at0Xgqg|org.eventb.core.guard#_yC4h0tqwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd4_1" org.eventb.core.predicate="snsrElevatorFloor≠−1" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_9uF54dd9Ed-Dle0at0Xgqg|org.eventb.core.guard#_BGpzQdrCEd-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
@@ -470,7 +470,7 @@
<org.eventb.core.scAction name="ACT1" org.eventb.core.assignment="moved ≔ TRUE" org.eventb.core.label="act2_1" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_9uF54dd9Ed-Dle0at0Xgqg|org.eventb.core.action#_yC5I4NqwEd-O4vbSPlarTw"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="EVT37" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="stop" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw">
-<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT37" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw|org.eventb.core.refinesEvent#_0nIkcO5-Ed-dEtybZVK09Q"/>
+<org.eventb.core.scRefinesEvent name="REF0" org.eventb.core.scTarget="/ProvenLift/lift22_conv_phys_light_off.bcm|org.eventb.core.scMachineFile#lift22_conv_phys_light_off|org.eventb.core.scEvent#EVT37" org.eventb.core.source="/ProvenLift/lift23_scheduler.bum|org.eventb.core.machineFile#lift23_scheduler|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw|org.eventb.core.refinesEvent#_fbsU4O6TEd-y3JdGki7orA"/>
<org.eventb.core.scGuard name="GRD0" org.eventb.core.label="grd2_1" org.eventb.core.predicate="ctrlCableCommand≠CABLE_STOP" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw|org.eventb.core.guard#_yC5I4tqwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD1" org.eventb.core.label="grd2_2" org.eventb.core.predicate="moved=TRUE" org.eventb.core.source="/ProvenLift/lift02_main_engine.bum|org.eventb.core.machineFile#lift02_main_engine|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw|org.eventb.core.guard#_yC5I49qwEd-O4vbSPlarTw" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="GRD2" org.eventb.core.label="grd4_1" org.eventb.core.predicate="snsrElevatorFloor≠−1" org.eventb.core.source="/ProvenLift/lift04_phys_main_engine.bum|org.eventb.core.machineFile#lift04_phys_main_engine|org.eventb.core.event#_yC5I4dqwEd-O4vbSPlarTw|org.eventb.core.guard#_BGpzQ9rCEd-L_e8_V4iXIg" org.eventb.core.theorem="false"/>
View
230 rodin/lift23_scheduler.bpo
115 additions, 115 deletions not shown
View
2,160 rodin/lift23_scheduler.bpr
325 additions, 1,835 deletions not shown
View
64 rodin/lift23_scheduler.bps
@@ -1,38 +1,38 @@
<?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="1" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="FIN" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIALISATION/inv23_3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIALISATION/inv23_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIALISATION/inv23_4/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="INITIALISATION/inv23_5/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="start_move_up/inv23_3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="start_move_up/inv23_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="start_move_up/inv23_5/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="move_up/inv23_3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="move_up/inv23_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="start_move_down/inv23_3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="start_move_down/inv23_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="start_move_down/inv23_5/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="move_down/inv23_3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="move_down/inv23_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="stop/inv23_3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="stop/inv23_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="stop/inv23_4/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="stop/inv23_5/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="switch_schedule_to_up/inv23_3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="switch_schedule_to_up/inv23_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="switch_schedule_to_up/inv23_5/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="switch_schedule_to_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="resume_schedule_up/inv23_3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="resume_schedule_up/inv23_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="resume_schedule_up/inv23_5/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="resume_schedule_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="switch_schedule_to_down/inv23_3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="switch_schedule_to_down/inv23_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="switch_schedule_to_down/inv23_5/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="switch_schedule_to_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="resume_schedule_down/inv23_3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="resume_schedule_down/inv23_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="resume_schedule_down/inv23_5/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
-<org.eventb.core.psStatus name="resume_schedule_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="1" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="INITIALISATION/inv23_5/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="start_move_up/inv23_3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="start_move_up/inv23_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="start_move_up/inv23_5/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="move_up/inv23_3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="move_up/inv23_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="start_move_down/inv23_3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="start_move_down/inv23_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="start_move_down/inv23_5/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="move_down/inv23_3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="move_down/inv23_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="stop/inv23_3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="stop/inv23_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="stop/inv23_4/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="stop/inv23_5/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="switch_schedule_to_up/inv23_3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="switch_schedule_to_up/inv23_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="switch_schedule_to_up/inv23_5/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="switch_schedule_to_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="resume_schedule_up/inv23_3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="resume_schedule_up/inv23_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="resume_schedule_up/inv23_5/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="resume_schedule_up/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="switch_schedule_to_down/inv23_3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="switch_schedule_to_down/inv23_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="switch_schedule_to_down/inv23_5/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="switch_schedule_to_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="resume_schedule_down/inv23_3/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="resume_schedule_down/inv23_2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="resume_schedule_down/inv23_5/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+<org.eventb.core.psStatus name="resume_schedule_down/VAR" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
</org.eventb.core.psFile>
View
94 rodin/lift23_scheduler.bum
@@ -1,7 +1,7 @@
<?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="1289581428735" org.eventb.texttools.text_representation="machine lift23_scheduler refines lift22_conv_phys_light_off sees ctx5_scheduler&#10;&#10;variables floor moved opened PhyCableEngine PhyElevatorFloor PhyElevatorBetweenTwoFloors ctrlCableCommand snsrCableEngine snsrElevatorFloor PhyDoorEngine PhyDoorPosition ctrlDoorCommand snsrDoorEngine snsrDoorPosition PhyFloorButtonsSet snsrFloorButtonsSet PhyFloorButtonLightsSet ctrlFloorButtonLightsSet PhyUpButtonsSet snsrUpButtonsSet PhyUpButtonLightsSet ctrlUpButtonLightsSet PhyDownButtonsSet snsrDownButtonsSet PhyDownButtonLightsSet ctrlDownButtonLightsSet last_schedule schedule&#10;&#10;invariants&#10; @inv23_1 schedule ∈ SCHEDULER_STRATEGY&#10; @inv23_3 ctrlCableCommand = CABLE_STOP ∧ floor = LAST_FLOOR ⇒ schedule ≠ SCHEDULER_UP&#10; @inv23_2 ctrlCableCommand = CABLE_STOP ∧ floor = 0 ⇒ schedule ≠ SCHEDULER_DOWN&#10; @inv23_4 last_schedule ∈ {SCHEDULER_UP, SCHEDULER_DOWN}&#10; @inv23_5 schedule = SCHEDULER_WAIT ⇒ ctrlCableCommand = CABLE_STOP&#10;// @inv23_6 schedule ≠ SCHEDULER_WAIT ⇒ (∃x·x∈0‥LAST_FLOOR ∧ x ≠ floor ∧ (x∈ctrlUpButtonLightsSet ∨ x∈ctrlFloorButtonLightsSet ∨ x∈ctrlDownButtonLightsSet))&#10;// @inv23_7 ¬(∃x· x∈0‥LAST_FLOOR ∧ (x∈ctrlUpButtonLightsSet ∨ x∈ctrlFloorButtonLightsSet ∨ x∈ctrlDownButtonLightsSet)) ⇒ schedule = SCHEDULER_WAIT ∧ snsrDoorPosition = DOOR_OPENED&#10;&#10;variant {schedule} ∩ {SCHEDULER_WAIT}&#10;&#10;events&#10; event INITIALISATION extends INITIALISATION&#10; then&#10; @act23_2 last_schedule ≔ SCHEDULER_UP&#10; @act23_1 schedule ≔ SCHEDULER_WAIT&#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; event TURNS_ON_DOWN_BUTTON_LIGHT extends TURNS_ON_DOWN_BUTTON_LIGHT&#10; end&#10;&#10; event TURNS_OFF_DOWN_BUTTON_LIGHT extends TURNS_OFF_DOWN_BUTTON_LIGHT&#10; end&#10;&#10; event turn_down_button_light_on extends turn_down_button_light_on&#10; end&#10;&#10; event turn_down_button_light_off extends turn_down_button_light_off&#10; where&#10; @grd23_1 schedule = SCHEDULER_DOWN&#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; event TURNS_ON_UP_BUTTON_LIGHT extends TURNS_ON_UP_BUTTON_LIGHT&#10; end&#10;&#10; event TURNS_OFF_UP_BUTTON_LIGHT extends TURNS_OFF_UP_BUTTON_LIGHT&#10; end&#10;&#10; event turn_up_button_light_on extends turn_up_button_light_on&#10; end&#10;&#10; event turn_up_button_light_off extends turn_up_button_light_off&#10; where&#10; @grd23_1 schedule = SCHEDULER_UP&#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; event TURNS_ON_FLOOR_BUTTON_LIGHT extends TURNS_ON_FLOOR_BUTTON_LIGHT&#10; end&#10;&#10; event TURNS_OFF_FLOOR_BUTTON_LIGHT extends TURNS_OFF_FLOOR_BUTTON_LIGHT&#10; end&#10;&#10; event turn_floor_button_light_on extends turn_floor_button_light_on&#10; end&#10;&#10; event turn_floor_button_light_off extends turn_floor_button_light_off&#10; end&#10;&#10; event DOOR_OPENS_WHEN_CLOSED extends DOOR_OPENS_WHEN_CLOSED&#10; end&#10;&#10; event DOOR_OPENS_WHEN_HALF extends DOOR_OPENS_WHEN_HALF&#10; end&#10;&#10; event DOOR_CLOSES_WHEN_OPENED extends DOOR_CLOSES_WHEN_OPENED&#10; end&#10;&#10; event DOOR_CLOSES_WHEN_HALF extends DOOR_CLOSES_WHEN_HALF&#10; end&#10;&#10; event DOOR_CLOSES_WHEN_CLOSED extends DOOR_CLOSES_WHEN_CLOSED&#10; end&#10;&#10; event STOP_DOOR_ENGINE extends STOP_DOOR_ENGINE&#10; end&#10;&#10; event ELEVATOR_LEAVES_FLOOR_UP extends ELEVATOR_LEAVES_FLOOR_UP&#10; end&#10;&#10; event ELEVATOR_REACHES_FLOOR_UP extends ELEVATOR_REACHES_FLOOR_UP&#10; end&#10;&#10; event ELEVATOR_LEAVES_FLOOR_DOWN extends ELEVATOR_LEAVES_FLOOR_DOWN&#10; end&#10;&#10; event ELEVATOR_REACHES_FLOOR_DOWN extends ELEVATOR_REACHES_FLOOR_DOWN&#10; end&#10;&#10; event STOP_CABLE_ENGINE extends STOP_CABLE_ENGINE&#10; end&#10;&#10; event open_door extends open_door&#10; end&#10;&#10; event stop_door extends stop_door&#10; end&#10;&#10; event close_door extends close_door&#10; where&#10; @grd23_4 schedule = SCHEDULER_DOWN ⇒ floor ∉ ctrlDownButtonLightsSet&#10; @grd23_3 schedule = SCHEDULER_UP ⇒ floor ∉ ctrlUpButtonLightsSet&#10; @grd23_1 schedule ≠ SCHEDULER_WAIT&#10; @grd23_2 floor ∉ ctrlFloorButtonLightsSet&#10; end&#10;&#10; event start_move_up extends start_move_up&#10; where&#10; @grd23_1 schedule = SCHEDULER_UP&#10; end&#10;&#10; event move_up extends move_up&#10; end&#10;&#10; event start_move_down extends start_move_down&#10; where&#10; @grd23_1 schedule = SCHEDULER_DOWN&#10; end&#10;&#10; event move_down extends move_down&#10; end&#10;&#10; event stop extends stop&#10; where&#10; @grd23_1 (floor∈ctrlFloorButtonLightsSet) ∨&#10; (floor∈ctrlUpButtonLightsSet ∧ schedule = SCHEDULER_UP) ∨&#10; (floor∈ctrlDownButtonLightsSet ∧ schedule = SCHEDULER_DOWN) ∨&#10; (floor∈ctrlUpButtonLightsSet ∧ schedule = SCHEDULER_DOWN ∧ (∀x·x∈0‥floor−1 ⇒ (x∉ctrlUpButtonLightsSet ∧ x∉ctrlDownButtonLightsSet ∧ x∉ctrlFloorButtonLightsSet))) ∨&#10; (floor∈ctrlDownButtonLightsSet ∧ schedule = SCHEDULER_UP ∧ (∀y·y∈floor+1‥LAST_FLOOR ⇒ (y∉ctrlUpButtonLightsSet ∧ y∉ctrlDownButtonLightsSet ∧ y∉ctrlFloorButtonLightsSet)))&#10; then&#10; @act23_2 schedule ≔ SCHEDULER_WAIT&#10; @act23_1 last_schedule ≔ schedule&#10; end&#10;&#10; convergent event switch_schedule_to_up&#10; any x y&#10; where&#10; @grd23_0 snsrDoorPosition = DOOR_OPENED&#10; @grd23_1 schedule = SCHEDULER_WAIT&#10; @grd23_2 x ∈ 0‥floor−1&#10; @grd23_3 ¬ (x∈ctrlUpButtonLightsSet ∨ x∈ctrlFloorButtonLightsSet ∨ x∈ctrlDownButtonLightsSet)&#10; @grd23_4 y ∈ floor+1‥LAST_FLOOR&#10; @grd23_5 y∈ctrlUpButtonLightsSet ∨ y∈ctrlFloorButtonLightsSet ∨ y∈ctrlDownButtonLightsSet&#10; @grd23_6 last_schedule = SCHEDULER_DOWN&#10; then&#10; @act23_1 schedule ≔ SCHEDULER_UP&#10; end&#10;&#10; convergent event resume_schedule_up&#10; any x&#10; where&#10; @grd23_0 snsrDoorPosition = DOOR_OPENED&#10; @grd23_1 schedule = SCHEDULER_WAIT&#10; @grd23_2 x ∈ floor+1‥LAST_FLOOR&#10; @grd23_3 x∈ctrlUpButtonLightsSet ∨ x∈ctrlFloorButtonLightsSet ∨ x∈ctrlDownButtonLightsSet&#10; @grd23_4 last_schedule = SCHEDULER_UP&#10; then&#10; @act23_1 schedule ≔ SCHEDULER_UP&#10; end&#10;&#10; convergent event switch_schedule_to_down&#10; any x y&#10; where&#10; @grd23_0 snsrDoorPosition = DOOR_OPENED&#10; @grd23_1 schedule = SCHEDULER_WAIT&#10; @grd23_2 x ∈ floor+1‥LAST_FLOOR&#10; @grd23_3 ¬ (x∈ctrlUpButtonLightsSet ∨ x∈ctrlFloorButtonLightsSet ∨ x∈ctrlDownButtonLightsSet)&#10; @grd23_4 y ∈ 0‥floor−1&#10; @grd23_5 y∈ctrlUpButtonLightsSet ∨ y∈ctrlFloorButtonLightsSet ∨ y∈ctrlDownButtonLightsSet&#10; @grd23_6 last_schedule = SCHEDULER_UP&#10; then&#10; @act23_1 schedule ≔ SCHEDULER_DOWN&#10; end&#10;&#10; convergent event resume_schedule_down&#10; any x&#10; where&#10; @grd23_0 snsrDoorPosition = DOOR_OPENED&#10; @grd23_1 schedule = SCHEDULER_WAIT&#10; @grd23_2 x ∈ 0‥floor−1&#10; @grd23_3 x∈ctrlUpButtonLightsSet ∨ x∈ctrlFloorButtonLightsSet ∨ x∈ctrlDownButtonLightsSet&#10; @grd23_4 last_schedule = SCHEDULER_DOWN&#10; then&#10; @act23_1 schedule ≔ SCHEDULER_DOWN&#10; end&#10;end&#10;" version="5">
-<org.eventb.core.refinesMachine name="_0m8XMO5-Ed-dEtybZVK09Q" org.eventb.core.target="lift22_conv_phys_light_off"/>
-<org.eventb.core.seesContext name="_0m8-QO5-Ed-dEtybZVK09Q" org.eventb.core.target="ctx5_scheduler"/>
+<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.texttools.text_lastmodified="1289590307080" org.eventb.texttools.text_representation="machine lift23_scheduler refines lift22_conv_phys_light_off sees ctx5_scheduler&#10;&#10;variables floor moved opened PhyCableEngine PhyElevatorFloor PhyElevatorBetweenTwoFloors ctrlCableCommand snsrCableEngine snsrElevatorFloor PhyDoorEngine PhyDoorPosition ctrlDoorCommand snsrDoorEngine snsrDoorPosition PhyFloorButtonsSet snsrFloorButtonsSet PhyFloorButtonLightsSet ctrlFloorButtonLightsSet PhyUpButtonsSet snsrUpButtonsSet PhyUpButtonLightsSet ctrlUpButtonLightsSet PhyDownButtonsSet snsrDownButtonsSet PhyDownButtonLightsSet ctrlDownButtonLightsSet last_schedule schedule&#10;&#10;invariants&#10; @inv23_1 schedule ∈ SCHEDULER_STRATEGY&#10; @inv23_3 ctrlCableCommand = CABLE_STOP ∧ floor = LAST_FLOOR ⇒ schedule ≠ SCHEDULER_UP&#10; @inv23_2 ctrlCableCommand = CABLE_STOP ∧ floor = 0 ⇒ schedule ≠ SCHEDULER_DOWN&#10; @inv23_4 last_schedule ∈ {SCHEDULER_UP, SCHEDULER_DOWN}&#10; @inv23_5 schedule = SCHEDULER_WAIT ⇒ ctrlCableCommand = CABLE_STOP&#10;// @inv23_7 schedule ≠ SCHEDULER_WAIT ⇒ (∃x·x∈0‥LAST_FLOOR ∧ x ≠ floor ∧ (x∈ctrlUpButtonLightsSet ∨ x∈ctrlFloorButtonLightsSet ∨ x∈ctrlDownButtonLightsSet))&#10;// @inv23_6 ¬(∃x· x∈0‥LAST_FLOOR ∧ (x∈ctrlUpButtonLightsSet ∨ x∈ctrlFloorButtonLightsSet ∨ x∈ctrlDownButtonLightsSet)) ⇒ schedule = SCHEDULER_WAIT ∧ snsrDoorPosition = DOOR_OPENED&#10;&#10;variant {schedule} ∩ {SCHEDULER_WAIT}&#10;&#10;events&#10; event INITIALISATION extends INITIALISATION&#10; then&#10; @act23_2 last_schedule ≔ SCHEDULER_UP&#10; @act23_1 schedule ≔ SCHEDULER_WAIT&#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; event TURNS_ON_DOWN_BUTTON_LIGHT extends TURNS_ON_DOWN_BUTTON_LIGHT&#10; end&#10;&#10; event TURNS_OFF_DOWN_BUTTON_LIGHT extends TURNS_OFF_DOWN_BUTTON_LIGHT&#10; end&#10;&#10; event turn_down_button_light_on extends turn_down_button_light_on&#10; end&#10;&#10; event turn_down_button_light_off extends turn_down_button_light_off&#10; where&#10; @grd23_1 schedule = SCHEDULER_DOWN&#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; event TURNS_ON_UP_BUTTON_LIGHT extends TURNS_ON_UP_BUTTON_LIGHT&#10; end&#10;&#10; event TURNS_OFF_UP_BUTTON_LIGHT extends TURNS_OFF_UP_BUTTON_LIGHT&#10; end&#10;&#10; event turn_up_button_light_on extends turn_up_button_light_on&#10; end&#10;&#10; event turn_up_button_light_off extends turn_up_button_light_off&#10; where&#10; @grd23_1 schedule = SCHEDULER_UP&#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; event TURNS_ON_FLOOR_BUTTON_LIGHT extends TURNS_ON_FLOOR_BUTTON_LIGHT&#10; end&#10;&#10; event TURNS_OFF_FLOOR_BUTTON_LIGHT extends TURNS_OFF_FLOOR_BUTTON_LIGHT&#10; end&#10;&#10; event turn_floor_button_light_on extends turn_floor_button_light_on&#10; end&#10;&#10; event turn_floor_button_light_off extends turn_floor_button_light_off&#10; end&#10;&#10; event DOOR_OPENS_WHEN_CLOSED extends DOOR_OPENS_WHEN_CLOSED&#10; end&#10;&#10; event DOOR_OPENS_WHEN_HALF extends DOOR_OPENS_WHEN_HALF&#10; end&#10;&#10; event DOOR_CLOSES_WHEN_OPENED extends DOOR_CLOSES_WHEN_OPENED&#10; end&#10;&#10; event DOOR_CLOSES_WHEN_HALF extends DOOR_CLOSES_WHEN_HALF&#10; end&#10;&#10; event DOOR_CLOSES_WHEN_CLOSED extends DOOR_CLOSES_WHEN_CLOSED&#10; end&#10;&#10; event STOP_DOOR_ENGINE extends STOP_DOOR_ENGINE&#10; end&#10;&#10; event ELEVATOR_LEAVES_FLOOR_UP extends ELEVATOR_LEAVES_FLOOR_UP&#10; end&#10;&#10; event ELEVATOR_REACHES_FLOOR_UP extends ELEVATOR_REACHES_FLOOR_UP&#10; end&#10;&#10; event ELEVATOR_LEAVES_FLOOR_DOWN extends ELEVATOR_LEAVES_FLOOR_DOWN&#10; end&#10;&#10; event ELEVATOR_REACHES_FLOOR_DOWN extends ELEVATOR_REACHES_FLOOR_DOWN&#10; end&#10;&#10; event STOP_CABLE_ENGINE extends STOP_CABLE_ENGINE&#10; end&#10;&#10; event open_door extends open_door&#10; end&#10;&#10; event stop_door extends stop_door&#10; end&#10;&#10; event close_door extends close_door&#10; where&#10; @grd23_4 schedule = SCHEDULER_DOWN ⇒ floor ∉ ctrlDownButtonLightsSet&#10; @grd23_3 schedule = SCHEDULER_UP ⇒ floor ∉ ctrlUpButtonLightsSet&#10; @grd23_1 schedule ≠ SCHEDULER_WAIT&#10; @grd23_2 floor ∉ ctrlFloorButtonLightsSet&#10; end&#10;&#10; event start_move_up extends start_move_up&#10; where&#10; @grd23_1 schedule = SCHEDULER_UP&#10; end&#10;&#10; event move_up extends move_up&#10; end&#10;&#10; event start_move_down extends start_move_down&#10; where&#10; @grd23_1 schedule = SCHEDULER_DOWN&#10; end&#10;&#10; event move_down extends move_down&#10; end&#10;&#10; event stop extends stop&#10; where&#10; @grd23_1 (floor∈ctrlFloorButtonLightsSet) ∨&#10; (floor∈ctrlUpButtonLightsSet ∧ schedule = SCHEDULER_UP) ∨&#10; (floor∈ctrlDownButtonLightsSet ∧ schedule = SCHEDULER_DOWN) ∨&#10; (floor∈ctrlUpButtonLightsSet ∧ schedule = SCHEDULER_DOWN ∧ (∀x·x∈0‥floor−1 ⇒ (x∉ctrlUpButtonLightsSet ∧ x∉ctrlDownButtonLightsSet ∧ x∉ctrlFloorButtonLightsSet))) ∨&#10; (floor∈ctrlDownButtonLightsSet ∧ schedule = SCHEDULER_UP ∧ (∀y·y∈floor+1‥LAST_FLOOR ⇒ (y∉ctrlUpButtonLightsSet ∧ y∉ctrlDownButtonLightsSet ∧ y∉ctrlFloorButtonLightsSet)))&#10; then&#10; @act23_2 schedule ≔ SCHEDULER_WAIT&#10; @act23_1 last_schedule ≔ schedule&#10; end&#10;&#10; convergent event switch_schedule_to_up&#10; any x y&#10; where&#10; @grd23_0 snsrDoorPosition = DOOR_OPENED&#10; @grd23_1 schedule = SCHEDULER_WAIT&#10; @grd23_2 x ∈ 0‥floor−1&#10; @grd23_3 ¬ (x∈ctrlUpButtonLightsSet ∨ x∈ctrlFloorButtonLightsSet ∨ x∈ctrlDownButtonLightsSet)&#10; @grd23_4 y ∈ floor+1‥LAST_FLOOR&#10; @grd23_5 y∈ctrlUpButtonLightsSet ∨ y∈ctrlFloorButtonLightsSet ∨ y∈ctrlDownButtonLightsSet&#10; @grd23_6 last_schedule = SCHEDULER_DOWN&#10; then&#10; @act23_1 schedule ≔ SCHEDULER_UP&#10; end&#10;&#10; convergent event resume_schedule_up&#10; any x&#10; where&#10; @grd23_0 snsrDoorPosition = DOOR_OPENED&#10; @grd23_1 schedule = SCHEDULER_WAIT&#10; @grd23_2 x ∈ floor+1‥LAST_FLOOR&#10; @grd23_3 x∈ctrlUpButtonLightsSet ∨ x∈ctrlFloorButtonLightsSet ∨ x∈ctrlDownButtonLightsSet&#10; @grd23_4 last_schedule = SCHEDULER_UP&#10; then&#10; @act23_1 schedule ≔ SCHEDULER_UP&#10; end&#10;&#10; convergent event switch_schedule_to_down&#10; any x y&#10; where&#10; @grd23_0 snsrDoorPosition = DOOR_OPENED&#10; @grd23_1 schedule = SCHEDULER_WAIT&#10; @grd23_2 x ∈ floor+1‥LAST_FLOOR&#10; @grd23_3 ¬ (x∈ctrlUpButtonLightsSet ∨ x∈ctrlFloorButtonLightsSet ∨ x∈ctrlDownButtonLightsSet)&#10; @grd23_4 y ∈ 0‥floor−1&#10; @grd23_5 y∈ctrlUpButtonLightsSet ∨ y∈ctrlFloorButtonLightsSet ∨ y∈ctrlDownButtonLightsSet&#10; @grd23_6 last_schedule = SCHEDULER_UP&#10; then&#10; @act23_1 schedule ≔ SCHEDULER_DOWN&#10; end&#10;&#10; convergent event resume_schedule_down&#10; any x&#10; where&#10; @grd23_0 snsrDoorPosition = DOOR_OPENED&#10; @grd23_1 schedule = SCHEDULER_WAIT&#10; @grd23_2 x ∈ 0‥floor−1&#10; @grd23_3 x∈ctrlUpButtonLightsSet ∨ x∈ctrlFloorButtonLightsSet ∨ x∈ctrlDownButtonLightsSet&#10; @grd23_4 last_schedule = SCHEDULER_DOWN&#10; then&#10; @act23_1 schedule ≔ SCHEDULER_DOWN&#10; end&#10;end&#10;" version="5">
+<org.eventb.core.refinesMachine name="_fbh80O6TEd-y3JdGki7orA" org.eventb.core.target="lift22_conv_phys_light_off"/>
+<org.eventb.core.seesContext name="_fbh80e6TEd-y3JdGki7orA" org.eventb.core.target="ctx5_scheduler"/>
<org.eventb.core.variable name="_9uEEsNd9Ed-Dle0at0Xgqg" org.eventb.core.identifier="floor"/>
<org.eventb.core.variable name="_BGiegNrCEd-L_e8_V4iXIg" org.eventb.core.identifier="moved"/>
<org.eventb.core.variable name="_84_BUNqzEd-IzpmRUY7GDg" org.eventb.core.identifier="opened"/>
@@ -34,130 +34,130 @@
<org.eventb.core.invariant name="_UthHge5-Ed-dEtybZVK09Q" org.eventb.core.label="inv23_3" org.eventb.core.predicate="ctrlCableCommand = CABLE_STOP ∧ floor = LAST_FLOOR ⇒ schedule ≠ SCHEDULER_UP"/>
<org.eventb.core.invariant name="_UthHgu5-Ed-dEtybZVK09Q" org.eventb.core.label="inv23_2" org.eventb.core.predicate="ctrlCableCommand = CABLE_STOP ∧ floor = 0 ⇒ schedule ≠ SCHEDULER_DOWN"/>
<org.eventb.core.invariant name="_UthHg-5-Ed-dEtybZVK09Q" org.eventb.core.label="inv23_4" org.eventb.core.predicate="last_schedule ∈ {SCHEDULER_UP, SCHEDULER_DOWN}"/>
-<org.eventb.core.invariant name="_0m_agO5-Ed-dEtybZVK09Q" org.eventb.core.comment="@inv23_6 schedule ≠ SCHEDULER_WAIT ⇒ (∃x·x∈0‥LAST_FLOOR ∧ x ≠ floor ∧ (x∈ctrlUpButtonLightsSet ∨ x∈ctrlFloorButtonLightsSet ∨ x∈ctrlDownButtonLightsSet))&#10;@inv23_7 ¬(∃x· x∈0‥LAST_FLOOR ∧ (x∈ctrlUpButtonLightsSet ∨ x∈ctrlFloorButtonLightsSet ∨ x∈ctrlDownButtonLightsSet)) ⇒ schedule = SCHEDULER_WAIT ∧ snsrDoorPosition = DOOR_OPENED" org.eventb.core.label="inv23_5" org.eventb.core.predicate="schedule = SCHEDULER_WAIT ⇒ ctrlCableCommand = CABLE_STOP"/>
+<org.eventb.core.invariant name="_0m_agO5-Ed-dEtybZVK09Q" org.eventb.core.comment="@inv23_7 schedule ≠ SCHEDULER_WAIT ⇒ (∃x·x∈0‥LAST_FLOOR ∧ x ≠ floor ∧ (x∈ctrlUpButtonLightsSet ∨ x∈ctrlFloorButtonLightsSet ∨ x∈ctrlDownButtonLightsSet))&#10;@inv23_6 ¬(∃x· x∈0‥LAST_FLOOR ∧ (x∈ctrlUpButtonLightsSet ∨ x∈ctrlFloorButtonLightsSet ∨ x∈ctrlDownButtonLightsSet)) ⇒ schedule = SCHEDULER_WAIT ∧ snsrDoorPosition = DOOR_OPENED" org.eventb.core.label="inv23_5" org.eventb.core.predicate="schedule = SCHEDULER_WAIT ⇒ ctrlCableCommand = CABLE_STOP"/>
<org.eventb.core.variant name="_UthukO5-Ed-dEtybZVK09Q" org.eventb.core.expression="{schedule} ∩ {SCHEDULER_WAIT}"/>
<org.eventb.core.event name="'" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION">
<org.eventb.core.action name="_Uthuke5-Ed-dEtybZVK09Q" org.eventb.core.assignment="last_schedule ≔ SCHEDULER_UP" org.eventb.core.label="act23_2"/>
<org.eventb.core.action name="_Uthuku5-Ed-dEtybZVK09Q" org.eventb.core.assignment="schedule ≔ SCHEDULER_WAIT" org.eventb.core.label="act23_1"/>
</org.eventb.core.event>
<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="_0nABkO5-Ed-dEtybZVK09Q" org.eventb.core.target="USER_PRESSES_DOWN_BUTTON"/>
+<org.eventb.core.refinesEvent name="_fblAIO6TEd-y3JdGki7orA" org.eventb.core.target="USER_PRESSES_DOWN_BUTTON"/>
</org.eventb.core.event>
-<org.eventb.core.event name="_0nABke5-Ed-dEtybZVK09Q" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_DOWN_BUTTON">
-<org.eventb.core.refinesEvent name="_0nABku5-Ed-dEtybZVK09Q" org.eventb.core.target="USER_RELEASES_DOWN_BUTTON"/>
+<org.eventb.core.event name="_fblAIe6TEd-y3JdGki7orA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_DOWN_BUTTON">
+<org.eventb.core.refinesEvent name="_fblAIu6TEd-y3JdGki7orA" org.eventb.core.target="USER_RELEASES_DOWN_BUTTON"/>
</org.eventb.core.event>
<org.eventb.core.event name="_3Il25eWyEd-64JNDK1TKiQ" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="TURNS_ON_DOWN_BUTTON_LIGHT">
-<org.eventb.core.refinesEvent name="_0nAooO5-Ed-dEtybZVK09Q" org.eventb.core.target="TURNS_ON_DOWN_BUTTON_LIGHT"/>
+<org.eventb.core.refinesEvent name="_fblAI-6TEd-y3JdGki7orA" org.eventb.core.target="TURNS_ON_DOWN_BUTTON_LIGHT"/>
</org.eventb.core.event>
<org.eventb.core.event name="_3Imd9eWyEd-64JNDK1TKiQ" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="TURNS_OFF_DOWN_BUTTON_LIGHT">
-<org.eventb.core.refinesEvent name="_0nAooe5-Ed-dEtybZVK09Q" org.eventb.core.target="TURNS_OFF_DOWN_BUTTON_LIGHT"/>
+<org.eventb.core.refinesEvent name="_fblnMO6TEd-y3JdGki7orA" org.eventb.core.target="TURNS_OFF_DOWN_BUTTON_LIGHT"/>
</org.eventb.core.event>
<org.eventb.core.event name="_3InsEuWyEd-64JNDK1TKiQ" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="turn_down_button_light_on">
-<org.eventb.core.refinesEvent name="_0nAoou5-Ed-dEtybZVK09Q" org.eventb.core.target="turn_down_button_light_on"/>
+<org.eventb.core.refinesEvent name="_fblnMe6TEd-y3JdGki7orA" 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="0" org.eventb.core.extended="true" org.eventb.core.label="turn_down_button_light_off">
-<org.eventb.core.refinesEvent name="_0nAoo-5-Ed-dEtybZVK09Q" org.eventb.core.target="turn_down_button_light_off"/>
+<org.eventb.core.refinesEvent name="_fblnMu6TEd-y3JdGki7orA" org.eventb.core.target="turn_down_button_light_off"/>
<org.eventb.core.guard name="_Uti8su5-Ed-dEtybZVK09Q" org.eventb.core.label="grd23_1" org.eventb.core.predicate="schedule = SCHEDULER_DOWN"/>
</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="_0nBPsO5-Ed-dEtybZVK09Q" org.eventb.core.target="USER_PRESSES_UP_BUTTON"/>
+<org.eventb.core.refinesEvent name="_fbmOQO6TEd-y3JdGki7orA" 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="_0nBPse5-Ed-dEtybZVK09Q" org.eventb.core.target="USER_RELEASES_UP_BUTTON"/>
+<org.eventb.core.refinesEvent name="_fbmOQe6TEd-y3JdGki7orA" org.eventb.core.target="USER_RELEASES_UP_BUTTON"/>
</org.eventb.core.event>
<org.eventb.core.event name="_pvV5BuEsEd-bh-7nDQnLgQ" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="TURNS_ON_UP_BUTTON_LIGHT">
-<org.eventb.core.refinesEvent name="_0nB2wO5-Ed-dEtybZVK09Q" org.eventb.core.target="TURNS_ON_UP_BUTTON_LIGHT"/>
+<org.eventb.core.refinesEvent name="_fbmOQu6TEd-y3JdGki7orA" 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="0" org.eventb.core.extended="true" org.eventb.core.label="TURNS_OFF_UP_BUTTON_LIGHT">
-<org.eventb.core.refinesEvent name="_0nB2we5-Ed-dEtybZVK09Q" org.eventb.core.target="TURNS_OFF_UP_BUTTON_LIGHT"/>
+<org.eventb.core.refinesEvent name="_fbmOQ-6TEd-y3JdGki7orA" 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="0" org.eventb.core.extended="true" org.eventb.core.label="turn_up_button_light_on">
-<org.eventb.core.refinesEvent name="_0nB2wu5-Ed-dEtybZVK09Q" org.eventb.core.target="turn_up_button_light_on"/>
+<org.eventb.core.refinesEvent name="_fbm1UO6TEd-y3JdGki7orA" 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="0" org.eventb.core.extended="true" org.eventb.core.label="turn_up_button_light_off">
-<org.eventb.core.refinesEvent name="_0nCd0O5-Ed-dEtybZVK09Q" org.eventb.core.target="turn_up_button_light_off"/>
+<org.eventb.core.refinesEvent name="_fbm1Ue6TEd-y3JdGki7orA" org.eventb.core.target="turn_up_button_light_off"/>
<org.eventb.core.guard name="_UtkK0u5-Ed-dEtybZVK09Q" org.eventb.core.label="grd23_1" org.eventb.core.predicate="schedule = SCHEDULER_UP"/>
</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="_0nCd0e5-Ed-dEtybZVK09Q" org.eventb.core.target="USER_PRESSES_FLOOR_BUTTON"/>
+<org.eventb.core.refinesEvent name="_fbm1Uu6TEd-y3JdGki7orA" org.eventb.core.target="USER_PRESSES_FLOOR_BUTTON"/>
</org.eventb.core.event>
-<org.eventb.core.event name="_0nCd0u5-Ed-dEtybZVK09Q" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_FLOOR_BUTTON">
-<org.eventb.core.refinesEvent name="_0nCd0-5-Ed-dEtybZVK09Q" org.eventb.core.target="USER_RELEASES_FLOOR_BUTTON"/>
+<org.eventb.core.event name="_fbm1U-6TEd-y3JdGki7orA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="USER_RELEASES_FLOOR_BUTTON">
+<org.eventb.core.refinesEvent name="_fbncYO6TEd-y3JdGki7orA" 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="0" org.eventb.core.extended="true" org.eventb.core.label="TURNS_ON_FLOOR_BUTTON_LIGHT">
-<org.eventb.core.refinesEvent name="_0nDE4O5-Ed-dEtybZVK09Q" org.eventb.core.target="TURNS_ON_FLOOR_BUTTON_LIGHT"/>
+<org.eventb.core.refinesEvent name="_fbncYe6TEd-y3JdGki7orA" 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="0" org.eventb.core.extended="true" org.eventb.core.label="TURNS_OFF_FLOOR_BUTTON_LIGHT">
-<org.eventb.core.refinesEvent name="_0nDE4e5-Ed-dEtybZVK09Q" org.eventb.core.target="TURNS_OFF_FLOOR_BUTTON_LIGHT"/>
+<org.eventb.core.refinesEvent name="_fbncYu6TEd-y3JdGki7orA" 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="0" org.eventb.core.extended="true" org.eventb.core.label="turn_floor_button_light_on">
-<org.eventb.core.refinesEvent name="_0nDr8O5-Ed-dEtybZVK09Q" org.eventb.core.target="turn_floor_button_light_on"/>
+<org.eventb.core.refinesEvent name="_fboDcO6TEd-y3JdGki7orA" 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="0" org.eventb.core.extended="true" org.eventb.core.label="turn_floor_button_light_off">
-<org.eventb.core.refinesEvent name="_0nDr8e5-Ed-dEtybZVK09Q" org.eventb.core.target="turn_floor_button_light_off"/>
+<org.eventb.core.refinesEvent name="_fboDce6TEd-y3JdGki7orA" org.eventb.core.target="turn_floor_button_light_off"/>
</org.eventb.core.event>
<org.eventb.core.event name="_KgayBOAzEd-73py7lbE8bg" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="DOOR_OPENS_WHEN_CLOSED">
-<org.eventb.core.refinesEvent name="_0nDr8u5-Ed-dEtybZVK09Q" org.eventb.core.target="DOOR_OPENS_WHEN_CLOSED"/>
+<org.eventb.core.refinesEvent name="_fboDcu6TEd-y3JdGki7orA" org.eventb.core.target="DOOR_OPENS_WHEN_CLOSED"/>
</org.eventb.core.event>
<org.eventb.core.event name="_KgcAIOAzEd-73py7lbE8bg" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="DOOR_OPENS_WHEN_HALF">
-<org.eventb.core.refinesEvent name="_0nETAO5-Ed-dEtybZVK09Q" org.eventb.core.target="DOOR_OPENS_WHEN_HALF"/>
+<org.eventb.core.refinesEvent name="_fboDc-6TEd-y3JdGki7orA" org.eventb.core.target="DOOR_OPENS_WHEN_HALF"/>
</org.eventb.core.event>
<org.eventb.core.event name="_KgcnM-AzEd-73py7lbE8bg" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="DOOR_CLOSES_WHEN_OPENED">
-<org.eventb.core.refinesEvent name="_0nETAe5-Ed-dEtybZVK09Q" org.eventb.core.target="DOOR_CLOSES_WHEN_OPENED"/>
+<org.eventb.core.refinesEvent name="_fboqgO6TEd-y3JdGki7orA" org.eventb.core.target="DOOR_CLOSES_WHEN_OPENED"/>
</org.eventb.core.event>
<org.eventb.core.event name="_KgdOReAzEd-73py7lbE8bg" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="DOOR_CLOSES_WHEN_HALF">
-<org.eventb.core.refinesEvent name="_0nETAu5-Ed-dEtybZVK09Q" org.eventb.core.target="DOOR_CLOSES_WHEN_HALF"/>
+<org.eventb.core.refinesEvent name="_fboqge6TEd-y3JdGki7orA" org.eventb.core.target="DOOR_CLOSES_WHEN_HALF"/>
</org.eventb.core.event>
<org.eventb.core.event name="_KgecYeAzEd-73py7lbE8bg" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="DOOR_CLOSES_WHEN_CLOSED">
-<org.eventb.core.refinesEvent name="_0nE6EO5-Ed-dEtybZVK09Q" org.eventb.core.target="DOOR_CLOSES_WHEN_CLOSED"/>
+<org.eventb.core.refinesEvent name="_fboqgu6TEd-y3JdGki7orA" org.eventb.core.target="DOOR_CLOSES_WHEN_CLOSED"/>
</org.eventb.core.event>
<org.eventb.core.event name="_KgfDcuAzEd-73py7lbE8bg" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="STOP_DOOR_ENGINE">
-<org.eventb.core.refinesEvent name="_0nE6Ee5-Ed-dEtybZVK09Q" org.eventb.core.target="STOP_DOOR_ENGINE"/>
+<org.eventb.core.refinesEvent name="_fbpRkO6TEd-y3JdGki7orA" org.eventb.core.target="STOP_DOOR_ENGINE"/>
</org.eventb.core.event>
-<org.eventb.core.event name="_0nE6Eu5-Ed-dEtybZVK09Q" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_UP">
-<org.eventb.core.refinesEvent name="_0nE6E-5-Ed-dEtybZVK09Q" org.eventb.core.target="ELEVATOR_LEAVES_FLOOR_UP"/>
+<org.eventb.core.event name="_fbpRke6TEd-y3JdGki7orA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_UP">
+<org.eventb.core.refinesEvent name="_fbpRku6TEd-y3JdGki7orA" org.eventb.core.target="ELEVATOR_LEAVES_FLOOR_UP"/>
</org.eventb.core.event>
-<org.eventb.core.event name="_0nE6FO5-Ed-dEtybZVK09Q" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_UP">
-<org.eventb.core.refinesEvent name="_0nFhIO5-Ed-dEtybZVK09Q" org.eventb.core.target="ELEVATOR_REACHES_FLOOR_UP"/>
+<org.eventb.core.event name="_fbpRk-6TEd-y3JdGki7orA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_UP">
+<org.eventb.core.refinesEvent name="_fbpRlO6TEd-y3JdGki7orA" org.eventb.core.target="ELEVATOR_REACHES_FLOOR_UP"/>
</org.eventb.core.event>
-<org.eventb.core.event name="_0nFhIe5-Ed-dEtybZVK09Q" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_DOWN">
-<org.eventb.core.refinesEvent name="_0nFhIu5-Ed-dEtybZVK09Q" org.eventb.core.target="ELEVATOR_LEAVES_FLOOR_DOWN"/>
+<org.eventb.core.event name="_fbpRle6TEd-y3JdGki7orA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_LEAVES_FLOOR_DOWN">
+<org.eventb.core.refinesEvent name="_fbp4oO6TEd-y3JdGki7orA" org.eventb.core.target="ELEVATOR_LEAVES_FLOOR_DOWN"/>
</org.eventb.core.event>
-<org.eventb.core.event name="_0nFhI-5-Ed-dEtybZVK09Q" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_DOWN">
-<org.eventb.core.refinesEvent name="_0nFhJO5-Ed-dEtybZVK09Q" org.eventb.core.target="ELEVATOR_REACHES_FLOOR_DOWN"/>
+<org.eventb.core.event name="_fbp4oe6TEd-y3JdGki7orA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="ELEVATOR_REACHES_FLOOR_DOWN">
+<org.eventb.core.refinesEvent name="_fbp4ou6TEd-y3JdGki7orA" 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="0" org.eventb.core.extended="true" org.eventb.core.label="STOP_CABLE_ENGINE">
-<org.eventb.core.refinesEvent name="_0nGIMO5-Ed-dEtybZVK09Q" org.eventb.core.target="STOP_CABLE_ENGINE"/>
+<org.eventb.core.refinesEvent name="_fbp4o-6TEd-y3JdGki7orA" org.eventb.core.target="STOP_CABLE_ENGINE"/>
</org.eventb.core.event>
<org.eventb.core.event name="_HKimItqzEd-7IuFxCL4SWw" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="open_door">
-<org.eventb.core.refinesEvent name="_0nGIMe5-Ed-dEtybZVK09Q" org.eventb.core.target="open_door"/>
+<org.eventb.core.refinesEvent name="_fbqfsO6TEd-y3JdGki7orA" org.eventb.core.target="open_door"/>
</org.eventb.core.event>
<org.eventb.core.event name="_SjmMQNq3Ed-AAt710HomgA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="stop_door">
-<org.eventb.core.refinesEvent name="_0nGvQO5-Ed-dEtybZVK09Q" org.eventb.core.target="stop_door"/>
+<org.eventb.core.refinesEvent name="_fbqfse6TEd-y3JdGki7orA" org.eventb.core.target="stop_door"/>
</org.eventb.core.event>
<org.eventb.core.event name="_HKjNMtqzEd-7IuFxCL4SWw" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="close_door">
-<org.eventb.core.refinesEvent name="_0nGvQe5-Ed-dEtybZVK09Q" org.eventb.core.target="close_door"/>
+<org.eventb.core.refinesEvent name="_fbqfsu6TEd-y3JdGki7orA" org.eventb.core.target="close_door"/>
<org.eventb.core.guard name="_UtocQu5-Ed-dEtybZVK09Q" org.eventb.core.label="grd23_4" org.eventb.core.predicate="schedule = SCHEDULER_DOWN ⇒ floor ∉ ctrlDownButtonLightsSet"/>
<org.eventb.core.guard name="_UtocQ-5-Ed-dEtybZVK09Q" org.eventb.core.label="grd23_3" org.eventb.core.predicate="schedule = SCHEDULER_UP ⇒ floor ∉ ctrlUpButtonLightsSet"/>
<org.eventb.core.guard name="_UtpDUO5-Ed-dEtybZVK09Q" org.eventb.core.label="grd23_1" org.eventb.core.predicate="schedule ≠ SCHEDULER_WAIT"/>
<org.eventb.core.guard name="_UtpDUe5-Ed-dEtybZVK09Q" org.eventb.core.label="grd23_2" org.eventb.core.predicate="floor ∉ ctrlFloorButtonLightsSet"/>
</org.eventb.core.event>
<org.eventb.core.event name="_yC2soNqwEd-O4vbSPlarTw" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="start_move_up">
-<org.eventb.core.refinesEvent name="_0nHWUO5-Ed-dEtybZVK09Q" org.eventb.core.target="start_move_up"/>
+<org.eventb.core.refinesEvent name="_fbrGwO6TEd-y3JdGki7orA" org.eventb.core.target="start_move_up"/>
<org.eventb.core.guard name="_UtpDU-5-Ed-dEtybZVK09Q" org.eventb.core.label="grd23_1" org.eventb.core.predicate="schedule = SCHEDULER_UP"/>
</org.eventb.core.event>
<org.eventb.core.event name="_9uFS0Nd9Ed-Dle0at0Xgqg" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="move_up">
-<org.eventb.core.refinesEvent name="_0nHWUe5-Ed-dEtybZVK09Q" org.eventb.core.target="move_up"/>
+<org.eventb.core.refinesEvent name="_fbrGwe6TEd-y3JdGki7orA" org.eventb.core.target="move_up"/>
</org.eventb.core.event>
<org.eventb.core.event name="_yC36wNqwEd-O4vbSPlarTw" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="start_move_down">
-<org.eventb.core.refinesEvent name="_0nH9YO5-Ed-dEtybZVK09Q" org.eventb.core.target="start_move_down"/>
+<org.eventb.core.refinesEvent name="_fbrt0O6TEd-y3JdGki7orA" org.eventb.core.target="start_move_down"/>
<org.eventb.core.guard name="_UtpqYu5-Ed-dEtybZVK09Q" org.eventb.core.label="grd23_1" org.eventb.core.predicate="schedule = SCHEDULER_DOWN"/>
</org.eventb.core.event>
<org.eventb.core.event name="_9uF54dd9Ed-Dle0at0Xgqg" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="move_down">
-<org.eventb.core.refinesEvent name="_0nH9Ye5-Ed-dEtybZVK09Q" org.eventb.core.target="move_down"/>
+<org.eventb.core.refinesEvent name="_fbrt0e6TEd-y3JdGki7orA" org.eventb.core.target="move_down"/>
</org.eventb.core.event>
<org.eventb.core.event name="_yC5I4dqwEd-O4vbSPlarTw" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="stop">
-<org.eventb.core.refinesEvent name="_0nIkcO5-Ed-dEtybZVK09Q" org.eventb.core.target="stop"/>
+<org.eventb.core.refinesEvent name="_fbsU4O6TEd-y3JdGki7orA" org.eventb.core.target="stop"/>
<org.eventb.core.guard name="_UtqRcu5-Ed-dEtybZVK09Q" org.eventb.core.label="grd23_1" org.eventb.core.predicate="(floor∈ctrlFloorButtonLightsSet) ∨&#10; (floor∈ctrlUpButtonLightsSet ∧ schedule = SCHEDULER_UP) ∨&#10; (floor∈ctrlDownButtonLightsSet ∧ schedule = SCHEDULER_DOWN) ∨&#10; (floor∈ctrlUpButtonLightsSet ∧ schedule = SCHEDULER_DOWN ∧ (∀x·x∈0‥floor−1 ⇒ (x∉ctrlUpButtonLightsSet ∧ x∉ctrlDownButtonLightsSet ∧ x∉ctrlFloorButtonLightsSet))) ∨&#10; (floor∈ctrlDownButtonLightsSet ∧ schedule = SCHEDULER_UP ∧ (∀y·y∈floor+1‥LAST_FLOOR ⇒ (y∉ctrlUpButtonLightsSet ∧ y∉ctrlDownButtonLightsSet ∧ y∉ctrlFloorButtonLightsSet)))"/>
<org.eventb.core.action name="_UtqRc-5-Ed-dEtybZVK09Q" org.eventb.core.assignment="schedule ≔ SCHEDULER_WAIT" org.eventb.core.label="act23_2"/>
<org.eventb.core.action name="_UtqRdO5-Ed-dEtybZVK09Q" org.eventb.core.assignment="last_schedule ≔ schedule" org.eventb.core.label="act23_1"/>
Please sign in to comment.
Something went wrong with that request. Please try again.